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 (see the examples below). Hence Sahlqvist formulas define only a (decidable) subset of modal formulas with first-order correspondents.
Read more about Sahlqvist Formula: Definition, Examples of Sahlqvist Formulas, Examples of Non-Sahlqvist Formulas, Kracht's Theorem
Famous quotes containing the word formula:
“So, if we must give a general formula applicable to all kinds of soul, we must describe it as the first actuality [entelechy] of a natural organized body.”
—Aristotle (384–323 B.C.)