First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

Résumé technique : Logique modale du premier ordre dans HOL : Plongements profonds et superficiels avec fidélité automatisée

Énoncé du problème
La logique modale du premier ordre (FML) combine la puissance expressive de la quantification avec la modalité, servant de cadre critique pour des applications en intelligence artificielle, en informatique et en philosophie. Bien que les plongements de la logique modale propositionnelle (PML) dans la logique d'ordre supérieur classique (HOL) aient été automatisés avec succès, l'extension de ces techniques à la FML introduit une complexité significative. Plus précisément, la FML nécessite la gestion de la liaison de variables, de la substitution et de la quantification sur des domaines potentiellement non dénombrables. Des travaux antérieurs [5] ont établi une méthodologie de plongement profond et superficiel pour la PML mais n'ont pas abordé la machinerie de substitution ou les problèmes de surjectivité inhérents à la quantification du premier ordre. Le défi consiste à fournir simultanément un plongement profond (pour le raisonnement syntaxique) et des plongements superficiels (pour la recherche de preuves automatisée) tout en prouvant leur fidélité mutuelle, particulièrement lorsque le domaine des individus est non dénombrable et que l'affectation des variables dans le plongement superficiel est restreinte à un ensemble dénombrable (par exemple, les entiers naturels).

Méthodologie
Les auteurs étendent l'environnement Isabelle/HOL pour supporter la FML sous sémantique de Kripke à domaine constant. La méthodologie emploie trois plongements parallèles :

1. Plongement profond (Deep Embedding) : Les formules sont représentées par un type de données inductif $\mathcal{F}$. La vérité est définie de manière récursive sur un modèle $\langle W, R, I, D \rangle$, une affectation $g$, et un monde $w$. La validité ($ValD$) quantifie universellement sur tous les modèles, affectations respectant le domaine $D$, et mondes.
2. Plongement superficiel maximal (Maximal Shallow Embedding) : Les formules sont élevées en termes-$\lambda$ qui abstraient explicitement sur tous les paramètres du modèle ($W, R, I, D, g, w$). Cela permet l'utilisation directe de l'automatisation d'Isabelle mais entraîne des types complexes.
3. Plongement superficiel minimal (Minimal Shallow Embedding) : Implémenté comme un locale d'Isabelle/HOL (MinS), cette approche promeut les paramètres statiques ($W, R, I, g$) en arguments de la locale, réduisant le type de la formule à $w \Rightarrow bool$. Crucialement, le quantificateur existentiel est encodé en utilisant le lieur méta-niveau natif d'Isabelle, tandis que l'opérateur modal déplace le paramètre du monde.

Pour combler l'écart entre le plongement profond et le plongement superficiel minimal, les auteurs développent une machinerie de substitution complète (prédicats de variables libres/liées, substitution évitant la capture, renommage alphabétique) nécessaire pour gérer les quantificateurs du premier ordre, ce qui était absent du travail propositionnel précédent.

Une innovation technique centrale est la mécanisation du théorème de Löwenheim–Skolem descendant dénombrable pour la FML. Ce théorème garantit que pour tout modèle et toute sous-domaine initiale dénombrable $D_0$, il existe un sous-domaine élémentaire dénombrable $\mathcal{N}$ préservant la vérité. Ceci est utilisé pour résoudre le problème de surjectivité : puisque l'affectation superficielle minimale $g: V \to D$ (où $V = \mathbb{N}$) ne peut pas être surjective sur un domaine $D$ non dénombrable, la fidélité directe échoue. En construisant un sous-domaine élémentaire dénombrable $\mathcal{N}$ sur lequel $g$ peut être surjective, et en prouvant que la vérité dans $D$ coïncide avec la vérité dans $\mathcal{N}$, les auteurs restaurent la fidélité sur le domaine complet.

Contributions clés

1. Développement de MinFMLinHOL : Une théorie Isabelle/HOL complète couvrant la FML avec des atomes relationnels binaires, des connecteurs propositionnels, la quantification existentielle et l'opérateur de boîte sous sémantique de domaine constant.
2. Trois plongements : La fourniture d'un plongement profond, d'un plongement superficiel maximal et d'un plongement superficiel minimal léger (emballé dans une locale).
3. Théorème de fidélité globale : L'introduction de la locale MinS permet un théorème global fort, FaithfulMS_all, stipulant que quantifier sur toutes les interprétations superficielles minimales récupère exactement la validité profonde.
4. Machinerie de substitution : Le développement d'outils syntaxiques nécessaires (lemmes de substitution, renommage, induction basée sur la taille) pour le plongement profond de la FML, étendant le travail propositionnel antérieur.
5. Théorème de Löwenheim–Skolem mécanisé : La formalisation du théorème de Löwenheim–Skolem descendant pour la sémantique de Kripke à domaine constant, qui sous-tend l'automatisation de la preuve de fidélité entre le plongement profond et le plongement superficiel minimal.
6. Résolution de la surjectivité : La conception d'une locale raffinée MinS_surj qui suppose que l'affectation est surjective sur un sous-domaine élémentaire, élevant la fidélité de la portée de l'affectation vers le domaine complet $D$.

Résultats
Le développement est validé par plusieurs expériences :

• Vérification axiomatique : Confirmation de l'axiome K, de la règle de nécessitation, et de la validité des formules Barcan et de la contraires de Barcan (qui sont valides sous sémantique de domaine constant).
• Correspondances de cadres (Frame Correspondences) : Vérification automatisée des correspondances entre les cadres réflexifs, transitifs et symétriques et les schémas d'axiomes T, 4 et B.
• Automatisation : L'utilisation des outils sledgehammer et nitpick est démontrée. Le plongement superficiel minimal permet à sledgehammer de traiter les buts modaux du premier ordre comme des buts HOL ordinaires, tandis que nitpick peut trouver des contre-exemples en réduisant le type du domaine, contournant ainsi efficacement les gardes de domaine explicites.

Signification
L'article affirme que ce travail représente l'extension naturelle des méthodologies de plongement propositionnel antérieures au cas du premier ordre. Sa signification primaire réside dans la démonstration que les plongements profonds et superficiels peuvent coexister dans une seule théorie HOL avec des preuves de fidélité automatisées, même en présence de quantification du premier ordre et de domaines non dénombrables. En exploitant le mécanisme de locale et le théorème de Löwenheim–Skolem, les auteurs surmontent la barrière technique de la surjectivité de l'affectation de variables, permettant l'utilisation d'outils d'automatisation HOL puissants pour la logique modale du premier ordre sans sacrifier la rigueur de la représentation syntaxique profonde. Ce travail établit une fondation pour de futures extensions, telles que les sémantiques à domaines variables ou l'inclusion de l'égalité, tout en se concentrant actuellement sur le fragment minimal à domaine constant.