A Gödel Modal Logic Over Witnessed Models

Résumé Technique : Une logique modale de Gödel sur des modèles avec témoins

Énoncé du Problème
Les logiques modales de Gödel (GK) fournissent un cadre pour raisonner sur les notions graduées d'incomplétude et de vague en utilisant les opérateurs de nécessité ($\Box$) et de possibilité ($\Diamond$) évalués sur l'intervalle unité réel $[0,1]$. La sémantique standard de ces logiques repose sur des modèles de Gödel-Kripke (modèles G), où la valeur de vérité d'une formule modale est définie par l'infimum ou le supremum des valeurs de vérité sur les mondes accessibles. Une limitation critique de cette sémantique standard est que ces bornes ne sont pas nécessairement atteintes par un monde accessible spécifique. Ce phénomène de « base limite » entraîne des pathologies logiques significatives : la logique ne possède pas la propriété du modèle fini (FMP), et certaines validités dans les modèles finis (par exemple, $\Box\neg\neg\phi \to \neg\Box\phi$) échouent dans les modèles infinis. Par conséquent, les arguments sémantiques nécessitent souvent des comportements véritablement infinitaires, ce qui complique le raisonnement automatisé et l'analyse de la théorie de la preuve.

Méthodologie
Les auteurs introduisent GW, une logique modale de Gödel basée sur des modèles avec témoins (witnessed models). Dans un modèle GW, la sémantique des opérateurs modaux est contrainte de telle sorte que l'infimum et le supremum définissant les valeurs de vérité de $\Box\phi$ et $\Diamond\phi$ doivent être atteints par au moins un monde accessible (un « témoin »). Cela garantit que la valeur de vérité d'une formule modale est déterminée par des mondes concrets plutôt que par des approximations asymptotiques.

Pour analyser GW, les auteurs développent un calcul de réfutation fondé sur des contraintes nommé CGW. La méthodologie implique :

1. Langage de contraintes : Les formules sont traduites en contraintes sur un ensemble dénombrable d'étiquettes représentant des mondes. Ces contraintes impliquent des termes atomiques (mondes, relations d'accessibilité $R$, et évaluations propositionnelles) et des relations ($<, \le, >, \ge$) sur les nombres rationnels dans $[0,1]$.
2. Calcul de réfutation : CGW est conçu pour certifier qu'une formule n'est pas valide dans n'importe quel modèle GW. Il emploie des règles propositionnelles, des règles modales (introduisant de nouvelles étiquettes pour les témoins) et des règles pour la relation d'accessibilité (règles $R$).
3. Recherche de preuve et génération de contre-modèle : Les auteurs conçoivent une procédure de recherche de preuve par rétroaction (backward) qui se termine. Si la recherche échoue à dériver une contradiction, la procédure trace le calcul pour construire un contre-modèle fini (spécifiquement, un modèle GW discret) pour la formule d'entrée.
4. Analyse de complexité : Une procédure de décision PSPACE est esquissée, utilisant une recherche récursive qui gère les assignations de valeurs de vérité aux sous-formules sans construire explicitement l'ensemble du modèle en mémoire.

Contributions Clés

• Définition de GW : La formalisation de la logique modale de Gödel sur des modèles de Kripke avec témoins, la distinguant de la GK standard et de la variante nette (crisp) $GW^c$.
• Calcul CGW : La présentation d'un calcul de réfutation sain et complet pour GW. Le calcul gère les contraintes spécifiques de la sémantique avec témoins, particulièrement l'exigence que les bornes soient atteintes.
• Propriété du Modèle Fini (FMP) : Les auteurs prouvent que GW jouit de la FMP comme conséquence directe de la procédure de recherche de preuve qui se termine. Si une formule n'est pas valide, un contre-modèle fini existe. Cela contraste avec la GK standard, qui ne possède pas la FMP.
• Inclusion et non-interdéfiniabilité :
  • Le papier démontre que la logique modale classique K peut être plongée dans GW (et des logiques apparentées) via une traduction impliquant la double négation.
  • Il prouve que $\Box$ et $\Diamond$ ne sont pas interdéfinissables dans toute logique modale contenue dans $GW^c$, étendant les résultats connus pour les modèles nets.
• Résultats de complexité : La validité de GW est établie comme étant PSPACE-complète. La borne inférieure provient de l'inclusion de K, et la borne supérieure est dérivée de la procédure PSPACE pour l'existence de contre-modèles.
• Implémentation : Un prototype de prouveur nommé gwref est implémenté, utilisant le moteur JTabWb et le solveur Choco pour les vérifications de cohérence des contraintes.

Résultats

• Correction et Complétude : CGW est prouvé sain et complet par rapport aux modèles GW. Une formule $\phi$ est valide dans GW si et seulement si l'ensemble de contraintes $\{w : \phi < 1\}$ n'est pas prouvable dans CGW.
• Terminaison : Le calcul est fortement terminable. Une relation bien ordonnée sur les multisets de contraintes garantit que toute recherche de preuve par rétroaction s'arrête.
• Extraction de contre-modèle : Lorsque la recherche de preuve échoue, la procédure construit un contre-modèle discret dont la taille est bornée par $O(|\phi|^{| \phi |})$.
• Hiérarchie Logique : Le papier clarifie les relations entre diverses logiques : $GK \subset G^c \subset GW^c$ et $GK \subset GW \subset GW^c$. Il montre que l'axiome « Net » (valide dans $G^c$) n'est pas valide dans $GW$, et que l'axiome « Témoin » ($\Box\neg\neg\alpha \to \neg\neg\Box\alpha$) est valide dans $GW$ mais pas dans $G^c$.

Signification
Le papier soutient que la sémantique avec témoins offre un moyen principalisé de surmonter les difficultés associées aux phénomènes de base limite dans les logiques modales floues. En garantissant que les comportements existentiels et universels sont soutenus par des témoins explicites, la sémantique de GW ressemble davantage à la quantification gardée de la logique du premier ordre et restaure une lecture constructive.

La signification de ce travail réside dans :

1. Restauration des propriétés constructives : La FMP et les résultats de décidabilité font de GW un outil adapté au raisonnement automatisé, permettant de remplacer les arguments sémantiques infinitaires par des arguments combinatoires finis.
2. Alignement de la théorie de la preuve : La sémantique avec témoins s'aligne plus étroitement avec les calculs syntaxiques, facilitant les constructions de modèles canoniques et les preuves de complétude standard.
3. Connexions avec les logiques intermédiaires : Les résultats sont positionnés comme pertinents pour l'étude des logiques de prédicats intermédiaires, suggérant des connexions profondes avec des propriétés telles que le théorème de Herbrand et l'interpolation dans les fragments à une variable des logiques de prédicats intuitionnistes.
4. Applicabilité pratique : Le développement d'une procédure de recherche de preuve qui se termine avec génération de contre-modèle offre un outil pratique pour vérifier les propriétés dans les systèmes impliquant l'incertitude graduée, la représentation des connaissances et les systèmes multi-agents.

Les auteurs notent que si l'approche fonctionne bien pour les modèles avec témoins, traiter les logiques modales de Gödel avec des modèles sans témoins reste un problème ouvert nettement plus difficile. Les travaux futurs incluent l'extension de la procédure à d'autres logiques avec témoins possédant des contraintes de cadre supplémentaires (réflexivité, transitivité) et le développement d'une sémantique de Kripke birélationnelle pour GW.