Sahlqvist formula

Sahlqvist formula   (Redirected from Sahlqvist correspondence theorem) Jump to navigation Jump to search 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.

Contents 1 Definition 2 Examples of Sahlqvist formulas 3 Examples of non-Sahlqvist formulas 4 Kracht's theorem 5 References Definition 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 {displaystyle Box cdots Box p} (often abbreviated as {displaystyle Box ^{i}p} for {displaystyle 0leq i

Si quieres conocer otros artículos parecidos a Sahlqvist formula puedes visitar la categoría Modal logic.

Deja una respuesta

Tu dirección de correo electrónico no será publicada.


Utilizamos cookies propias y de terceros para mejorar la experiencia de usuario Más información