Méthode syntaxique en logique modale identifiant une vaste classe de formules modales (formules de Sahlqvist) qui bénéficient de correspondants de cadre du premier ordre garantis et de la canonicité complète : chaque formule de Sahlqvist correspond effectivement à une condition de cadre du premier ordre et engendre un axiome canonique dont l′ajout assure la complétude pour la classe de cadres correspondante.

Principe

Exploiter une forme syntaxique contrainte — occurrences positives et négatives arrangées selon un schéma de Sahlqvist — de sorte que les techniques de correspondance standard (dépliage, analyse de polarité et élimination du second ordre) conduisent à une condition de cadre du premier ordre et garantissent la canonicité par préservation syntaxique sous extensions canoniques.

Démonstration

L′axiome modal □p → p est une formule de Sahlqvist simple dont la correspondance est la condition de réflexivité en premier ordre : tout monde voit lui‑même ; des schémas de Sahlqvist plus complexes produisent des conditions de cadre telles que la transitivité ou la sérialité et garantissent la complétude de la logique axiomatisée par eux.

Mauvaise application

Supposer qu′un axiome donné est de Sahlqvist sans vérifier son motif syntaxique, ou attendre que les résultats de Sahlqvist couvrent des axiomes hors de la classe (par ex. formules non‑Sahlqvist mais ayant un correspondant de cadre), ce qui peut conduire à des affirmations erronées de canonicité ou de correspondants du premier ordre simples.

Conséquence

Lorsque applicable, la correspondance de Sahlqvist fournit des algorithmes effectifs pour calculer les conditions de cadre et garantit que les axiomes sont canoniques et que la logique axiomatisée est complète pour la classe de cadres correspondante, simplifiant les preuves de correspondance et de complétude.

Inversion

L′inversion est l′observation que de nombreuses conditions de cadre et résultats de complétude existent au‑delà des formules de Sahlqvist : certains correspondants valides ne sont pas de Sahlqvist et exigent des méthodes de correspondance algorithmiques (ALBA, extensions de la théorie de la correspondance) ou des arguments sémantiques au lieu de la voie Sahlqvist directe.

Limite

S′applique aux langages modaux normaux où le motif syntaxique de Sahlqvist tient ; n′englobe pas toutes les conditions de cadre exprimables modalement, et les extensions (modalités supplémentaires, points fixes, features hybrides) nécessitent des critères syntaxiques adaptés ou des techniques de correspondance séparées.

Tension sémantique

Tension entre la simplicité syntaxique et les garanties fortes de la classe de Sahlqvist et le désir d′une applicabilité plus large : les méthodes de correspondance algorithmiques vont au‑delà de Sahlqvist mais au prix de transformations plus complexes et de garanties uniformes de canonicité plus faibles.

Synthèse

La Correspondance de Sahlqvist est un critère syntaxique garantissant que certains axiomes modaux ont des correspondants effectifs du premier ordre et produisent des axiomatizations canoniques et complètes ; elle constitue un pont uniforme puissant entre syntaxe modale et sémantique de cadre, avec des limites reconnues qui motivent des généralisations algorithmiques.