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:
“My formula for greatness in human beings is amor fati: that one wants to change nothing, neither forwards, nor backwards, nor in all eternity. Not merely to endure necessity, still less to hide it—all idealism is mendacity in the face of necessity—but rather to love it.”
—Friedrich Nietzsche (1844–1900)