Modèles de Prouvabilité

Informations Fondamentales

• ID de l'article : 2510.06696
• Titre : Provability Models
• Auteurs : Mojtaba Mojtahedi (Université de Gand), Borja Sierra Miranda (Université de Berne)
• Classification : math.LO (Logique Mathématique)
• Date de publication : 15 octobre 2025
• Lien de l'article : https://arxiv.org/abs/2510.06696

Résumé

Cet article étudie une nouvelle sémantique de type Kripke — les modèles de prouvabilité (provability models) — pour la logique modale classique. L'étude couvre les modèles de prouvabilité pour les logiques modales propositionnelles K, K4, S4, GL, GLP ainsi que pour la logique d'interprétabilité ILM. Les modèles de prouvabilité combinent les caractéristiques des modèles de Kripke avec l'approche consistant à assigner une logique à chaque monde individuel. Ce modèle a été initialement introduit par Mojtahedi en 2022 pour établir la complétude arithmétique de la logique de prouvabilité intuitionniste. Fait intéressant, cet article démontre que ILM est complet pour les mêmes modèles de prouvabilité que GL. Dans le cas de GL et ILM, l'article améliore les modèles de prouvabilité en modèles de prouvabilité prévisibles et décidables, et démontre la solidité et la complétude de GLP pour les modèles de prouvabilité.

Contexte et Motivation de la Recherche

Problème Central

Dans la recherche traditionnelle sur la logique de prouvabilité, l'opérateur modal est généralement interprété comme un prédicat de prouvabilité dans un système arithmétique du premier ordre ou une théorie des ensembles. Cependant, on peut également interpréter □A comme L ⊢ A (pour une théorie propositionnelle donnée L). Bien que pour toute logique L contenant GL, on puisse démontrer que GL est solide pour l'interprétation L, aucune interprétation L ne peut fournir la complétude de GL.

Importance du Problème

