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

摘要

Modal formulae express monadic second-order properties on Kripkeframes, but in many important cases these have first-orderequivalents. Computing such equivalents is important for both logicaland computational reasons. On the other hand, canonicity of modalformulae is important, too, because it implies frame-completeness oflogics axiomatized with canonical formulae. Computing a first-order equivalent of a modal formula amounts toelimination of second-order quantifiers. Two algorithms have beendeveloped for second-order quantifier elimination: SCAN, based onconstraint resolution, and DLS, based on a logical equivalenceestablished by Ackermann. In this paper we introduce a new algorithm, SQEMA, for computingfirst-order equivalents (using a modal version of Ackermann's lemma)and, moreover, for proving canonicity of modal formulae. Unlike SCANand DLS, it works directly on modal formulae, thus avoidingSkolemization and the subsequent problem of unskolemization. Wepresent the core algorithm and illustrate it with some examples. Wethen prove its correctness and the canonicity of all formulae on whichthe algorithm succeeds. We show that it succeeds not only on allSahlqvist formulae, but also on the larger class of inductiveformulae, introduced in our earlier papers. Thus, we develop a purelyalgorithmic approach to proving canonical completeness in modal logicand, in particular, establish one of the most general completenessresults in modal logic so far.