Iterating reflection over intuitionistic arithmetic

Cet article examine les itérations de la consistance et des principes de réflexion locale et uniforme sur l'arithmétique intuitionniste (HA), en fournissant une nouvelle preuve de l'extension par Dragalin du théorème de complétude de Feferman à HA.

L'essentiel

🧠 L'Exploration de l'Infini : Une Aventure en Mathématiques Intuitionnistes

Imaginez que les mathématiques sont une immense bibliothèque. Dans cette bibliothèque, il y a deux grands types de règles pour écrire des livres (des preuves) :

1. Les règles classiques (PA) : C'est comme si l'on disait : « Tout est soit vrai, soit faux. S'il n'y a pas de preuve du contraire, alors c'est faux. » C'est la logique habituelle.
2. Les règles intuitionnistes (HA) : C'est plus strict. Ici, on dit : « Pour dire qu'une chose est vraie, il faut pouvoir la construire ou la démontrer concrètement. On ne peut pas simplement dire "ce n'est pas faux". » C'est comme si l'on exigeait un plan d'architecte solide avant de construire une maison.

L'auteur de ce papier, Emanuele Frittaion, s'intéresse à cette deuxième bibliothèque (l'arithmétique de Heyting, ou HA). Il veut savoir : jusqu'où peut-on aller si l'on ajoute continuellement de nouvelles règles de vérification ?

🔄 Le concept de "Miroir" (La Réflexion)

Imaginez que votre bibliothèque a un miroir magique.

• La cohérence (Consistency) : Le miroir vous dit : « Je ne vois aucune contradiction dans mes livres. »
• La réflexion locale (Local Reflection) : Le miroir vous dit : « Si un livre dit "X est prouvé", alors X est vrai. »
• La réflexion uniforme (Uniform Reflection) : C'est le miroir ultime. Il dit : « Pour n'importe quelle phrase, si je dis qu'elle est prouvable, alors elle est vraie. »

L'idée du papier est de répéter ce processus à l'infini.

1. On commence avec la bibliothèque de base (HA).
2. On ajoute le miroir (on ajoute la règle "si prouvable, alors vrai").
3. On prend la nouvelle bibliothèque, on ajoute un nouveau miroir encore plus puissant.
4. On recommence encore et encore, en suivant une échelle infinie appelée O de Kleene (une sorte de compteur d'ordres infinis).

🏆 Le Grand Défi : Le Théorème de Dragalin

Dans le monde classique (PA), on savait déjà que si l'on répétait ce processus de miroir assez longtemps, on finissait par pouvoir prouver toutes les vérités mathématiques. C'est le théorème de complétude de Feferman.

Mais dans le monde intuitionniste (HA), c'était un mystère. Les mathématiciens se demandaient : « Si on fait la même chose avec les règles strictes, arrive-t-on aussi à tout prouver ? »

La réponse de Frittaion est OUI.
Il prouve que si l'on itère (répète) la réflexion uniforme sur HA, on obtient exactement la même puissance que si l'on avait ajouté une règle magique appelée la règle ω récursive.

L'analogie de la règle ω :
Imaginez que vous voulez prouver une phrase comme « Tous les nombres entiers ont la propriété P ».

• Méthode classique : Vous pouvez dire « C'est vrai » sans vérifier un par un, en utilisant des raccourcis logiques.
• Méthode ω (récursive) : Pour prouver que c'est vrai, vous devez être capable de vérifier chaque nombre un par un (0, 1, 2, 3...) de manière mécanique et infinie. C'est une tâche énorme, presque impossible à faire à la main, mais théoriquement possible.

Frittaion montre que répéter le processus de "vérification de la vérification" (réflexion uniforme) revient exactement à avoir cette capacité de vérifier chaque nombre un par un.

🛠️ Comment a-t-il fait ? (L'astuce de l'ingénieur)

Le problème, c'est que les preuves classiques utilisaient des astuces qui ne fonctionnent pas dans le monde strict de l'intuitionnisme (comme le principe du "tiers exclu").

Frittaion a utilisé une nouvelle méthode, inspirée par Rathjen, qui ressemble à la construction d'un arbre généalogique infini :

1. Il imagine un arbre où chaque branche représente une tentative de preuve.
2. Il construit cet arbre de manière mécanique (récursive).
3. Si l'arbre est "correct" (il ne contient pas de boucles infinies inutiles), alors la phrase est prouvée.
4. L'astuce géniale est d'utiliser un théorème de Löb (une sorte de "miroir qui se regarde lui-même") pour prouver, à l'intérieur même du système, que cet arbre fonctionne, sans avoir besoin de sortir du système pour regarder de l'extérieur.

C'est comme si un architecte pouvait prouver que son immeuble est solide en utilisant uniquement les briques de l'immeuble lui-même, sans avoir besoin d'un ingénieur extérieur.

💡 Pourquoi est-ce important ?

Ce papier répond à une question fondamentale : Quelle est la limite de la logique constructive ?
Il montre que même avec des règles très strictes (intuitionnistes), si l'on accepte de vérifier les preuves de manière infinie et itérative, on ne perd pas de puissance par rapport aux règles classiques. On arrive au même but, mais par un chemin plus rigoureux.

Il y a aussi une petite surprise : le papier montre que certaines règles "magiques" (comme le principe de Markov) ne peuvent pas être prouvées simplement en répétant ce processus de miroir. Cela nous dit qu'il y a des vérités qui échappent à cette méthode d'itération, ce qui ouvre de nouvelles questions pour les mathématiciens.

En résumé

Ce papier est une victoire de la logique rigoureuse. Il nous dit que si l'on prend le système de logique le plus strict (HA) et qu'on lui donne une machine à "vérifier les vérifications" qui tourne à l'infini, on finit par pouvoir prouver tout ce qui est vrai, exactement comme dans le système classique, mais sans jamais tricher avec des hypothèses non prouvées. C'est une démonstration magnifique de la puissance de la logique constructive.

Résumé technique

Voici un résumé technique détaillé du papier « Iterating Reflection over Intuitionistic Arithmetic » d'Emanuele Frittaion, rédigé en français.

Titre : Itération de la réflexion sur l'arithmétique intuitionniste

Auteur : Emanuele Frittaion
Sujet : Logique mathématique, Théorie de la preuve, Arithmétique intuitionniste (HA).

---

1. Problématique et Contexte

Le papier s'inscrit dans le cadre de l'étude des progressions récursives transfinies de théories, un concept introduit par Turing et développé par Feferman. L'objectif est d'itérer des principes de réflexion (consistance, réflexion locale, réflexion uniforme) le long des notations d'ordinaux de Kleene ($O$) pour capturer la vérité arithmétique.

• Contexte Classique (PA) : Feferman a démontré que l'itération de la réflexion uniforme sur l'arithmétique de Peano (PA) permet de prouver toutes les sentences vraies de l'arithmétique (Théorème de complétude de Feferman). En revanche, l'itération de la consistance ou de la réflexion locale ne capture que les sentences $\Pi_1$ vraies.
• Problème Intuitionniste (HA) : La question centrale est de savoir si ces résultats se généralisent à l'arithmétique de Heyting (HA), qui est basée sur la logique intuitionniste.
  • Le défi majeur réside dans le fait que les preuves classiques de Feferman reposent crucialement sur le principe du tiers exclu pour les formules $\Sigma_1$ ($\Sigma_1$-LEM), qui n'est pas valide en logique intuitionniste.
  • Dragalin a énoncé un théorème analogue pour HA (théorème 1.3), affirmant que l'itération de la réflexion uniforme sur HA correspond à l'ajout de la règle $\omega$ récursive, mais sa preuve n'était qu'une ébauche.
  • Une question ouverte majeure est de savoir si la règle $\omega$ récursive intuitionniste est complète pour la vérité arithmétique, ou si elle est strictement plus faible que la règle $\omega$ complète (non constructive).

2. Méthodologie

L'auteur propose une nouvelle preuve complète et autonome du théorème de Dragalin, en s'appuyant sur la méthode de Rathjen pour le cas classique, mais adaptée à la logique intuitionniste.

• Cadre Formel : Le travail se déroule entièrement dans HA (ou ses extensions récursivement énumérables). L'auteur utilise une arithmétisation standard des formules et des preuves.
• Outils Techniques Clés :
  1. Arbres de recherche canoniques (Schütte) : Pour chaque nombre $a$, l'auteur construit un arbre primitif récursif $S(a)$. Dans le cas classique, cet arbre est une preuve $\omega$ de $\phi$ si et seulement si $\phi$ est vrai. En intuitionnisme, la construction est modifiée : $S(a)$ est une preuve $\omega$ intuitionniste (avec répétitions possibles) de $\phi$ si et seulement si $a$ code une telle preuve.
  2. Théorème de Löb restreint : Bien que le théorème de Löb ne tienne pas globalement en HA, sa restriction aux formules $\Pi_2$ est valide. L'auteur exploite cette restriction pour formaliser des arguments d'induction sur les notations d'ordinaux de Kleene à l'intérieur de HA, évitant ainsi de devoir effectuer l'induction métathéorique sur $O$.
  3. Règle $\omega$ récursive : Définition d'un système de preuve $P$ où les règles d'inférence sont restreintes aux fonctions récursives totales (via les indices de Kleene).

3. Contributions et Résultats Principaux

Le papier établit les équivalences suivantes pour HA (et ses extensions r.e.) :

A. Réflexion Uniforme et Règle $\omega$ Récursive (Théorème 4.2)

C'est le résultat central. L'auteur prouve que :

Une formule $\phi$ est prouvable dans une itération de la réflexion uniforme sur HA si et seulement si $\phi$ possède une preuve dans le système de la règle $\omega$ récursive (noté $P$).

• Implication (1) $\Rightarrow$ (2) : Si $\phi$ est prouvable par itération, on peut construire effectivement une preuve dans $P$ en utilisant le théorème de récursion pour trouver un indice de fonction.
• Implication (2) $\Rightarrow$ (1) : C'est la partie difficile. L'auteur définit une fonction récursive totale $g$ (via le théorème de récursion) qui mappe une preuve $a \in P$ vers une notation d'ordinal $g(a) \in O$. Il montre que dans HA, si $a$ est une preuve de $\phi$ dans $P$, alors la théorie $T_{g(a)}$ (l'étape $g(a)$ de la progression) prouve $\phi$.
  • La preuve utilise une induction structurelle sur la preuve $a$ et le théorème de Löb pour gérer les cas limites et les répétitions dans les arbres de preuve.

B. Consistance et Réflexion Locale (Théorème 3.1)

L'auteur confirme que, comme dans le cas classique, l'itération de la consistance ou de la réflexion locale sur HA ne capture que les sentences $\Pi_1$ vraies :

Les sentences prouvables par itération de la consistance ou de la réflexion locale sur HA sont exactement celles prouvables dans HA + toutes les sentences $\Pi_1$ vraies.

• La preuve montre que l'utilisation du tiers exclu dans la preuve classique de Feferman peut être évitée pour ce résultat spécifique, bien que l'auteur note que la preuve utilise le principe d'explosion (ex falso quodlibet), ce qui pose la question de la validité en logique minimale.

C. Caractérisation de la Réalisabilité (Discussion et Théorème 1.9)

Le papier discute la relation entre la réalisabilité de Kleene et la réflexion itérée :

• Il est rappelé que les sentences prouvables par itération de réflexion uniforme sur HA sont réalisables.
• Cependant, l'inverse n'est pas vrai : le principe de Markov (MP) est une sentence vraie et réalisable, mais elle n'est pas prouvable par itération de réflexion uniforme sur HA.
• Cela implique que la règle $\omega$ récursive intuitionniste est strictement plus faible que la règle $\omega$ complète (qui prouve MP).
• L'auteur conclut qu'aucune notion de "vérité" compositionnelle ne peut rendre ces itérations complètes pour HA, car la fermeture de HA sous la règle de Markov dépasse la puissance de la réflexion itérée.

4. Signification et Implications

1. Résolution d'un problème ouvert : Le papier fournit la première preuve complète et détaillée du théorème de Dragalin, comblant un vide laissé par les ébauches antérieures.
2. Compréhension de la logique intuitionniste : Il met en lumière les limites de la logique intuitionniste par rapport à la logique classique dans le contexte des progressions transfinies. La nécessité de la règle $\omega$ récursive (et non complète) pour capturer la réflexion uniforme montre une différence fondamentale de puissance expressive.
3. Méthodologie innovante : L'utilisation combinée des arbres de recherche de Schütte et du théorème de Löb restreint pour formaliser l'induction sur les ordinaux dans HA est une contribution méthodologique importante. Cela permet de contourner les obstacles liés à l'absence de $\Sigma_1$-LEM.
4. Limites de la réalisabilité : La démonstration que MP n'est pas dérivable par réflexion itérée sur HA (bien que réalisable) fournit un contre-exemple clair aux tentatives de caractériser la vérité intuitionniste par de simples principes de réflexion itérée.

En résumé, ce papier établit une correspondance précise entre les principes de réflexion itérée et la règle $\omega$ récursive en arithmétique intuitionniste, tout en délimitant clairement les frontières de ce qui peut être prouvé par ces moyens par rapport à la vérité arithmétique complète.