Sahlqvist theorem

A theorem about the relational properties expressed by formulas of modal logic, and about canonicity of modal formulas.

To be precise, let a positive (negative) formula of modal logic be one where all proposition letters occur in the scope of an even (odd) number of negation signs only. Let a Sahlqvist antecedent be a formula that is built up from proposition letters prefixed by any finite number of necessity operators $\Box$ and negative formulas, using only $\lor$, $\land$ and the possibility operator $\Diamond$. Then, a Sahlqvist formula is any formula that may be obtained by applying conjunctions and necessity operators $\Box$ to implications of the form $\phi\to\psi$, where $\phi$ is a Sahlqvist antecedent and $\psi$ is a positive formula. For example, $\alpha=\Diamond\Box p\to\Box p$ is a Sahlqvist formula.

Sahlqvist's theorem states two things. First, although, in general, every modal formula is equivalent to a second-order formula, Sahlqvist formulas have a first-order equivalent (cf. Modal logic); moreover, this first-order equivalent $FO(\varphi)$ of $\varphi$ may be obtained in an effective way. For instance, for $\alpha$ as above, $FO(\alpha)$ expresses Euclidicity: $\forall x\forall y\forall z((Rxy\land Rxz)\to Ryz)$. Secondly, every Sahlqvist formula is canonical. Here, canonicity of a modal formula means that it is valid on the canonical frame. Algebraically, the latter may be viewed as the Stone representation of the free Boolean algebra with operators over $\omega$ many generators. Canonicity of a modal formula $\varphi$ implies that the modal logic obtained from the minimal logic $K$ by adding $\varphi$ as an axiom, is axiomatically complete with respect to the class of models satisfying $FO(\varphi)$. Thus, the modal logic $K+\alpha$ is complete with respect to Euclidean Kripke frames (cf. also Kripke models).

References

[a1]	J. van Benthem, "Correspondence theory" D. Gabbay (ed.) F. Guenthner (ed.) , Handbook of Philos. Logic , 2 , Reidel (1984) pp. 167–242
[a2]	M. Kracht, "How completeness and correspondence got married" M. de Rijke (ed.) , Diamonds and Defaults , Kluwer Acad. Publ. (1993) pp. 175–214
[a3]	H. Sahlqvist, "Completeness and correspondence in the first and second order semantics for modal logic" S. Kanger (ed.) , Proc. Third Scand. Logic Symp. Uppsala (1973) , North-Holland (1975) pp. 110–143
[a4]	G. Sambin, V. Vaccaro, "A new proof of Sahlqvist's theorem on modal definability and completeness" J. Symb. Logic , 54 (1989) pp. 992–999