A Sahlqvist theorem for distributive modal logic (Q705532)

A distributive modal logic is the negation-free fragment of a classical modal logic. The authors investigate, within the context of distributive modal logics, two types of modal operators: those that preserve disjunctions and conjunctions and those that turn disjunctions into conjunctions and conjunctions into disjunctions. Both algebraic and relational semantics for distributive modal logics are defined. The main contribution of the paper is an extension of Sahlqvist correspondence theory to this generalized setting of distributive modal logic. The proof of the Sahlqvist correspondence relies on a reduction to the classical case. The canonicity proof departs from the traditional style and uses the theory of canonical extensions developed by \textit{M. Gehrke} and \textit{B. Jónsson} [``Bounded distributive lattice expansions'', Math. Scand. 94, No. 1, 13--45 (2004; Zbl 1077.06008)]. Consequently, the authors obtain a general completeness result for distributive modal logics that are axiomatized by Sahlqvist axioms. This approach is related to that of \textit{S. Ghilardi} and \textit{G. Meloni} [``Constructive canonicity in non-classical logics'', Ann. Pure Appl. Logic 86, No. 1, 1--32 (1997; Zbl 0949.03019)], where canonicity for intuitionistic modal logics is investigated.