Monotonicity versus positivity in modal logics

TL;DR

This paper explores the Lyndon positivity property in propositional monotone modal logics, establishing conditions under which monotone formulas are equivalent to positive formulas and analyzing various modal logic classes.

Contribution

It extends Lyndon's classical results to modal logics, characterizes logics with LPP, and connects LPP with Lyndon interpolation and bisimulation invariance.

Findings

LPP holds for all normal modal logics with LIP

Logics between K4.3 and S4.3 lack LPP

Infinitely many tabular extensions of S4 have or lack LPP

Abstract

We say that a logic L has the Lyndon positivity property (LPP) if all formulas which are monotone in L (that is, are preserved under increasing the valuation on L-algebras) are L-equivalent to positive formulas (formulas without negation and implication symbols). In the present paper, we investigate LPP in propositional monotone modal logics. First, we transfer Lyndon's result from classical predicate calculus and prove LPP for all normal modal logics with the Lyndon interpolation property (LIP). Then we prove that all logics between K4.3 and S4.3 do not have LPP. We also show that among tabular extensions of S4 there are infinitely many logics with LPP and infinitely many logics without this property. Finally, we prove that all canonical monotone modal logics which are preserved under bisimulation products have both LIP and LPP. In particular, we show LIP and LPP for all logics that are axiomatizable over the minimal monotone logic EM by means of closed formulas and formulas of the form A(p) -> <>p, where A is positive.