Sahlqvist formula

Sahlqvist formula

In modal logic, Sahlqvist formulae are a certain kind of modal formula with remarkable properties. The Sahlqvist correspondence theorem states that everySahlqvist 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 BoxcdotsBox p.
* A "Sahlqvist antecedent" is a formula constructed using ∧, ∨, and Diamond from boxed atoms, and negative formulae (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 Box (unlimited), and using ∨ on formulae with no common variables.

Examples of non-Sahlqvist formulae

* The "McKinsey formula" BoxDiamond p ightarrow Diamond Box p does not have a first-order frame condition, hence is not Sahlqvist.
* The "Löb axiom" Box(Box p ightarrow p) ightarrow Box p is not Sahlqvist, again because it does not have a first-order frame condition.

Sahlqvist's definition characterises a decidable set of formulae. Since it is undecidable, by Chagrova's theorem, whether an arbitrary modal formula has a first-order frame condition, there are formulae with first-order frame conditions that are not Sahlqvist (Chagrova 1991).

* (BoxDiamond p ightarrow Diamond Box p) land (DiamondDiamond p ightarrow Diamond q) (the conjunction of the McKinsey formula and the 4 axiom) has a first-order frame condition but is not equivalent to any Sahlqvist formula.

References

* L. A. Chagrova, 1991. An undecidable problem in correspondence theory. "Journal of Symbolic Logic" 56:1261-1272.
* Marcus Kracht, 1993. How completeness and correspondence theory got married. In de Rijke, editor, "Diamonds and Defaults", pages 175-214. Kluwer.
* Henrik Sahlqvist, 1975. Correspondence and completeness in the first- and second-order semantics for modal logic. In "Proceedings of the Third Scandinavian Logic Symposium". North-Holland, Amsterdam.


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Formule De Sahlqvist — En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule …   Wikipédia en Français

  • Formule de sahlqvist — En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule …   Wikipédia en Français

  • Formule de Sahlqvist — En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule …   Wikipédia en Français

  • Kripke semantics — (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal… …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

  • Golden ratio — For the Ace of Base album, see The Golden Ratio (album). Not to be confused with Golden number. The golden section is a line segment divided according to the golden ratio: The total length a + b is to the length of the longer segment a as the… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”