Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA

Abstract

Modal formulae express monadic second-order properties on Kripke frames, but in many important cases these have first-order equivalents. Computing such equivalents is important for both logical and computational reasons. On the other hand, canonicity of modal formulae is important, too, because it implies frame-completeness of logics axiomatized with canonical formulae. Computing a first-order equivalent of a modal formula amounts to elimination of second-order quantifiers. Two algorithms have been developed for second-order quantifier elimination: SCAN, based on constraint resolution, and DLS, based on a logical equivalence established by Ackermann. In this paper we introduce a new algorithm, SQEMA, for computing first-order equivalents (using a modal version of Ackermann's lemma) and, moreover, for proving canonicity of modal formulae. Unlike SCAN and DLS, it works directly on modal formulae, thus avoiding Skolemization and the subsequent problem of unskolemization. We present the core algorithm and illustrate it with some examples. We then prove its correctness and the canonicity of all formulae on which the algorithm succeeds. We show that it succeeds not only on all Sahlqvist formulae, but also on the larger class of inductive formulae, introduced in our earlier papers. Thus, we develop a purely algorithmic approach to proving canonical completeness in modal logic and, in particular, establish one of the most general completeness results in modal logic so far.

26 pages, no figures, to appear in the Logical Methods in Computer Science

References in corpus (1)

• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA

Cited by in corpus (18)

• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Sahlqvist theory for impossible worlds
• Sahlqvist via Translation
• Dual characterizations for finite lattices via correspondence theory for monotone modal logic
• Constructive Canonicity of Inductive Inequalities
• Unified Correspondence and Proof Theory for Strict Implication
• Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Application of ALBA
• The Boolean Solution Problem from the Perspective of Predicate Logic -- Extended Version
• Complete Additivity and Modal Incompleteness
• Algorithmic Correspondence and Canonicity for Possibility Semantics
• Sahlqvist Correspondence Theory for Sabotage Modal Logic
• Unified Correspondence as a Proof-Theoretic Tool
• Algorithmic Correspondence for Hybrid Logic with Binder
• Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic
• Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)
• Distribution-Free Modal Logics: Sahlqvist -- Van Benthem Correspondence
• An extension of Kracht's theorem to generalized Sahlqvist formulas
• Sahlqvist Correspondence Theory for Second-Order Propositional Modal Logic