Misplaced Pages

Sahlqvist formula

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.

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 (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 ◻ ⋯ ◻ p {\displaystyle \Box \cdots \Box p} (often abbreviated as ◻ i p {\displaystyle \Box ^{i}p} for 0 ≤ i < ω {\displaystyle 0\leq i<\omega } ).
  • A Sahlqvist antecedent is a formula constructed using ∧, ∨, and ◊ {\displaystyle \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 ◻ {\displaystyle \Box } (unrestricted), and using ∨ on formulas with no common variables.

Examples of Sahlqvist formulas

p → ◊ p {\displaystyle p\rightarrow \Diamond p}
Its first-order corresponding formula is ∀ x R x x {\displaystyle \forall x\;Rxx} , and it defines all reflexive frames
p → ◻ ◊ p {\displaystyle p\rightarrow \Box \Diamond p}
Its first-order corresponding formula is ∀ x ∀ y [ R x y → R y x ] {\displaystyle \forall x\forall y} , and it defines all symmetric frames
◊ ◊ p → ◊ p {\displaystyle \Diamond \Diamond p\rightarrow \Diamond p} or ◻ p → ◻ ◻ p {\displaystyle \Box p\rightarrow \Box \Box p}
Its first-order corresponding formula is ∀ x ∀ y ∀ z [ ( R x y ∧ R y z ) → R x z ] {\displaystyle \forall x\forall y\forall z} , and it defines all transitive frames
◊ p → ◊ ◊ p {\displaystyle \Diamond p\rightarrow \Diamond \Diamond p} or ◻ ◻ p → ◻ p {\displaystyle \Box \Box p\rightarrow \Box p}
Its first-order corresponding formula is ∀ x ∀ y [ R x y → ∃ z ( R x z ∧ R z y ) ] {\displaystyle \forall x\forall y} , and it defines all dense frames
◻ p → ◊ p {\displaystyle \Box p\rightarrow \Diamond p}
Its first-order corresponding formula is ∀ x ∃ y R x y {\displaystyle \forall x\exists y\;Rxy} , and it defines all right-unbounded frames (also called serial)
◊ ◻ p → ◻ ◊ p {\displaystyle \Diamond \Box p\rightarrow \Box \Diamond p}
Its first-order corresponding formula is ∀ x ∀ x 1 ∀ z 0 [ R x x 1 ∧ R x z 0 → ∃ z 1 ( R x 1 z 1 ∧ R z 0 z 1 ) ] {\displaystyle \forall x\forall x_{1}\forall z_{0}} , and it is the Church–Rosser property.

Examples of non-Sahlqvist formulas

◻ ◊ p → ◊ ◻ p {\displaystyle \Box \Diamond p\rightarrow \Diamond \Box p}
This is the McKinsey formula; it does not have a first-order frame condition.
◻ ( ◻ p → p ) → ◻ p {\displaystyle \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.
( ◻ ◊ p → ◊ ◻ p ) ∧ ( ◊ ◊ q → ◊ q ) {\displaystyle (\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 ∀ x [ ∀ y ( R x y → ∃ z [ R y z ] ) → ∃ y ( R x y ∧ ∀ z [ R y z → z = y ] ) ] {\displaystyle \forall x)\rightarrow \exists y(Rxy\wedge \forall z)]} ) 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 . 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 .

References

  • 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: