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 . Hence Sahlqvist formulas define only a 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 of boxes, i.e. a formula of the form .
  • A Sahlqvist antecedent is a formula constructed using ∧, ∨, and from boxed atoms, and negative formulas.
  • 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, and using ∨ on formulas with no common variables.

Examples of Sahlqvist formulas

;
;
; or
; or
;
;

Examples of non-Sahlqvist formulas

;
;
;

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 .