On a Theorem by Bezboruah & Shepherdson

Cet article examine et réfute l'objection de Kreisel concernant le théorème d'incomplétude de Bezboruah et Shepherdson sur la théorie ${\sf PA}^-$, le compare à l'extension de Pudlák du deuxième théorème d'incomplétude, et en propose une nouvelle démonstration fondée sur un codage des suites inspiré par Nielsen et Markov.

L'essentiel

🕵️‍♂️ Le Mystère du "Grand Théorème" : Une histoire de castors et de murs

Imaginez que les mathématiques sont un immense château fort. Au cœur de ce château se trouve une règle d'or, le Grand Théorème (le deuxième théorème d'incomplétude de Gödel). Cette règle dit essentiellement : "Aucun système logique ne peut prouver sa propre sécurité, sauf s'il est déjà cassé de l'intérieur."

En 1976, deux chercheurs, Bezboruah et Shepherdson, ont voulu tester cette règle sur un petit poste de garde très simple, appelé Q (une théorie mathématique très basique, presque un jouet comparé aux géants comme l'arithmétique de Peano). Ils ont découvert que même ce petit poste de garde ne pouvait pas prouver qu'il était sûr.

Mais alors, un vieux sage du château, Georg Kreisel, a levé la main et a dit : "Attendez ! Votre preuve est inutile. Votre petit poste de garde est si faible qu'il ne comprend même pas ce que signifie 'être sûr'. C'est comme demander à un castor de comprendre la théorie de la relativité. Le résultat n'a aucun sens philosophique."

Albert Visser, l'auteur de cet article, revient aujourd'hui pour dire : "Non, Kreisel a tort. Le castor a parfaitement compris la question, et la réponse est tout aussi fascinante, même si le castor est petit."

Voici les trois actes de cette histoire :

---

Acte 1 : Le débat sur le sens (Pourquoi le castor compte)

Kreisel pensait que pour qu'une phrase dise "Je suis sûr", il faut que le système ait assez de puissance pour vérifier les règles de la logique (les "conditions de Hilbert-Bernays"). Pour lui, dans un système faible comme Q, la phrase "Je suis sûr" ne signifie pas vraiment la sécurité, mais juste une propriété algébrique bizarre.

L'analogie du castor :
Imaginez que vous demandez à un castor : "Peux-tu prouver que ton barrage ne va pas s'effondrer ?"
Kreisel dit : "Non, le castor ne sait pas ce qu'est un 'barrage'. Il ne voit que des branches. Donc sa réponse ne compte pas."

Visser répond : "Mais le castor voit bien les branches ! Si le castor dit 'Je ne peux pas prouver que mon barrage tient', c'est une information précieuse. Peu importe si le castor ne connaît pas la physique des fluides. Le fait qu'il échoue à prouver la sécurité montre une limite fondamentale de sa capacité à raisonner, même avec ses outils simples."

Visser explique que le sens d'une phrase ne change pas selon qui la lit. Si "Je suis sûr" signifie la sécurité dans un grand système, cela signifie la même chose dans un petit système. Le fait que le petit système ne puisse pas le prouver est une découverte technique magnifique, pas une erreur de sens.

---

Acte 2 : Deux façons de construire le mur

L'article compare deux méthodes pour prouver que le castor (la théorie Q) ne peut pas prouver sa sécurité.

1. La méthode moderne (Pudlák) : C'est comme construire un pont très sophistiqué. On utilise des outils mathématiques avancés (des "coupes" définissables) pour montrer que si le petit système prouvait sa sécurité, il deviendrait aussi puissant qu'un géant, ce qui est impossible. C'est élégant, mais un peu abstrait.
2. La méthode Bezboruah-Shepherdson (1976) : C'est comme construire un mur de briques, une par une, avec les mains. Ils ont créé un modèle (un monde imaginaire) où le système pense avoir prouvé sa sécurité, mais en réalité, il y a une faille cachée. C'est une preuve très "concrète" et visuelle.

Visser dit que ces deux méthodes sont comme deux routes différentes menant au même sommet. Elles ne se ressemblent pas, mais elles confirment toutes deux la même vérité : la sécurité ne peut pas être prouvée de l'intérieur, même pour les plus petits systèmes.

---

Acte 3 : La nouvelle preuve avec le code "Markov" (Le tour de magie)

Dans la dernière partie, Visser fait quelque chose d'amusant. Il dit : "Les anciens ont utilisé un code pour écrire les preuves (le code bêta), un peu comme un code-barres complexe. Mais j'ai trouvé un nouveau code, basé sur les matrices (des grilles de nombres), inventé par un mathématicien nommé Markov."

L'analogie des matrices :
Imaginez que vous avez deux types de briques magiques, appelées A et B.

• La brique A ajoute une marche.
• La brique B tourne d'un quart de tour.
  Si vous empilez ces briques dans un ordre précis, vous créez une "tour" (une séquence).

Visser construit un monde imaginaire (un modèle mathématique) où il y a deux castors, disons Castor A et Castor B.

• Castor A a empilé une tour de briques A pendant une durée infinie (mais finie dans son monde).
• Castor B a empilé une tour de briques B pendant une autre durée.

Ensuite, Visser mélange les deux tours pour créer une super-tour qui semble être une preuve parfaite de la sécurité. Mais, dans ce monde imaginaire, il y a un piège : la super-tour cache une faille. Elle commence par des briques "A" (les axiomes) et finit par des briques "B" (la contradiction), mais il manque le moment précis où l'on passe de l'un à l'autre.

Dans ce monde, le système croit avoir prouvé qu'il est sûr, mais en réalité, il a prouvé qu'il est faux (il a prouvé le "Faux" ou $\bot$). C'est une preuve visuelle et concrète que même avec un système très simple, on peut tromper la logique si on ne fait pas attention.

---

🎯 Leçon à retenir

Cet article nous dit trois choses importantes :

1. Ne sous-estimez pas les petits systèmes : Même les théories mathématiques les plus simples ont des limites profondes. Le fait qu'elles ne puissent pas prouver leur propre sécurité est une vérité universelle, pas un détail technique.
2. La critique de Kreisel était trop stricte : On ne doit pas rejeter une preuve juste parce qu'elle utilise un système "faible". La faiblesse du système est précisément ce qui rend la découverte intéressante.
3. L'ingéniosité des mathématiciens : En utilisant des codes différents (comme les matrices de Markov), on peut voir les mêmes vérités sous un angle nouveau et plus clair. C'est comme regarder un diamant sous différentes lumières pour voir tous ses éclats.

En résumé, Visser nous invite à célébrer la preuve de Bezboruah et Shepherdson comme un chef-d'œuvre de logique, même si elle a été critiquée il y a 50 ans. C'est une preuve que parfois, pour comprendre les limites de la raison, il faut regarder les plus petits outils de notre boîte à outils.

Résumé technique

Voici un résumé technique détaillé de l'article « On a Theorem by Bezboruah & Shepherdson » d'Albert Visser, structuré selon les points demandés.

1. Le Problème et le Contexte

L'article se concentre sur un résultat d'incomplétude établi par Bezboruah et Shepherdson en 1976 ([BS76]), concernant la théorie arithmétique faible $PA^-$ (la théorie des parties non-négatives d'un anneau commutatif ordonné discrètement) et son incapacité à prouver sa propre cohérence, ou celle de théories encore plus faibles.

Le débat central :

• L'objection de Kreisel : Georg Kreisel a soutenu que le théorème d'incomplétude de Gödel n'avait pas de sens pour des théories aussi faibles que $Q$ (l'arithmétique de Robinson) ou $PA^-$. Son argument repose sur le fait que ces théories ne peuvent pas vérifier les conditions de Hilbert-Bernays-Löb pour le prédicat de prouvabilité. Selon Kreisel, la formule $con(Q)$ n'exprimerait pas la « cohérence » de $Q$ dans le contexte de $Q$ lui-même, mais seulement une propriété algébrique qui ne deviendrait une expression de cohérence que dans une théorie plus forte.
• La position de Visser : Visser rejette l'objection de Kreisel. Il soutient que le sens d'une formule (comme $con(Q)$) ne doit pas varier selon la théorie dans laquelle on l'interprète. Si une formule exprime la cohérence dans l'arithmétique vraie, elle l'exprime aussi dans les sous-théories, même si ces dernières ne peuvent pas prouver les propriétés métamathématiques attendues du prédicat de prouvabilité.

2. Méthodologie

Visser adopte une approche triple pour traiter ce sujet :

1. Analyse Philosophique et Logique : Il examine l'argument de Kreisel et le compare aux versions modernes du deuxième théorème d'incomplétude (notamment celles de Pavel Pudlák).
2. Comparaison Technique : Il met en contraste la méthode de Bezboruah-Shepherdson (basée sur la construction de modèles spécifiques) avec la méthode de Gödel-Pudlák (basée sur l'interprétation de théories plus fortes sur des coupes définissables).
3. Nouvelle Preuve Constructive : Il propose une nouvelle preuve du théorème de Bezboruah-Shepherdson en utilisant un codage de séquences différent de celui de l'article original (qui utilisait la fonction $\beta$ de Gödel). Visser utilise un codage basé sur la théorie des groupes et des matrices, inspiré par les travaux de Nielsen et Markov.

3. Contributions Clés et Résultats

A. Réfutation de l'objection de Kreisel

Visser démontre que l'argument de Kreisel n'est pas convaincant. Il soutient que l'incomplétude pour $Q$ ou $PA^-$ reste un résultat technique significatif et didactique. Il note que les preuves de tels résultats permettent de construire des modèles avec des propriétés très spécifiques (par exemple, des preuves d'incohérence visibles et compréhensibles dans le modèle), ce qui a une valeur pédagogique que les preuves d'incomplétude standard (via des coupes) n'ont pas toujours.

B. Comparaison : Bezboruah-Shepherdson vs. Gödel-Pudlák

Visser clarifie la relation entre deux résultats qui semblent similaires mais sont fondamentalement différents :

• Théorème de Gödel-Pudlák (Théorème 3.4) : Si une théorie c.e. $U$ interprète $Q + con(U)$, alors $U$ est incohérente. Ce résultat repose sur le fait que $Q$ interprète $S^1_2$ (la théorie de la complexité temporelle polynomiale) sur une coupe définissable. Il est très général mais dépend fortement de la capacité d'interprétation.
• Théorème de Bezboruah-Shepherdson (Théorème 3.5) : $PA^-$ ne prouve pas la cohérence d'une théorie extrêmement faible (appelée $BeSh$), sous réserve d'un codage spécifique (fonction $\beta$).
• Différences majeures :
  • Le résultat de Bezboruah-Shepherdson ne se généralise pas facilement aux versions par interprétation (ex: $R$ n'interprète pas $R + con(R)$ de la même manière).
  • Le codage est crucial pour Bezboruah-Shepherdson (nécessite la fonction $\beta$), tandis que le résultat de Pudlák est plus robuste face aux variations de codage.
  • Le résultat de Pudlák implique la fermeture sous la règle de Löb, ce qui n'est pas le cas pour Bezboruah-Shepherdson.

C. Nouvelle Preuve avec le Codage de Markov (Section 4)

C'est la contribution technique principale de l'article. Visser reprouve le théorème en utilisant un codage de séquences basé sur le groupe $SL_2(\mathbb{Z})$ (matrices $2 \times 2$ à coefficients entiers et déterminant 1).

• Le Codage : Il utilise l'isomorphisme entre le monoïde libre à deux générateurs et le sous-groupe $SL_2(\mathbb{Z}^+)$ (matrices à coefficients non négatifs). Les générateurs sont $A = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$ et $B = \begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}$. Une séquence est codée par un produit de matrices.
• Construction du Modèle :
  • Visser considère deux modèles non standards de l'arithmétique vraie, $M$ et $N$, où $N$ est une extension élémentaire terminale de $M$.
  • Il choisit des éléments non standards $a \in M$ et $b \in N \setminus M$.
  • Il construit une matrice $\beta = [n]^a [m]^b$ dans $N$, où $[n]$ et $[m]$ sont des matrices spécifiques codant des axiomes et des conclusions.
  • Il définit un sous-modèle $K$ (partie non négative d'un anneau ordonné) généré par les entrées de cette matrice.
• Le Paradoxe du Modèle :
  • Dans le modèle $K$, la séquence codée par $\beta$ apparaît comme une preuve valide de la contradiction ($\bot$) dans la théorie $BeSh$.
  • Cependant, cette « preuve » est illégale dans le modèle standard car elle repose sur une transition invisible entre les axiomes et la conclusion qui n'est pas détectable dans $K$ (la séquence contient une partie infinie d'axiomes suivie d'une partie infinie de conclusions, mais le point de bascule est « caché » par la structure du modèle).
  • Résultat (Théorème 4.1) : La théorie $PA^-$ (plus toutes les sentences universelles vraies) ne prouve pas la cohérence de $BeSh$ sous ce codage.

4. Signification et Impact

• Valeur Didactique : La preuve de Visser offre une visualisation claire de la différence entre les sentences universelles et les sentences $\Pi^0_1$. Elle montre comment un modèle peut « croire » à une preuve d'incohérence alors que cette preuve n'existe pas dans le monde standard, en manipulant la structure des séquences infinies.
• Robustesse du Théorème : En fournissant une troisième preuve (après celle de Bezboruah-Shepherdson et celle utilisant la fonction $\beta$), Visser confirme que le résultat n'est pas un artefact d'un codage spécifique, mais une propriété fondamentale des théories faibles comme $PA^-$.
• Clarification Conceptuelle : L'article dissipe le malentendu persistant autour de l'objection de Kreisel, réaffirmant que l'incomplétude s'applique même aux théories les plus faibles, à condition de bien définir ce que signifie « prouver la cohérence » dans ce contexte.
• Innovation Technique : L'utilisation du codage de Markov via $SL_2$ ouvre de nouvelles perspectives pour l'étude des preuves dans les théories faibles, en évitant les complexités de la fonction $\beta$ de Gödel tout en conservant la puissance nécessaire pour encoder la structure des preuves.

En résumé, Visser réhabilite le théorème de Bezboruah-Shepherdson, le distingue clairement des résultats modernes d'interprétation, et fournit une preuve élégante et nouvelle utilisant la théorie des groupes et les modèles non standards, renforçant ainsi notre compréhension des limites de l'arithmétique faible.