Formule de Sahlqvist

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 ${\displaystyle \Box \cdots \Box p}$.
• Une formule positive est une formule ne comportant pas de symbole ${\displaystyle \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 ${\displaystyle \wedge }$ et ${\displaystyle \Diamond }$.
• Une formule de Sahlqvist est une conjonction de négations de formules détachées.

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.

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

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 ${\displaystyle \Box \Diamond p\rightarrow \Diamond \Box p}$
• La formule de Löb ${\displaystyle \Box (\Box p\rightarrow p)\rightarrow \Box p}$
• La formule de Kripke ${\displaystyle \Box (p\to q)\to (\Box p\to \Box q)}$

• (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, Cambridge University Press, 1980 [détail de l’édition], 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 de l’article de Wikipédia en anglais intitulé « Sahlqvist formula » (voir la liste des auteurs).