Namespaces
Variants
Actions

Difference between revisions of "Sahlqvist theorem"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
(TeX)
Line 1: Line 1:
 +
{{TEX|done}}
 
A theorem about the relational properties expressed by formulas of [[Modal logic|modal logic]], and about canonicity of modal formulas.
 
A theorem about the relational properties expressed by formulas of [[Modal logic|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100301.png" /> and negative formulas, using only <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100302.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100303.png" /> and the possibility operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100304.png" />. Then, a Sahlqvist formula is any formula that may be obtained by applying conjunctions and necessity operators <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100305.png" /> to implications of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100306.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100307.png" /> is a Sahlqvist antecedent and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100308.png" /> is a positive formula. For example, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s1100309.png" /> is a Sahlqvist formula.
+
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|Modal logic]]); moreover, this first-order equivalent <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003010.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003011.png" /> may be obtained in an effective way. For instance, for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003012.png" /> as above, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003013.png" /> expresses Euclidicity: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003014.png" />. 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|Boolean algebra]] with operators over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003015.png" /> many generators. Canonicity of a modal formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003016.png" /> implies that the modal logic obtained from the minimal logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003017.png" /> by adding <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003018.png" /> as an axiom, is axiomatically complete with respect to the class of models satisfying <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003019.png" />. Thus, the modal logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/s/s110/s110030/s11003020.png" /> is complete with respect to Euclidean Kripke frames (cf. also [[Kripke models|Kripke models]]).
+
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|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|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|Kripke models]]).
  
 
====References====
 
====References====
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. van Benthem,  "Correspondence theory"  D. Gabbay (ed.)  F. Guenthner (ed.) , ''Handbook of Philos. Logic'' , '''2''' , Reidel  (1984)  pp. 167–242</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  M. Kracht,  "How completeness and correspondence got married"  M. de Rijke (ed.) , ''Diamonds and Defaults'' , Kluwer Acad. Publ.  (1993)  pp. 175–214</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  G. Sambin,  V. Vaccaro,  "A new proof of Sahlqvist's theorem on modal definability and completeness"  ''J. Symb. Logic'' , '''54'''  (1989)  pp. 992–999</TD></TR></table>
 
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  J. van Benthem,  "Correspondence theory"  D. Gabbay (ed.)  F. Guenthner (ed.) , ''Handbook of Philos. Logic'' , '''2''' , Reidel  (1984)  pp. 167–242</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  M. Kracht,  "How completeness and correspondence got married"  M. de Rijke (ed.) , ''Diamonds and Defaults'' , Kluwer Acad. Publ.  (1993)  pp. 175–214</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  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</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  G. Sambin,  V. Vaccaro,  "A new proof of Sahlqvist's theorem on modal definability and completeness"  ''J. Symb. Logic'' , '''54'''  (1989)  pp. 992–999</TD></TR></table>

Revision as of 10:14, 11 October 2014

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
How to Cite This Entry:
Sahlqvist theorem. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Sahlqvist_theorem&oldid=33526
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