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 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.

Definition

Sahlqvist formulas are built up from implications, where the consequent is positive and the antecedent is of a restricted form.

Examples of Sahlqvist formulas

Its first-order corresponding formula is , and it defines all reflexive frames
Its first-order corresponding formula is , and it defines all symmetric frames
or
Its first-order corresponding formula is , and it defines all transitive frames
or
Its first-order corresponding formula is , and it defines all dense frames
Its first-order corresponding formula is , and it defines all right-unbounded frames (also called serial)
Its first-order corresponding formula is , and it is the Church-Rosser property.

Examples of non-Sahlqvist formulas

This is the McKinsey formula; it does not have a first-order frame condition.
The Löb axiom is not Sahlqvist; again, it does not have a first-order frame condition.
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 ) 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 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].

References

This article is issued from Wikipedia - version of the 10/12/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.