Formule de Sahlqvist

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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é.

Définition[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

  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

Voir aussi[modifier | modifier le code]

Articles connexes[modifier | modifier le code]