Namespaces
Variants
Actions

Sahlqvist theorem

From Encyclopedia of Mathematics
Jump to: navigation, search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

2020 Mathematics Subject Classification: Primary: 03B45 [MSN][ZBL]

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 theory got married" M. de Rijke (ed.) , Diamonds and Defaults , Kluwer Acad. Publ. (1993) pp. 175–214 Zbl 0829.03010
[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
How to Cite This Entry:
Sahlqvist theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Sahlqvist_theorem&oldid=54240
This article was adapted from an original article by W. van der HoekM. de Rijke (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article