Positive monotone modal logic (Q2243549)

Classical modal logic can be described using a set of atomic propositions, the usual Boolean operations, and a unary operator \(\Box\), subject to the axioms ensuring that \(\Box\) preserves finite meets. A second unary operator \(\lozenge\) can be then defined as De Morgan dual of \(\Box\). In particular, both are monotone and distribute over each other, that is, they satisfy \( \Box a \wedge \lozenge b \le \lozenge(a\wedge b)\) and \(\Box(a\vee b)\le \lozenge a \vee \Box b\). Monotone modal logic generalises normal modal logic in that it only requires that \(\Box\) colaxly preserve meets \( \Box(a\wedge b) \to \Box a \wedge \Box b \) and leaves aside the distributivity rules above. Semantics for monotone modal logic is given by coalgebras for the monotone neighbourhood functor on sets, which in turn correspond to Boolean algebras with monotone operators on the logical side [\textit{H. H. Hansen} and \textit{C. Kupke}, Electron. Notes Theor. Comput. Sci. 106, 121--143 (2004; Zbl 1271.03029)]. Similarly to Dunn's positive modal logic, positive monotone modal logic is the negation-free fragment of monotone modal logic; hence it is based on both modal operators \(\Box\) and \(\lozenge\), subject only to the monotonicity requirement and to the duality rules \( a \lor b = \top \Longrightarrow \Box a \lor \lozenge b = \top\) and \(a \land b = \bot \Longrightarrow \Box a \land \lozenge b = \bot\) (which in presence of negation reduce to the usual \(\lozenge = \neg \Box\neg\)). The paper under review provides full axiomatics for positive monotone modal logic, developed using the algebra-coalgebra formalism on top of the Priestley duality, as follows: First, a sound and complete semantics for positive monotone modal logic is provided by distributive lattices with monotone operators, which only form a quasi-variety due to the implicational form of the duality rules. Next, positive monotone modal logic is shown to be sound with respect to certain frames based on posets, which in turn can be described as coalgebras for a poset-based analogue of the monotone neighbourhood functor. Finally, completeness is established using descriptive monotone frames -- these being coalgebras for a convenient subfunctor of the double convex Vietoris functor on Priestley spaces, and a categorical duality between these and the distributive lattices with monotone operators mentioned above.