,
42 tweets,
7 min read
Read on Twitter
Ce qui suit est un fil un peu long sur le théorème de Gödel, que je comptais poster en réponse à — mais que je me dis qu'il vaut mieux poster comme un fil autonome quitte à le retweeter là. •1/42
Je fais une tentative pour lever la confusion sur le 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. •2/42
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… •3/42
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)! •4/42
(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!) •5/42
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: •6/42
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. •7/42
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. •8/42
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). •9/42
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.) •10/42
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: •11/42
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>. •12/42
(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 «système interne» n'a pas de sens, pas plus qu'aucun énoncé du jeu. •13/42
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é.) •14/42
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». •15/42
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. J'explique ça en une quinzaine de tweets. •16/42
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). •17/42
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: •18/42
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… •19/42
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. •20/42
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. •21/42
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à): •22/42
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. •23/42
Cette fois c'est un vrai théorème du système externe, pas juste un métathéorème informel. •24/42
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). •25/42
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: •26/42
✱(A) si P est un théorème alors □P en est un, ✱(B) □P⇒□□P est un théorème, et ✱(C) si □(P⇒Q)⇒□P⇒□Q est un théorème (tous ces théorèmes dans le système externe!). •27/42
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». •28/42
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 madore.org/~david/compute… •29/42
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)», •30/42
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. •31/42
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 □□): •32/42
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. •33/42
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)… •34/42
…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. •35/42
Maintenant, en appliquant (A) à cette preuve (explicite!) de ¬□⊥⇒¬□G, on obtient □(¬□⊥⇒¬□G) donc □¬□⊥⇒□¬□G (par (C)). •36/42
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 ¬□⊥⇒¬□¬□⊥. •37/42
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² (¬□¬□⊥). •38/42
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). •39/42
É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). •40/42
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é). •41/42
J'avais fait une tentative d'explication assez semblable (mais néanmoins différente) sur mon blog ici: madore.org/~david/weblog/… •42/42
