Sahlqvist formula

Sahlqvist formulas are built up from implications, where the consequent is positive and the antecedent is of a restricted form.

• A boxed atom is a propositional atom preceded by a number (possibly 0) of boxes, i.e. a formula of the form $\backslash Box\backslash cdots\backslash Box\; p$ (often abbreviated as $\backslash Box^i\; p$ for ).
• A Sahlqvist antecedent is a formula constructed using ∧, ∨, and $\backslash Diamond$ from boxed atoms, and negative formulas (including the constants ⊥, ⊤).
• A Sahlqvist implication is a formula A → B, where A is a Sahlqvist antecedent, and B is a positive formula.
• A Sahlqvist formula is constructed from Sahlqvist implications using ∧ and $\backslash Box$ (unrestricted), and using ∨ on formulas with no common variables.

; $p\; \backslash rightarrow\; \backslash Diamond\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash ;\; Rxx$, and it defines all reflexive frames

; $p\; \backslash rightarrow\; \backslash Box\backslash Diamond\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash forall\; y\; [Rxy\; \backslash rightarrow\; Ryx]$, and it defines all symmetric frames

; $\backslash Diamond\; \backslash Diamond\; p\; \backslash rightarrow\; \backslash Diamond\; p$ or $\backslash Box\; p\; \backslash rightarrow\; \backslash Box\; \backslash Box\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash forall\; y\; \backslash forall\; z\; [(Rxy\; \backslash land\; Ryz)\; \backslash rightarrow\; Rxz]$, and it defines all transitive frames

; $\backslash Diamond\; p\; \backslash rightarrow\; \backslash Diamond\; \backslash Diamond\; p$ or $\backslash Box\; \backslash Box\; p\; \backslash rightarrow\; \backslash Box\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash forall\; y\; [Rxy\; \backslash rightarrow\; \backslash exists\; z\; (Rxz\; \backslash land\; Rzy)]$, and it defines all dense frames

; $\backslash Box\; p\; \backslash rightarrow\; \backslash Diamond\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash exists\; y\; \backslash ;\; Rxy$, and it defines all right-unbounded frames (also called serial)

; $\backslash Diamond\backslash Box\; p\; \backslash rightarrow\; \backslash Box\backslash Diamond\; p$

: Its first-order corresponding formula is $\backslash forall\; x\; \backslash forall\; x\_1\; \backslash forall\; z\_0\; [Rxx\_1\; \backslash land\; Rxz\_0\; \backslash rightarrow\; \backslash exists\; z\_1\; (Rx\_1z\_1\; \backslash land\; Rz\_0z\_1)]$, and it is the Church–Rosser property.

; $\backslash Box\backslash Diamond\; p\; \backslash rightarrow\; \backslash Diamond\; \backslash Box\; p$

: This is the McKinsey formula; it does not have a first-order frame condition.

; $\backslash Box(\backslash Box\; p\; \backslash rightarrow\; p)\; \backslash rightarrow\; \backslash Box\; p$

: The Löb axiom is not Sahlqvist; again, it does not have a first-order frame condition.

; $(\backslash Box\backslash Diamond\; p\; \backslash rightarrow\; \backslash Diamond\; \backslash Box\; p)\; \backslash land\; (\backslash Diamond\backslash Diamond\; q\; \backslash rightarrow\; \backslash Diamond\; q)$

: The conjunction of the McKinsey formula and the (4) axiom has a first-order frame condition (the conjunction of the transitivity property with the property $\backslash forall\; x[\backslash forall\; y(Rxy\; \backslash rightarrow\; \backslash exists\; z[Ryz])\; \backslash rightarrow\; \backslash exists\; y(Rxy\; \backslash wedge\; \backslash forall\; z[Ryz\; \backslash rightarrow\; z\; =\; y])]$) but is not equivalent to any Sahlqvist formula.

When a Sahlqvist formula is used as an axiom in a normal modal logic, the logic is guaranteed to be complete with respect to the basic elementary class of frames the axiom defines. This result comes from the Sahlqvist completeness theorem [Modal Logic, Blackburn et al., Theorem 4.42]. But there is also a converse theorem, namely a theorem that states which first-order conditions are the correspondents of Sahlqvist formulas. Kracht's theorem states that any Sahlqvist formula locally corresponds to a Kracht formula; and conversely, every Kracht formula is a local first-order correspondent of some Sahlqvist formula which can be effectively obtained from the Kracht formula [Modal Logic, Blackburn et al., Theorem 3.59].

• Patrick Blackburn, Maarten de Rijke, Yde Venema, 2010. Modal logic (4. print. with corr.). Cambridge Univ. Press.
• L. A. Chagrova, 1991. An undecidable problem in correspondence theory. Journal of Symbolic Logic 56:1261–1272.
• Marcus Kracht, 1993. How completeness and correspondence theory got married. In de Rijke, editor, Diamonds and Defaults, pages 175–214. Kluwer.
• Henrik Sahlqvist, 1975. Correspondence and completeness in the first- and second-order semantics for modal logic. In Proceedings of the Third Scandinavian Logic Symposium. North-Holland, Amsterdam.

Category:Modal logic