Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules

1. Problématique et Contexte

L'article aborde le défi de la construction de systèmes de preuve analytiques (sans coupure) pour une large classe de logiques modales quantifiées (QML) incluant l'égalité.

• Limites des approches existantes : Bien que les systèmes de séquents étiquetés (labeled sequents) aient réussi à fournir des calculs corrects et complets pour de nombreuses QML, ils souffrent de défauts structurels : ils introduisent souvent des structures syntaxiques redondantes, gonflent la taille des preuves et manquent d'une interprétation par une formule unique (formula interpretation).
• Le problème des domaines : Dans le contexte des logiques modales quantifiées, les règles d'inférence standards pour les quantificateurs tendent à forcer des conditions de domaines trop restrictives (notamment des domaines constants). Par exemple, l'ajout des règles standards pour le quantificateur universel dans un système de séquents imbriqués (nested sequents) entraîne la preuve de la formule de Barcan (BF) et de sa converse (CBF), ce qui correspond sémantiquement à des domaines constants.
• Objectif : Développer un système de séquents imbriqués (nested sequents) sans coupure, capable de capturer une variété de conditions de domaines (croissants, décroissants, constants, vides) et de conditions de cadres (frames) générales, tout en conservant une interprétation par formule et des propriétés de preuve élégantes.

2. Méthodologie

Les auteurs proposent une extension des séquents imbriqués en intégrant deux mécanismes clés :

A. Signatures et Séquents Imbriqués

• Structure : Un séquent imbriqué est défini comme un arbre de séquents plats (multisets de formules).
• Signatures : Chaque composante (nœud) du séquent imbriqué est associée à une signature, c'est-à-dire un multiset de termes. Cela permet d'encoder explicitement les prédicats d'existence locaux ($E$) et de restreindre l'introduction des quantificateurs, évitant ainsi les pièges des règles "structure-free" qui imposent des domaines constants.
• Sémantique : Les modèles utilisés sont des modèles relationnels avec deux types de domaines pour chaque monde : un domaine extérieur (objets possibles) et un domaine intérieur (objets existants). Les auteurs se concentrent sur des modèles à domaines extérieurs constants, car leur système de preuve implique naturellement cette condition.

B. Règles de Réachabilité (Reachability Rules)

C'est la contribution méthodologique majeure. Les règles d'inférence sont paramétrées par des grammaires formelles (systèmes semi-Thue, ou $\Sigma$-systèmes).

• Fonctionnement : Ces règles opèrent en propageant ou en consommant des formules et des termes le long de chemins spécifiques à l'intérieur de l'arbre du séquent imbriqué.
• Encodage : Les chemins sont encodés sous forme de chaînes de caractères générées par une grammaire (utilisant les symboles $R$ pour les transitions futures et $\bar{R}$ pour les transitions passées).
• Modularité : En changeant le $\Sigma$-système paramétrique, on peut capturer différentes conditions de cadres (réflexivité, transitivité, symétrie, conditions de chemin généralisées $G(n,k)$) et différentes conditions de domaines (croissants, décroissants, constants) sans modifier la structure de base du calcul.

3. Contributions Clés

1. Systèmes Unifiés et Modulaires : Présentation d'une famille de systèmes de séquents imbriqués ($NQ^{\circ}_{=.K}(C)$) paramétrés par un ensemble de conditions de cadres $C$. Un seul cadre formel suffit pour couvrir une vaste gamme de logiques (de $K$ à $S5$, avec égalité et variations de domaines).
2. Règles de Réachabilité : Introduction de règles d'inférence basées sur des langages formels qui permettent de gérer dynamiquement la propagation des informations le long des chemins de l'arbre de preuve.
3. Traitement de l'Égalité : Intégration complète de l'égalité (avec les axiomes de réflexivité, substitution et rigidité) dans le cadre des séquents imbriqués pour les QML.
4. Observation sur la Règle de Barcan Étendue (EBR) : Les auteurs démontrent que la règle universelle standard dans leur système imbriqué subsume la Règle de Barcan Étendue (EBR). Cela implique que leur système capture naturellement des logiques à domaines extérieurs constants, expliquant pourquoi il est impossible de capturer des modèles à domaines extérieurs variables avec cette formulation spécifique sans modifier la règle du quantificateur universel.
5. Preuve de l'Admissibilité de la Règle "Shift" : Identification d'une nouvelle règle structurelle, la règle shift ($sft(C)$), qui permet de propager les imbriquements le long des chemins. Cette règle est cruciale pour unifier la preuve d'élimination de la coupure.

4. Résultats Principaux

Les auteurs établissent les propriétés métathéoriques fondamentales de leurs systèmes :

• Correction (Soundness) : Les systèmes sont corrects par rapport à la sémantique des modèles relationnels à domaines intérieurs et extérieurs.
• Complétude : Ils prouvent la complétude en extrayant un contre-modèle à partir d'une tentative de preuve échouée (méthode de Kripke adaptée aux séquents imbriqués).
• Inversibilité (Invertibility) : Toutes les règles du système sont inversibles en préservant la hauteur (hp-invertible). Cela signifie que si la conclusion est prouvable, les prémisses le sont aussi avec une preuve de hauteur égale ou inférieure.
• Admissibilité des Règles Structurelles : Ils démontrent l'admissibilité en préservant la hauteur de règles telles que le renforcement (weakening), la contraction, la substitution et la nouvelle règle shift.
• Élimination de la Coupure (Cut-Elimination) :
  • Ils prouvent un théorème d'élimination de la coupure syntaxique et non trivial.
  • La preuve est uniforme pour toute la classe de logiques considérée, grâce à l'utilisation de la règle shift qui gère simultanément toutes les conditions de chemin généralisées, évitant ainsi d'avoir besoin de règles ad hoc pour chaque logique spécifique.

5. Signification et Perspectives

• Avancée Théorique : Ce travail fournit la première preuve de systèmes de séquents imbriqués corrects et complets (sans coupure) pour des QML caractérisées par des modèles à domaines intérieurs et extérieurs, comblant un vide dans la littérature par rapport aux systèmes étiquetés.
• Efficacité et Esthétique : La méthode évite la redondance syntaxique des systèmes étiquetés et conserve l'avantage des séquents imbriqués : des preuves compactes et une interprétation par formule directe.
• Limites et Futur :
  • Le système actuel impose des domaines extérieurs constants en raison de la nature de la règle universelle utilisée. Les auteurs suggèrent que pour capturer des modèles à domaines extérieurs variables, une nouvelle règle pour le quantificateur universel serait nécessaire.
  • Des travaux futurs visent à extraire des systèmes axiomatiques à partir de l'interprétation par formule des séquents imbriqués et à étendre le cadre à des termes non rigides ou à des sémantiques de type "counterpart".

En résumé, cet article propose un cadre unifié, puissant et élégant pour l'analyse proof-théorique des logiques modales quantifiées avec égalité, en surmontant les limitations des approches précédentes grâce à l'intégration intelligente de signatures et de règles de réachabilité paramétrées par grammaires.