Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA

Informations de base

• ID de l'article: 2507.11643
• Titre: Notes on the equiconsistency of ZFC without the Power Set axiom and second order PA
• Auteurs: Vladimir Kanovei, Vassily Lyubetsky
• Classification: math.LO (Logique mathématique)
• Date de publication: 13 octobre 2025
• Lien de l'article: https://arxiv.org/abs/2507.11643

Résumé

Cet article démontre l'équicohérence entre les théories Z⁻, ZF⁻, ZFC⁻ (le tiret indiquant l'absence de l'axiome de l'ensemble des parties) et PA₂, PA₂⁻ (le tiret indiquant l'absence du schéma de choix dénombrable). Les méthodes utilisées incluent l'interprétation de la théorie des ensembles sans axiome de l'ensemble des parties dans PA₂⁻ via des arbres bien fondés, ainsi que l'utilisation de la constructibilité de Gödel dans la théorie des ensembles sans axiome de l'ensemble des parties.

Contexte et motivation de la recherche

Problème central

Cet article vise à résoudre une question fondamentale de logique mathématique : démontrer les relations d'équicohérence entre plusieurs systèmes théoriques mathématiques importants. Spécifiquement, il s'agit d'établir l'équicohérence entre :

• Les systèmes de théorie des ensembles sans axiome de l'ensemble des parties : Z⁻, ZF⁻, ZFC⁻
• Les systèmes d'arithmétique du second ordre : PA₂, PA₂⁻

Importance du problème

1. Relations entre théories mathématiques fondamentales : Ces théories constituent des fondements importants des mathématiques modernes, et la compréhension de leurs relations logiques revêt une importance fondamentale pour la recherche en fondements mathématiques
2. Position centrale du problème de cohérence : En logique mathématique, la cohérence d'une théorie est sa propriété la plus fondamentale, et les relations d'équicohérence révèlent la force relative de différents systèmes théoriques
3. Signification historique : Ce résultat est connu depuis au moins la fin des années 1960, mais il manquait une preuve complète et autonome

Limitations des approches existantes

Les auteurs soulignent que, bien que ce théorème soit connu depuis au moins la fin des années 1960, aucune preuve autonome et relativement complète n'a apparemment jamais été publiée. C'est précisément la motivation principale de cet article : fournir une telle preuve complète.

Contributions essentielles

1. Fourniture d'une preuve complète : Première preuve autonome et complète du théorème 1.1 (résultat principal d'équicohérence)
2. Construction d'une théorie intermédiaire TMC : Introduction d'une théorie intermédiaire TMC qui étend Z⁻ et contient trois axiomes supplémentaires
3. Établissement de relations d'interprétation : Interprétation de TMC dans PA₂⁻ via des structures d'arbres bien fondés, interprétation de ZFC⁻ dans PA₂
4. Application de la constructibilité de Gödel : Développement de la théorie de la constructibilité dans le cadre TMC, établissement de l'interprétation de ZFC⁻ dans TMC
5. Fourniture de modèles concrets : Construction de l'ensemble ou de la classe L* spécifique satisfaisant ZFC⁻

Explication détaillée des méthodes

Définition des tâches

Démontrer l'équicohérence des théories suivantes :

• Théories d'entrée : PA₂⁻, PA₂, Z⁻, ZFC⁻, ZF⁻
• Résultat : Établir les relations d'interprétation mutuelle entre ces théories
• Contraintes : La preuve doit être autonome et ne pas dépendre de résultats non publiés

Architecture centrale

Première partie : Interprétation par structures d'arbres

1. Définition de la structure V : Définition dans PA₂⁻ de la structure V = ⟨WFT; ∼=, ∼∈⟩, où :
   • WFT est l'ensemble de tous les arbres bien fondés T ⊆ ω<ω
   • ∼= est la relation d'équivalence de bisimulation entre arbres
   • ∼∈ est la relation d'appartenance définie sur la base de ∼=
2. Établissement de l'interprétation :
   • Le théorème 5.2 démontre que V satisfait TMC sous PA₂⁻
   • V satisfait ZFC⁻ sous PA₂

Deuxième partie : Approche par constructibilité

1. Théorie intermédiaire TMC : Contient trois axiomes clés
   • Axiome des surensembles transitifs (TrSups) : Chaque ensemble possède un surensemble transitif
   • Axiome d'effondrement de Mostowski (MostColl) : Chaque relation bien fondée admet un modèle transitif
   • Axiome de dénombrabilité (Countability) : Tous les ensembles sont au plus dénombrables
2. Hiérarchie constructible : Développement de la hiérarchie constructible de Gödel dans TMC :

   L₀[u] = ω ∪ {u}
   Lₐ₊₁[u] = Def Lₐ[u]
   Lλ[u] = ⋃ₐ<λ Lₐ[u]
   L[u] = ⋃ₐ∈Ord Lₐ[u]
   

Points d'innovation technique

Théorème clé 8.6

Sous la condition F(u,Ω,K), l'ensemble K satisfait ZFC⁻, où F(u,Ω,K) définit deux cas :

• Cas A : Ω = Ord, K = Lu, et ω₁^Lu n'existe pas
• Cas B : Ω = ω₁^Lu existe, K = L_Ωu

Théorème technique principal 1.2

L* = {
  L,                    si ω₁^L n'existe pas
  L_Ω = ⋃ₐ<Ω Lₐ,      si ω₁^L = Ω existe
}

Cet ensemble ou cette classe satisfait ZFC⁻.

