Sahlqvist formula

In modal logic, Sahlqvist formulas are a certain kind of modal formula with remarkable properties. The Sahlqvist correspondence theorem states that every Sahlqvist formula is canonical, and corresponds to a class of Kripke frames definable by a first-order formula.

Sahlqvist's definition characterizes a decidable set of modal formulas with first-order correspondents. Since it is undecidable, by Chagrova's theorem, whether an arbitrary modal formula has a first-order correspondent, there are formulas with first-order frame conditions that are not Sahlqvist hagrova 1991(see the examples below). Hence Sahlqvist formulas define only a (decidable) subset of modal formulas with first-order correspondents.

Definition

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 $\Box\cdots\Box p$ (often abbreviated as $\Box^i p$ for $0 \leq i < \omega$).
* A ''Sahlqvist antecedent'' is a formula constructed using ∧, ∨, and $\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 $\Box$ (unrestricted), and using ∨ on formulas with no common variables.

Examples of Sahlqvist formulas

; $p \rightarrow \Diamond p$
: Its first-order corresponding formula is $\forall x \; Rxx$, and it defines all reflexive frames
; $p \rightarrow \Box\Diamond p$
: Its first-order corresponding formula is \forall x \forall y xy \rightarrow Ryx/math>, and it defines all symmetric frames
; $\Diamond \Diamond p \rightarrow \Diamond p$ or $\Box p \rightarrow \Box \Box p$
: Its first-order corresponding formula is \forall x \forall y \forall z Rxy \land Ryz) \rightarrow Rxz/math>, and it defines all transitive frames
; $\Diamond p \rightarrow \Diamond \Diamond p$ or $\Box \Box p \rightarrow \Box p$
: Its first-order corresponding formula is \forall x \forall y xy \rightarrow \exists z (Rxz \land Rzy)/math>, and it defines all dense frames
; $\Box p \rightarrow \Diamond p$
: Its first-order corresponding formula is $\forall x \exists y \; Rxy$, and it defines all right-unbounded frames (also called serial)
; $\Diamond\Box p \rightarrow \Box\Diamond p$
: Its first-order corresponding formula is \forall x \forall x_1 \forall z_0 xx_1 \land Rxz_0 \rightarrow \exists z_1 (Rx_1z_1 \land Rz_0z_1)/math>, and it is the Church–Rosser property.

Examples of non-Sahlqvist formulas

; $\Box\Diamond p \rightarrow \Diamond \Box p$
: This is the ''McKinsey formula''; it does not have a first-order frame condition.
; $\Box(\Box p \rightarrow p) \rightarrow \Box p$
: The ''Löb axiom'' is not Sahlqvist; again, it does not have a first-order frame condition.
; $(\Box\Diamond p \rightarrow \Diamond \Box p) \land (\Diamond\Diamond q \rightarrow \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 \forall x forall y(Rxy \rightarrow \exists z[Ryz \rightarrow \exists y(Rxy \wedge \forall z[Ryz \rightarrow z = y">yz.html" ;"title="forall y(Rxy \rightarrow \exists z[Ryz">forall y(Rxy \rightarrow \exists z[Ryz \rightarrow \exists y(Rxy \wedge \forall z[Ryz \rightarrow z = y] ) but is not equivalent to any Sahlqvist formula.

Kracht's theorem

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 odal 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'' odal Logic, Blackburn ''et al.'', Theorem 3.59

References

* 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.

Modal logic