# 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 [Chagrova 1991] (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 $\Box \cdots \Box p$ (often abbreviated as $\Box ^{i}p$ for $0\leq i<\omega$).
* A Sahlqvist antecedent is a formula constructed using ∧, ∨, and $\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 $\Box$ (unrestricted), and using ∨ on formulas with no common variables.

## Examples of Sahlqvist formulas
### $p\rightarrow \Diamond p$

    Its first-order corresponding formula is $\forall x\;Rxx$, and it defines all reflexive frames

### $p\rightarrow \Box \Diamond p$

    Its first-order corresponding formula is $\forall x\forall y[Rxy\rightarrow Ryx]$, and it defines all symmetric frames

### $\Diamond \Diamond p\rightarrow \Diamond p$ or $\Box p\rightarrow \Box \Box p$

    Its first-order corresponding formula is $\forall x\forall y\forall z[(Rxy\land Ryz)\rightarrow Rxz]$, and it defines all transitive frames

### $\Diamond p\rightarrow \Diamond \Diamond p$ or $\Box \Box p\rightarrow \Box p$

    Its first-order corresponding formula is $\forall x\forall y[Rxy\rightarrow \exists z(Rxz\land Rzy)]$, and it defines all dense frames

### $\Box p\rightarrow \Diamond p$

    Its first-order corresponding formula is $\forall x\exists y\;Rxy$, and it defines all right-unbounded frames (also called serial)

### $\Diamond \Box p\rightarrow \Box \Diamond p$

    Its first-order corresponding formula is $\forall x\forall x_{1}\forall z_{0}[Rxx_{1}\land Rxz_{0}\rightarrow \exists z_{1}(Rx_{1}z_{1}\land Rz_{0}z_{1})]$, and it is the Church–Rosser property.

## Examples of non-Sahlqvist formulas
### $\Box \Diamond p\rightarrow \Diamond \Box p$

    This is the McKinsey formula; it does not have a first-order frame condition.

### $\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.

### $(\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 $\forall x[\forall y(Rxy\rightarrow \exists z[Ryz])\rightarrow \exists y(Rxy\wedge \forall z[Ryz\rightarrow z=y])]$) 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 [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].