Sahlqvist formula

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

* A "boxed atom" is a propositional atom preceded by a number (possibly 0) of boxes, i.e. a formula of the form $BoxcdotsBox\; p$.
* A "Sahlqvist antecedent" is a formula constructed using ∧, ∨, and $Diamond$ from boxed atoms, and negative formulae (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 antecedents using ∧ and $Box$ (unlimited), and using ∨ on formulae with no common variables.

Examples of non-Sahlqvist formulae

* The "McKinsey formula" $BoxDiamond\; p\; ightarrow\; Diamond\; Box\; p$ does not have a first-order frame condition, hence is not Sahlqvist.
* The "Löb axiom" $Box(Box\; p\; ightarrow\; p)\; ightarrow\; Box\; p$ is not Sahlqvist, again because it does not have a first-order frame condition.

Sahlqvist's definition characterises a decidable set of formulae. Since it is undecidable, by Chagrova's theorem, whether an arbitrary modal formula has a first-order frame condition, there are formulae with first-order frame conditions that are not Sahlqvist (Chagrova 1991).

* $(BoxDiamond\; p\; ightarrow\; Diamond\; Box\; p)\; land\; (DiamondDiamond\; p\; ightarrow\; Diamond\; q)$ (the conjunction of the McKinsey formula and the 4 axiom) has a first-order frame condition but is not equivalent to any Sahlqvist formula.

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.