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 first-order definable class of Kripke frames.
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 [Chagrova 1991] (see the examples below). Hence Sahlqvist formulas define only a (decidable) subset of modal formulas with first-order correspondents.
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 (often abbreviated as ◻ i p for 0 ≤ i < ω ).A Sahlqvist antecedent is a formula constructed using ∧, ∨, and ◊ 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 ◻ (unrestricted), and using ∨ on formulas with no common variables. p → ◊ p Its first-order corresponding formula is
∀ x R x x , and it defines all
reflexive frames p → ◻ ◊ p Its first-order corresponding formula is
∀ x ∀ y [ R x y → R y x ] , and it defines all
symmetric frames ◊ ◊ p → ◊ p or ◻ p → ◻ ◻ p Its first-order corresponding formula is
∀ x ∀ y ∀ z [ ( R x y ∧ R y z ) → R x z ] , and it defines all
transitive frames ◊ p → ◊ ◊ p or ◻ ◻ p → ◻ p Its first-order corresponding formula is
∀ x ∀ y [ R x y → ∃ z ( R x z ∧ R z y ) ] , and it defines all
dense frames ◻ p → ◊ p Its first-order corresponding formula is
∀ x ∃ y R x y , and it defines all
right-unbounded frames (also called serial)
◊ ◻ p → ◻ ◊ 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 ) ] , and it is the Church-Rosser property.
◻ ◊ p → ◊ ◻ p This is the
McKinsey formula; it does not have a first-order frame condition.
◻ ( ◻ p → p ) → ◻ p The
Löb axiom is not Sahlqvist; again, it does not have a first-order frame condition.
( ◻ ◊ p → ◊ ◻ p ) ∧ ( ◊ ◊ q → ◊ 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 ] ) ] ) 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 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].