Configuration expérimentale

Vérification du cadre théorique

Cet article est un travail mathématique purement théorique qui n'implique pas d'expériences au sens traditionnel. Les méthodes de vérification incluent :

1. Vérification par raisonnement logique : Chaque théorème est vérifié par une preuve mathématique rigoureuse
2. Vérification de cohérence : Assurance de la cohérence interne de chaque système théorique
3. Vérification des relations d'interprétation : Vérification que les relations d'interprétation établies préservent effectivement les axiomes et les règles d'inférence des théories

Méthodes comparatives

• Approche de Simpson : Les auteurs comparent les différences et similitudes avec les interprétations connexes dans Simpson 30, VII.4
• Approches antérieures : Examen des méthodes d'interprétation antérieures définies dans 17
• Autres modèles : Discussion de trois autres modèles de ZFC⁻ à la section 13

Résultats principaux

Théorème central

Théorème 1.1 : Les théories PA₂⁻, PA₂, Z⁻, ZFC⁻, ZF⁻ sont équicohérentes.

Résultats intermédiaires clés

Théorème 5.2 (Théorème d'interprétation)

Dans le cadre PA₂⁻/PA₂, la structure V est bien définie, et V satisfait respectivement TMC/ZFC⁻.

Théorème 1.3 (Résultat de constructibilité)

Sous TMC :

1. L ∩ P(ω) satisfait PA₂
2. L lui-même satisfait l'axiome de séparation

Corollaire 12.1

Sous PA₂⁻, L ∩ P(ω) satisfait PA₂, ce qui fournit une interprétation de PA₂ dans PA₂⁻.

Travaux connexes

Développement historique

• Fin des années 1960 : Ce résultat a d'abord été découvert (comme mentionné dans 24)
• Kreisel 24 : Travaux connexes antérieurs
• Simpson 30 : Résultats connexes dans le cadre de la théorie ATR₀^set
• Série de travaux de Marek : Techniques connexes dans 26, 27

Relation entre cet article et les travaux connexes

1. Complétude : Première preuve complètement autonome
2. Unification des méthodes : Combinaison organique de la méthode d'interprétation par arbres et de la méthode de constructibilité
3. Améliorations techniques : Simplification de certains détails techniques dans le cadre TMC

Conclusions et discussion

Conclusions principales

1. Établissement réussi des relations d'équicohérence entre cinq théories mathématiques importantes
2. Fourniture d'une méthode de preuve complète et autonome
3. Démonstration de la combinaison efficace des méthodes d'interprétation par arbres et de constructibilité

Limitations

1. Problèmes ouverts : Les auteurs se demandent s'il existe une méthode d'interprétation de PA₂ dans PA₂⁻ qui évite l'utilisation extensive de concepts de théorie des ensembles
2. Complexité technique : La preuve implique plusieurs étapes techniques complexes avec un seuil de compréhension élevé
3. Portée des applications : Principalement des résultats de théorie fondamentale, avec des applications directes limitées

Directions futures

Problème 15.1

Concernant l'indépendance de l'axiome TrSups par rapport aux autres axiomes de TMC.

Problème 15.2

Recherche d'une preuve purement analytique du théorème 14.3 dans PA₂⁻, sans impliquer explicitement ou implicitement V ou des structures de théorie des ensembles dérivées similaires.

Perspectives d'application

Les auteurs espèrent que cette méthode pourrait être utilisée pour renforcer les applications récentes de la méthode de forçage de Cohen en théorie des ensembles dans les théories ZFC⁻ et PA₂.

Évaluation approfondie

Avantages

1. Complétude théorique : Comble une lacune de preuve longtemps existante dans ce domaine
2. Innovation méthodologique : Combinaison ingénieuse de deux méthodes classiques : l'interprétation par arbres et la constructibilité
3. Profondeur technique : Démontre une maîtrise profonde des techniques de logique mathématique
4. Clarté de la rédaction : Malgré la complexité technique, la structure organisationnelle est claire et facilite la compréhension

Insuffisances

1. Seuil technique élevé : Nécessite une formation approfondie en logique mathématique pour une compréhension complète
2. Utilité pratique limitée : Principalement une contribution théorique avec des scénarios d'application directe limités
3. Certains détails de preuve : Certaines preuves (comme le théorème 1.3(II)) ne sont que partiellement détaillées

Influence

1. Contribution à la théorie fondamentale : Fournit des outils théoriques importants pour la recherche en fondements mathématiques
2. Valeur méthodologique : Les techniques présentées peuvent s'appliquer à d'autres problèmes connexes
3. Valeur pédagogique : Peut servir de référence importante pour les cours avancés de logique mathématique

Scénarios d'application

1. Recherche en fondements mathématiques : Fournit des outils pour étudier les relations entre différents systèmes théoriques mathématiques
2. Recherche en logique : Soutien technique pour la recherche en théorie des modèles et théorie de la preuve
3. Fondements de l'informatique : Fournit des bases théoriques pour la théorie des types et la sémantique des langages de programmation

Références

L'article contient 35 références, couvrant les travaux classiques de Gödel et Kleene jusqu'aux recherches récentes sur les méthodes de forçage en théorie des ensembles, reflétant l'évolution historique et les progrès récents du domaine.

Évaluation globale : Ceci est un article de logique mathématique de haute qualité qui résout avec succès un problème important longtemps existant. Bien que le seuil technique soit élevé, sa contribution théorique et sa valeur méthodologique en font une littérature importante dans ce domaine.