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:
“Hidden away amongst Aschenbach’s writing was a passage directly asserting that nearly all the great things that exist owe their existence to a defiant despite: it is despite grief and anguish, despite poverty, loneliness, bodily weakness, vice and passion and a thousand inhibitions, that they have come into being at all. But this was more than an observation, it was an experience, it was positively the formula of his life and his fame, the key to his work.”
—Thomas Mann (18751955)