Cet échec contraste avec l'interprétation PA, provenant principalement du fait que la logique L ne peut pas simuler les modèles de Kripke, tandis que l'arithmétique de Peano peut exploiter sa capacité à simuler les modèles de Kripke (comme l'a démontré Solovay). Par conséquent, on ne peut pas s'attendre à ce que GL soit la logique de prouvabilité d'une seule logique propositionnelle.

Limitations des Approches Existantes

1. Restrictions des modèles de Kripke standards : incapacité à traiter directement les interprétations arithmétiques de la logique de prouvabilité
2. Incomplétude des interprétations propositionnelles de prouvabilité : une seule logique propositionnelle ne peut pas fournir la complétude de GL
3. Propriétés de cadre complexes : les propriétés de cadre complexes dans la sémantique d'Iemhoff rendent difficile l'établissement de théorèmes de complétude arithmétique

Motivation de la Recherche

Cet article comble cette limitation en intégrant explicitement les cadres de Kripke dans la logique propositionnelle, en considérant les modèles de Kripke standards où chaque monde w est équipé d'une logique Lw, et en imposant des relations d'accessibilité entre ces théories basées sur la relation d'accessibilité sous-jacente.

Contributions Principales

1. Proposition du cadre des modèles de prouvabilité : introduction d'une nouvelle sémantique de style Kripke pour la logique modale classique
2. Établissement de la complétude pour plusieurs logiques modales : démonstration de la solidité et de la complétude de K, K4, S4, GL pour les modèles de prouvabilité
3. Construction de modèles de prouvabilité indépendants : en particulier pour GL et ILM, démonstration de la construction de modèles de prouvabilité indépendants des modèles de Kripke standards
4. Réalisation de la décidabilité : dans le cas de GL et ILM, construction de modèles de prouvabilité décidables
5. Extension à la logique multimodale : démonstration de la solidité et de la complétude de GLP (logique de prouvabilité multimodale) pour les modèles de prouvabilité
6. Établissement de la complétude de ILM : démonstration que la logique d'interprétabilité ILM est complète pour les mêmes modèles de prouvabilité que GL

Détails Méthodologiques

Définition de la Tâche

Étude des modèles de prouvabilité en tant que sémantique pour la logique modale, où :

• Entrée : formule modale et modèle de prouvabilité
• Sortie : jugement de validité de la formule dans le modèle
• Contraintes : le modèle doit satisfaire des propriétés logiques spécifiques et des conditions de cadre

Architecture du Modèle

Définition du Prémodèle de Prouvabilité

Un prémodèle de prouvabilité P = (W, <, {Lw}w∈W, V) contient :

• W : ensemble non vide de mondes
• < : relation binaire sur W
• Lw : logique pour chaque monde <-accessible w
• V : relation d'assignation pour les propositions atomiques

Définition de la Validité

Pour une formule A, on définit P, w |= A par induction :

• Commute avec les connecteurs booléens
• P, w |= □A si et seulement si ∀u ⪯ w (⊢u A)

Conditions du Modèle de Prouvabilité

Un prémodèle de prouvabilité devient un modèle de prouvabilité s'il satisfait :

• Complétude modale : pour chaque formule purement modale A, si P, w |=+ A alors ⊢w A

Points d'Innovation Technique

1. Logicalisation des Conditions de Cadre

Les modèles de prouvabilité peuvent absorber les conditions de cadre comme règles d'inférence des logiques assignées aux mondes individuels :

• La transitivité peut être remplacée par une règle de nécessitation
• La bien-fondation inverse peut être remplacée par la règle de Löb

2. Approche Constructive

Pour GL et ILM, fourniture de méthodes constructives pour construire des modèles de prouvabilité :

Théorème 4.4 : Pour chaque prémodèle de prouvabilité d'arbre bien-fondé inverse P, il existe un modèle de prouvabilité P̄ avec nécessitation, tel que :

• P̄ possède la nécessitation
• P ⊆ P̄
• P̄ est le modèle de prouvabilité minimal contenant P

3. Garantie de Décidabilité

Si P est bifinite, alors P̄ est décidable, où bifinite signifie que W et Axiom(Lw) pour chaque w∈W sont finis.

Configuration Expérimentale

Cadre de Vérification Théorique

Cet article procède principalement par preuve théorique, le cadre de vérification incluant :

1. Preuve de Solidité

Pour diverses logiques modales, démonstration que si logique ⊢ A, alors P |= A pour tous les modèles de prouvabilité correspondants P.

2. Preuve de Complétude

Démonstration que si P |= A pour tous les modèles de prouvabilité correspondants P, alors logique ⊢ A.

3. Complétude Forte

Particulièrement pour GL, démonstration de la complétude forte : Γ |=P A implique Γ ⊢GL A.

Vérification des Méthodes de Construction

Vérification par construction concrète de :

• Existence de modèles de prouvabilité finis
• Réalisation de la décidabilité
• Indépendance (non-dépendance des modèles de Kripke standards)

Résultats Expérimentaux

Résultats Principaux

1. Complétude des Logiques Modales Fondamentales

• K : solide et complet pour les modèles de prouvabilité (Théorèmes 3.6, 3.7)
• K4 : solide et complet pour les modèles de prouvabilité avec nécessitation ou transitivité (Théorèmes 3.8, 3.9)
• S4 : solide et complet pour les modèles de prouvabilité réflexifs, transitifs, avec nécessitation et complétude locale (Théorèmes 3.11, 3.12)

2. Résultats pour la Logique de Prouvabilité GL

• Solidité : GL est solide pour les modèles de prouvabilité bien-fondés inverses avec nécessitation et règle de Löb (Théorème 3.14)
• Complétude : GL est complet pour les modèles de prouvabilité finis, transitifs et non-réflexifs (Théorème 3.17)
• Complétude Forte : GL est fortement complet pour les modèles de prouvabilité avec nécessitation et règle de Löb (Théorème 3.18)
• Complétude Finitaire : GL est complet pour les modèles de prouvabilité finitaires (Théorème 4.6)

3. Résultats pour la Logique d'Interprétabilité ILM

• Solidité : ILM est solide pour les modèles de prouvabilité bien-fondés inverses avec nécessitation (Théorème 5.6)
• Complétude : ILM est complet pour les modèles de prouvabilité d'arbre bien-fondé inverse finis avec nécessitation (Théorème 5.10)
• Complétude Finitaire : ILM est complet pour les modèles de prouvabilité finitaires (Théorème 5.13)

4. Résultats pour la Logique Multimodale de Prouvabilité GLP

• Solidité et Complétude : GLP est solide et fortement complet pour les modèles GLP-multiprouvabilité (Théorèmes 6.2, 6.3)

Résultats Constructifs

Construction réussie de modèles de prouvabilité indépendants des modèles de Kripke standards, en particulier :

• Pour tout cadre d'arbre bien-fondé inverse et toute assignation d'ensemble de formules aux nœuds, on peut construire le modèle de prouvabilité minimal
• Dans le cas bifinite, le modèle construit est décidable

Travaux Connexes

Recherche Traditionnelle en Logique de Prouvabilité

• Solovay (1976) : établissement de la logique de prouvabilité de PA
• Boolos (1995), Smoryński (1985) : manuels classiques de logique de prouvabilité
• Artemov et Beklemishev (2004) : enquête synthétique

Approches Sémantiques

• Sémantique de Kripke standard : utilisée pour diverses logiques modales
• Modèles de Veltman : utilisés pour la logique d'interprétabilité ILM
• Sémantique topologique : fournit la complétude pour GLP

Logique de Prouvabilité Intuitionniste

• Iemhoff (2001-2003) : introduction de la sémantique d'Iemhoff
• Mojtahedi (2022) : première utilisation des modèles de prouvabilité pour établir la complétude arithmétique de la logique de prouvabilité intuitionniste

Conclusion et Discussion

Conclusions Principales

1. Cadre Unifié : les modèles de prouvabilité fournissent un cadre sémantique unifié pour plusieurs logiques modales
2. Constructivité : particulièrement pour GL et ILM, on peut construire de manière constructive des modèles de prouvabilité indépendants
3. Décidabilité : dans les conditions appropriées, les modèles de prouvabilité sont décidables
4. Flexibilité : les conditions de cadre peuvent être remplacées par des propriétés logiques, offrant une plus grande flexibilité

Limitations

1. Restrictions pour GLP : pour GLP, on n'a pas encore trouvé de classe de modèles de prouvabilité décidables
2. Complexité des Constructions : certaines constructions (comme le modèle canonique pour GLP) peuvent ne pas être constructives
3. Portée d'Application : s'applique principalement aux logiques avec propriétés de prouvabilité

Directions Futures

L'article énonce explicitement plusieurs problèmes ouverts :

1. Extensions de Logiques de Preuve : définition de modèles de style prouvabilité pour la logique de preuve LP et JGL
2. Logique Modale Intuitionniste : définition de modèles de prouvabilité pour la logique modale intuitionniste avec deux opérateurs modaux □ et ◇
3. Modèles Décidables pour GLP : recherche de classes de modèles de prouvabilité décidables pour GLP
4. Simplification de la Complétude Arithmétique : exploration de la possibilité de simplifier la preuve de complétude arithmétique de ILM via les modèles de prouvabilité

Évaluation Approfondie

Points Forts

1. Innovation Théorique : proposition d'un nouveau cadre sémantique unifiant le traitement de plusieurs logiques modales
2. Profondeur Technique : fourniture de preuves mathématiques détaillées et de méthodes de construction
3. Valeur Pratique : les améliorations en matière de décidabilité sont particulièrement significatives
4. Systématicité : traitement systématique allant des logiques modales fondamentales aux logiques de prouvabilité complexes

Insuffisances

1. Complexité : la complexité de certaines constructions (particulièrement pour GLP) peut limiter les applications pratiques
2. Problèmes Ouverts : des problèmes importants restent non résolus, comme les modèles décidables pour GLP
3. Portée d'Application : principalement limitée à la recherche théorique, la valeur pratique reste à explorer davantage

Impact

1. Contribution Théorique : fourniture d'une nouvelle direction de recherche pour la sémantique de la logique modale
2. Valeur Méthodologique : la méthode de logicalisation des conditions de cadre a une portée universelle
3. Recherches Ultérieures : fourniture de nouveaux outils pour la recherche en logique intuitionniste, logique de preuve, etc.

Scénarios d'Application

1. Recherche en Logique de Prouvabilité : particulièrement adaptée à la recherche nécessitant la complétude arithmétique
2. Sémantique de la Logique Modale : fournit de nouvelles méthodes sémantiques pour les logiques modales complexes
3. Logique Computationnelle : valeur potentielle dans les applications nécessitant la décidabilité

Références Bibliographiques

L'article cite une riche littérature connexe, incluant :

• Littérature classique en logique de prouvabilité (Boolos, Smoryński, Solovay, etc.)
• Travaux importants en sémantique de la logique modale (Blackburn, etc.)
• Recherches clés en logique d'interprétabilité (Berarducci, Shavrukov, etc.)
• Travaux connexes en logique de prouvabilité intuitionniste (Iemhoff, etc.)

Cet article apporte une contribution théorique importante au domaine de la sémantique de la logique modale, fournissant un nouveau cadre unifié pour traiter diverses logiques de prouvabilité, tout en réalisant des progrès significatifs en constructivité et décidabilité. Bien que certains problèmes ouverts subsistent, ce travail jette les bases solides pour les recherches ultérieures.