Formule de sahlqvist

Formule de sahlqvist

Formule de Sahlqvist

En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule de Sahlqvist est canonique (au sens de la sémantique de Kripke) et correspond à une classe de cadres de Kripke caractérisable par une formule en logique du premier ordre décrivant une propriété de la relation d'accessibilité.

Sommaire

Définition

Les formules de Sahlqvist sont définies au moyen de plusieurs définitions intermédiaires. Il existe plusieurs manières de les caractériser, plus ou moins complexes. La définition présentée ici[1] n'est pas celle proposée originellement par Sahlqvist[2], mais elle lui est strictement équivalente.

Note : Les définitions intermédiaires ne valent que pour la définition des formules de Sahlqvist, et ne peuvent s'appliquer sans précaution à la logique modale en général.

  • Une formule positive forte est un atome propositionnel précédé d'un certain nombre (possiblement zéro) de modalités universelles, c'est-à-dire une formule de la forme \Box\cdots\Box p.
  • Une formule positive est une formule ne comportant pas de symbole \neg.
  • Une formule négative est la négation d'une formule positive.
  • Une formule détachée est une formule formée à partir de formules négatives et positives fortes en utilisant uniquement \wedge et \Diamond.
  • Une formule de Sahlqvist est une conjonction de négations de formules détachées.

Exemples

Dans les exemples[1], on trouvera entre crochets, pour plus de lisibilité, les formules négatives et positives fortes utilisées pour former les formules détachées.

  • \Box p \to p (axiome T de la logique modale) est équivalent à la formule de Sahlqvist : \neg([\Box p] \wedge [\neg p])
  • \Box p \to \Box\Box p (axiome 4 de la logique modale) est équivalent à la formule de Sahlqvist : \neg([\Box p] \wedge [\neg \Box\Box p])
  • \Diamond p \to \Box \Diamond p (axiome 5 de la logique modale) est équivalent à la formule de Sahlqvist : \neg(\Diamond [p] \wedge [\neg \Box \Diamond p])
  • \Diamond \Box p \to \Box \Diamond p est équivalent à la formule de Sahlqvist : \neg(\Diamond [\Box p] \wedge [\neg \Box \Diamond p])

Contre-exemples

La plupart des formules rencontrées en logique modale sont des formules de Sahlqvist. Les formules suivantes sont des contre-exemples célèbres, que le théorème de Sahlqvist ne met en correspondance avec aucune formule du premier ordre sur la relation d'accessibilité :

  • La formule de McKinsey \Box\Diamond p \rightarrow \Diamond \Box p
  • La formule de Löb \Box(\Box p \rightarrow p) \rightarrow \Box p
  • La formule de Kripke \Box (p \to q) \to (\Box p \to \Box q)

Conséquences du théorème de Chagrova

La définition de Sahlqvist caractérise en fait un ensemble décidable de formules. Or, d'après le théorème de Chagrova[3], le fait qu'une formule modale arbitraire corresponde ou non à une formule du premier ordre sur la relation d'accessibilité est indécidable. Il existe donc des formules modales qui correspondent à une telle formule, mais qui ne sont pas des formules de Sahlqvist. Un exemple en est la formule suivante, conjonction de la formule de McKinsey et de l'axiome 4 de la logique modale :

  • (\Box\Diamond p \rightarrow \Diamond \Box p) \land (\Diamond\Diamond p \rightarrow \Diamond q)

Notes et références de l'article

  1. ↑ a  et b  Ian Hodkinson, Marek Sergot et Michael Huth, Modal and Temporal Logic, Imperial College London, Londres, Grande-Bretagne, 2004, part 3, Frame conditions
  2. ↑ Henrik Sahlqvist, Correspondence and completeness in the first- and second-order semantics for modal logic. In Proceedings of the Third Scandinavian Logic Symposium, North-Holland, Amsterdam, 1975
  3. ↑ L. A. Chagrova, An undecidable problem in correspondence theory. In Journal of Symbolic Logic n° 56, 1991, pp. 1261-1272
  • (en) Patrick Blackburn, Maarten de Rijke et Yde Venema, Modal Logic, 2001 [détail des éditions], chap. 3 Frames, pp. 123-187.
  • (en)Brian F. Chellas, Modal logic, an introduction, 1980 [détail des éditions] , chap. 5 Determination and decidability for normal systems, pp. 162--206.
  • (en) Marcus Kracht, How completeness and correspondence theory got married. In de Rijke (ed), Diamonds and Defaults, Kluwer, 1993, pp. 175-214.
  • (en) Cet article est partiellement ou en totalité issu d’une traduction de l’article de Wikipédia en anglais intitulé « Sahlqvist formula ».

Voir aussi

Articles connexes


  • Portail de la logique Portail de la logique
Ce document provient de « Formule de Sahlqvist ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Formule de sahlqvist de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

  • Formule De Sahlqvist — En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule …   Wikipédia en Français

  • Formule de Sahlqvist — En logique modale, les formules de Sahlqvist (du nom du mathématicien norvégien Henrik Sahlqvist) constituent une classe de formules modales assortie de propriétés remarquables. Le théorème de correspondance de Sahlqvist affirme que toute formule …   Wikipédia en Français

  • Semantique de Kripke — Sémantique de Kripke La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à… …   Wikipédia en Français

  • Sémantique de Kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

  • Sémantique de kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

  • Aléthique — Logique modale La logique modale est une logique à laquelle on a ajouté des modificateurs, qu’on pourrait comprendre en grammaire comme des adverbes. Par exemple, on peut modifier la proposition « Il pleut » comme ceci : Il est… …   Wikipédia en Français

  • Catégorie modale — Logique modale La logique modale est une logique à laquelle on a ajouté des modificateurs, qu’on pourrait comprendre en grammaire comme des adverbes. Par exemple, on peut modifier la proposition « Il pleut » comme ceci : Il est… …   Wikipédia en Français

  • Catégories modales — Logique modale La logique modale est une logique à laquelle on a ajouté des modificateurs, qu’on pourrait comprendre en grammaire comme des adverbes. Par exemple, on peut modifier la proposition « Il pleut » comme ceci : Il est… …   Wikipédia en Français

  • Logique Modale — La logique modale est une logique à laquelle on a ajouté des modificateurs, qu’on pourrait comprendre en grammaire comme des adverbes. Par exemple, on peut modifier la proposition « Il pleut » comme ceci : Il est possible qu’il… …   Wikipédia en Français

  • Logique modale — La logique modale est une logique à laquelle on a ajouté des modificateurs, qu’on pourrait comprendre en grammaire comme des adverbes. Par exemple, on peut modifier la proposition « Il pleut » comme ceci : Il est possible qu’il… …   Wikipédia en Français

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”