Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Sahlqvist formula
Summary
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 [Chagrova 1991] (see the examples below). Hence Sahlqvist formulas define only a (decidable) subset of modal formulas with first-order correspondents.
Sahlqvist formulas are built up from implications, where the consequent is positive and the antecedent is of a restricted form.
A boxed atom is a propositional atom preceded by a number (possibly 0) of boxes, i.e. a formula of the form (often abbreviated as for ).
A Sahlqvist antecedent is a formula constructed using ∧, ∨, and 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 implications using ∧ and (unrestricted), and using ∨ on formulas with no common variables.
Its first-order corresponding formula is , and it defines all reflexive frames
Its first-order corresponding formula is , and it defines all symmetric frames
or
Its first-order corresponding formula is , and it defines all transitive frames
or
Its first-order corresponding formula is , and it defines all dense frames
Its first-order corresponding formula is , and it defines all right-unbounded frames (also called serial)
Its first-order corresponding formula is , and it is the Church-Rosser property.
This is the McKinsey formula; it does not have a first-order frame condition.
The Löb axiom is not Sahlqvist; again, it does not have a first-order frame condition.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.