|
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.
- A boxed atom is a propositional atom preceded by a number (possibly 0) of boxes, i.e. a formula of the form <math>\Box\cdots\Box p<math>.
- A Sahlqvist antecedent is a formula constructed using ∧, ∨, and <math>\Diamond<math> 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 antecedents using ∧ and <math>\Box<math> (unlimited), and using ∨ on formulas with no common variables.
References
- Marcus Kracht. How completeness and correspondence theory got married. In de Rijke, editor, Diamonds and Defaults, pages 175-214. Kluwer, 1993.
- Henrik Sahlqvist. Correspondence and completeness in the first- and second-order semantics for modal logic, presented to The Third Scandinavial Logic Symposium, Uppsala, 1973. Published in Proceedings of same, North-Holland, Amsterdam, 1975.
|
