Méta : J'ai écrit un fil un peu long sur Twitter pour tenter d'expliquer le théorème de Gödel, qui reprend grosso modo des idées de cette entrée passée (au moins la partie sur Gödel de celle-ci) mais en mettant l'accent un peu différemment et donnant plus de détails sur les conditions de prouvabilité. Comme ça peut être un complément intéressant et que tout le monde n'aime pas le format Twitter, je reproduis ici ce que j'y ai dit, en reformatant un minimum (en revanche, mon style sur Twitter est sans doute un peu différent de mon style sur ce blog, et je n'ai pas le courage de reformuler plus qu'a minima) :
Je fais d'abord une tentative pour lever la confusion au sujet
formalisme. Quand on formalise les [raisonnements] mathématiques, on
les décrit sous forme de manipulations de suites de symboles
(« syntaxe ») qui obéissent à des règles bien précises. Il est
évident que si on demande que les règles de
raisonnement elles-mêmes soient formalisées en mathématiques,
on a une régression infinie : si quelqu'un prétend ne comprendre que
ce qui est formel,
c'est turtles
all the way down
, on ne peut rien démarrer… Pour que
le bootstrap soit possible, il faut
bien accepter l'idée de décrire les règles de manipulation de la
logique en français, ou en faisant appel à des notions mathématiques
elles-mêmes pas formalisées (mais néanmoins précises) ! (Refuser
cette idée ce serait comme refuser qu'on puisse jouer aux échecs sous
prétexte que les règles des échecs n'ont pas été formalisées
dans ZFC. Or personne ne pense qu'on a besoin
de ZFC pour jouer aux échecs !)
En revanche, ce qu'on peut faire, c'est une fois qu'on a
accepté ces règles et construit un système formel avec, utiliser ce
système formel pour revisiter (« refléter ») les règles, cette fois-ci
formellement : autrement dit, on reconstruit tout le système qu'on a
déjà construit, mais on le fait cette fois-ci à l'intérieur du système
« externe » qui a été construit informellement. Il y a une mise en
abyme. Je parlerai de système interne
pour celui qu'on construit
ainsi.
Typiquement, ça se fait avec un truc appelé codage de Gödel
:
si le système externe contient l'arithmétique, on dit qu'on peut
refléter toutes les règles formelles comme des manipulations
arithmétiques pour fabriquer le système informel. Le code de Gödel
d'une formule, c'est l'entier qui représente cette formule (et qui
devient, du coup, manipulable par le système externe). Du coup les
énoncés comme P est prouvable
(qui sont, à la base,
informels, parlant du système externe) deviennent des énoncés formels
du système externe et qui parlent du système interne. Des énoncés
arithmétiques. (Je noterai □P
plus bas
pour P est prouvable
.)
Et là, il y a une sorte de postulat épistémologique, qui est que ce que :
Les règles du système interne (formalisées dans le système externe) reflètent correctement les règles du système externe lui-même.
Donc si on croit que le système externe ne dit pas de conneries, et
s'il dit que le système interne ne peut pas prouver <ceci-cela>,
alors effectivement le système externe ne peut pas prouver
<ceci-cela>. (Un ultra-formaliste pourrait rejeter ce postulat
et dire : pour moi, les maths formelles sont juste un jeu
typographique dénué de sens, le système externe ce sont les règles du
jeu, le prétendu
. Mais en vrai, les gens font des maths
parce qu'ils croient qu'une preuve du fait que 2+2=4 apporte quelque
information sur le monde réel, donc il y a bien une connexion entre le
système externe, qui vit dans le monde réel, et le système interne,
formalisé.)système interne
n'a pas de sens, pas plus
qu'aucun énoncé du jeu
Accessoirement, les systèmes externe et interne n'ont pas vraiment besoin d'être les mêmes : en fait on a besoin de très peu d'axiomes pour faire fonctionner Gödel. Mais je ne sais pas si ça aide de dire ça. Donc restons dans l'idée que ce sont « les mêmes ».
Maintenant, de quels ingrédients a-t-on besoin pour prouver Gödel ? On a besoin des trois « conditions de prouvabilité de Hilbert-Bernays » (que je noterai (A), (B), (C)), et de l'astuce de Quine. Expliquons ça successivement :
Les conditions
de prouvabilité de Hilbert-Bernays remplacent le postulat
épistémologique
dont j'ai parlé plus haut par quelque chose de
précis et de formel. En gros, elles font le lien entre les niveaux
externe et interne (et interne², cf. plus bas).
Première chose : (A) si le système externe prouve un énoncé P, alors il prouve que le système interne prouve P [ou plutôt, le code de Gödel de P]. Pourquoi ? Parce que si on a une preuve de P, on peut « refléter » cette preuve : la réécrire comme une preuve formelle dans le système interne, et ceci fournit une preuve de son existence dans le système externe. Bien sûr, tout ce que je viens de dire est informel, puisque (A) est par essence informel ! Mais si on applique ça à un P bien précis et une preuve de P formelle explicite, la recette que je viens de dire donne une preuve tout à fait explicite et formelle (dans le système formel externe) de l'existence d'une preuve dans le système interne. Donc, si on veut, (A) est un métathéorème informel : en soi il n'est pas formel, mais il s'instancie en des théorèmes formels (du système externe) dont on a la recette de construction.
Maintenant on peut refaire tout ça avec un niveau de plus (on a alors trois systèmes : l'externe est informel, l'interne est formalisé dans le système externe, et l'interne² dans le système interne — ça s'arrêtera là) : Tout ce que j'ai dit sur le (A) vaut de nouveau et donne, cette fois, une preuve formelle (dans le système externe) du fait (B) suivant : si le système interne prouve P alors il prouve que le système interne² prouve P. Cette fois c'est un vrai théorème du système externe, pas juste un métathéorème informel.
Enfin, (C) dit que si le système interne prouve [le code de Gödel] de P⇒Q et [celui de] P, alors il prouve [celui de] Q. Ça c'est juste le fait qu'on a la règle de modus ponens dans le système interne (c'est presque une définition).
Bref, si je note □P l'énoncé (du système externe) qui dit qu'il existe une preuve de P dans le système interne, mes conditions de prouvabilité sont :
- (A) si P est un théorème alors □P en est un,
- (B) □P⇒□□P est un théorème,
- (C) □(P⇒Q)⇒□P⇒□Q est un théorème
(tous ces théorèmes dans le système externe ! et ce, quels que soient les énoncés P et Q).
Maintenant, l'astuce de Quine (en fait,
le procédé
diagonal), c'est quelque chose qui permet de fabriquer un
énoncé G tel que G⇔¬□G
(démontrablement dans le système externe !), autrement dit un énoncé
qui dit je ne suis pas un théorème
.
L'astuce fonctionne exactement comme la manière dont on écrit des
programmes qui écrivent leur propre code, chose que j'explique en
détails dans cette page web
consacrée aux quines. On fabrique une
formule R(x) (du système externe) qui
dit si x est une formule du système interne ayant une
variable libre, et qu'on remplace cette variable par le code de Gödel
de x elle-même, alors le résultat n'est pas un théorème (du
système interne)
, ou de façon encore plus
informelle, R(x)
signifie x(‘x’) n'est pas un théorème
(soit ¬□x(‘x’)) en notant ‘x’ le code
de Gödel de x. Mais du coup, R(‘R’)
équivaut à R(‘R’) n'est pas un théorème
(soit ¬□R(‘R’)), et c'est ça que je
note G.
[Ajout par rapport au fil Twitter:] Dans la
présentation informelle proposée par Hofstadter, G est en
gros la phrase suivante : Si on prend le morceau de phrase suivant
et qu'on le fait suivre (après deux points) de lui-même entre
guillemets, on obtient quelque chose qui n'est pas un théorème :
— l'astuce est de dire Si
on prend le morceau de phrase suivant et qu'on le fait suivre (après
deux points) de lui-même entre guillemets, on obtient quelque chose
qui n'est pas un théorème
cet énoncé
n'est pas un théorème
sans passer par une référence à cet
énoncé
que notre système formel ne permet pas de faire ; ceci est
exactement parallèle au mécanisme des quines qui permettent de
coder imprimer ce programme
dans un langage qui ne permet pas
une référence à ce programme
.
Une fois qu'on a ces ingrédients, la preuve de Gödel est pure manipulation formelle. Tout le raisonnement est tenu dans le système externe (mais parle du système interne — voire interne² quand il y a des □□) :
Supposons □G. Alors □□G d'après (B). Mais la preuve (explicite !) de G⇒¬□G donne □(G⇒¬□G) d'après (A). Or □G et □(G⇒¬□G) donnent □¬□G par (C). Or □□G et □¬□G (i.e. □(□G⇒⊥)) donnent □⊥ d'après (C). Bref, on a prouvé □G⇒□⊥ soit ¬□⊥⇒¬□G. C'est-à-dire (qu'on a prouvé dans le système externe) que si le système interne prouve G alors il prouve ⊥ (c'est-à-dire 0=1). I.e., si le système interne est consistant (¬□⊥), il ne peut pas prouver G (soit : ¬□G)… …donc G, qui équivaut à ¬□G, est vrai ! (c'est-à-dire, est un théorème du système externe, prouvé sous l'hypothèse (¬□⊥) que le système interne est consistant. C'est le premier théorème d'incomplétude.
Maintenant, en appliquant (A) à cette preuve (explicite !)
de ¬□⊥⇒¬□G, on obtient □(¬□⊥⇒¬□G) donc
□¬□⊥⇒□¬□G (par (C)). Comme
¬□G⇒G donne □(¬□G⇒G)
par (A) donc □¬□G⇒□G par (C), les
implications □¬□⊥⇒□¬□G, □¬□G⇒□G et
□G⇒□⊥ mises bout à bout donnent finalement □¬□⊥⇒□⊥, ou
encore ¬□⊥⇒¬□¬□⊥. C'est le second théorème d'incomplétude : si le
système (interne) est consistant (¬□⊥) alors il ne prouve pas la
consistance du système interne² (¬□¬□⊥). Et comme en fait tous ces
systèmes sont le même, le postulat épistémologique évoqué ci-dessus
permet de lire ce théorème formel ¬□⊥⇒¬□¬□⊥ sous la forme si Peano
est consistant, il ne prouve pas sa propre consistance
(idem
pour ZFC).
Évidemment, l'ultra-formaliste dont j'ai parlé plus haut objectera et dira que j'ai juste prouvé un énoncé cabalistique ¬□⊥⇒¬□¬□⊥ sans aucun sens dans le monde réel et qui ne dit rien sur mon système externe (lequel vit dans le monde réel). Mais si on croit que les « vrais » entiers naturels ont un sens et que Peano en dit des choses vraies, on est forcé de conclure que Peano est incomplet et ne sait pas prouver certaines choses vraies (essentiellement, il ne sait pas qu'il dit lui-même la vérité).