Loading AI tools
De Wikipédia, l'encyclopédie libre
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é.
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.
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.
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 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 :
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.