Sahlqvist formula

From Wikipedia, the free encyclopedia

In modal logic, Sahlqvist formulae 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 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 \Box\cdots\Box 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.

[edit] Examples of non-Sahlqvist formulae

  • The McKinsey formula \Box\Diamond p \rightarrow \Diamond \Box p does not have a first-order frame condition, hence is not Sahlqvist.
  • The Löb axiom \Box(\Box p \rightarrow p) \rightarrow \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).

  • (\Box\Diamond p \rightarrow \Diamond \Box p) \land (\Diamond\Diamond p \rightarrow \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.

[edit] 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.
Languages