Аннотация:
In classical propositional logic, conjunction, disjunction, and the constants generate all monotone Boolean functions; in other words, every monotone formula is equivalent to a positive one (without negation or implication). Lyndon proved an analogue of this result for first-order logic. We study the same phenomenon, which we call the Lyndon positivity property (LPP), in propositional modal logics. The main question is how the presence of the modal operators affects the equivalence between monotone and positive formulas. A close connection between LPP and the Lyndon interpolation property is established; many standard modal systems are shown to enjoy LPP, while explicit counterexamples demonstrate that the property fails in some well-known modal logics.