Thread by @maxime_ramzi

C'est parti pour le troisième, sur les théorèmes d'incomplétude de Gödel (qui ont inexplicablement perdu contre la formule de Bayes........)
Bon évidemment je commence par une petite anecdote : mon prof de sup nous les a (trèèèès vaguement) présentés en tout début de sup.

Il venait de nous raconter le premier, en expliquant (vaguement à nouveau) comment dire "je ne suis pas prouvable", et je lui demande alors si on ne venait pas de prouver cet énoncé (on venait de voir qu'on ne pouvait pas le démontrer !), et il me répond alors

"si T sait qu'elle est cohérente ! C'est le 2nd théorème d'incomplétude" et je n'avais (évidemment) pas tout compris, mais l'élégance de l'argument m'a marqué et ça m'a poussé à étudier pas mal de logique après coup. C'était une très bonne manière de se mettre en confiance

pour la prépa 😁
Fin de l'anecdote, revenons au sujet : les théorèmes d'incomplétude de Gödel. Je ne vais pas les énoncer précisément, ça ne servirait à rien, mais en voici des approximations :
1- "Soit T une théorie cohérente suffisamment puissante pour exprimer l'arithmétique,

et qui se décrit de manière raisonnable. Alors il existe des énoncés qui ne sont ni démontrables, ni réfutables dans T" [on parle d'énoncés indécidables]

Ici, par "théorie" on entend un certain ensemble d'axiomes, exprimés dans un langage fixé à l'avance. Par exemple

l'arithmétique de Peano, ou encore la théorie des ensembles au sens usuel (ZF ou ZFC) sont de telles théorie.
Cohérente, ça veut dire qu'elle ne démontre pas de contradiction, comme "P et non P" (typiquement "on ne peut pas démontrer 0 = 1 dans l'arithmétique de Peano")

ou encore, par le principe d'explosion (ex falso quod libet, le faux implique tout), ça veut dire qu'il y a des choses qu'elle ne démontre pas.
"suffisamment puissante pour exprimer l'arithmétique" devrait être clair intuitivement; et finalement "qui se décrit de manière

raisonnable" est ma version d'une condition de calculabilité de la théorie - en gros on peut dire, algorithmiquement, quels sont les axiomes de la théorie ("raisonnable" parce que si notre théorie ne satisfait pas ça, on va avoir du mal à l'utiliser !!)

Je commence par une petite remarque pour expliquer pourquoi cette condition de "raisonnabilité" est "évidemment" nécessaire: soit T la théorie (dans le langage de l'arithmétique) dont les axiomes sont tous les énoncés vrais dans N. Bah il n'y a pas d'énoncé indécidable, puisque

un énoncé est vrai ou faux dans N, s'il est vrai, c'est un axiome (donc démontrable), s'il est faux, sa négation est un axiome (donc il est réfutable).
Bon évidemment cette théorie est inutilisable, et d'ailleurs un corollaire du théorème d'incomplétude est qu'elle n'est pas

"raisonnable" en ce sens algorithmique.
Comment on démontre ce théorème ? En gros l'idée c'est de formaliser, *à l'intérieur de T* (et c'est très important) la notion de proposition. C'est là qu'on se sert du pouvoir expressif de l'arithmétique : grâce aux "entiers"

on peut coder des formules. C'est un peu technique, et notamment c'est un endroit où on utilise que le langage aussi, est raisonnable, mais en gros on obtient un moyen pour T de parler d'énoncés. En gros on code des "métamaths" dans T.
(je grossis un peu le trait ici, je risque

de me faire crier dessus des mots comme "entiers non standard" mais bon pas grave je fais avec)
Maintenant, c'est là qu'on utilise l'hypothèse de raisonnabilité sur T : puisque T a des axiomes raisonnables (et que l'arithmétique suffit à parler de machines de Turing et donc,

d'algorithmes), on peut encoder, dans T, la notion de "démontrabilité dans T". Alors, en encodant la formule "n est un entier qui code un énoncé qui n'est pas démontrable" comme un entier, on fait un petit tour de passe-passe (il y a un théorème de point fixe qui intervient)

qui permet d'obtenir une formule f qui dit "f n'est pas démontrable".
En fait, peut-être pour en dire un peu plus : on encode par des entiers les formules de la forme g(x), et on regarde la formule "x est un entier qui code une formule g telle que g(x) n'est pas démontrable"

Cette formule est encodée par un entier n, et alors f(n) = "n est un entier qui code une formule g [c'est f !] telle que g(n) [c'est f(n) !!] n'est pas démontrable", i.e. f(n) est un énoncé équivalent à "f(n) n'est pas démontrable". On a maintenant presque fini:

si f(n) est démontrable dans T, alors première "f(n) n'est pas démontrable dans T" l'est aussi (bah oui, ce sont deux énoncés équivalents)
Mais aussi, "f(n) est démontrable dans T l'est aussi" : en effet si j'ai une vraie preuve de f(n), je peux l'encoder dans T (qui sait

exprimer ces choses là), donc T prouve une formule et son contraire, et donc T est incohérente (on a supposé qu'elle l'était, c'est donc absurde).
Donc f(n) n'est pas démontrable dans T.

Si f(n) est réfutable dans T, alors "f(n) est démontrable dans T" est démontrable,

et pareil la réfutation de f(n) peut s'encoder dans T, ce qui va à nouveau impliquer l'incohérence de T.
Donc f(n) est indécidable dans T.

Evidemment, il manque une grosse partie du travail (à savoir la formalisation des énoncés dans T etc. qui est du travail d'arithmétique et

il faut être patient), mais voilà l'idée.

Sauf que là, on se sent bête parce qu'on a l'impression qu'on vient de prouver que f(n) n'était pas démontrable, i.e. qu'on vient de prouver f(n) 🤯😱
Sauf que cette preuve, on l'a pas faite dans T. En particulier, on l'a faite en

supposant que T était cohérente, et c'est pas du tout clair qu'on puisse faire cette supposition dans T. En fait, pire : toute la preuve qu'on a faite, on peut la formaliser dans T (puisque T sait exprimer l'arithmétique, et le niveau de cette preuve ne dépasse pas trop ça)

et donc, dans T, on a "si T est cohérente, alors f(n) n'est pas démontrable" (note: pour pouvoir exprimer "T est cohérente" *dans T* il faut aussi cette hypothèse de raisonnabilité). En particulier, si T prouve sa propre cohérence, i.e. T prouve "T est cohérente", T prouve que

f(n) n'est pas démontrable, et donc T prouve f(n) (puisque T est cohérente). Mais ça, on a vu que ce n'était pas possible lorsque T est cohérente. On a donc le second théorème d'incomplétude:
2 - Une théorie comme plus haut ne démontre pas sa propre cohérence.

Bon après cette "preuve" relativement longue (plus que ce à quoi je m'attendais), continuons. Déjà, ces théorèmes sont un gros stop à Hilbert. En gros ils impliquent qu'on ne pourra jamais construire des maths sur des fondations dont on prouverait qu'elles sont cohérentes

(si on prouve qu'elles le sont, c'est qu'elles ne le sont pas, puisqu'évidemment cette preuve devrait se faire dans ces fondations), alors que c'était le rêve d'Hilbert, une partie de son programme.
ça implique que pour faire des maths (assez de maths pour parler d'arithmétique)

il faut à un moment un "saut de la foi" (ou être conscient que rien n'est assuré).
Moi je trouve ce théorème fou parce que c'est un théorème d'impossibilité, mais qui nous parle de démonstrations - il y a eu d'autres théorèmes d'impossibilité avant, par exemple Galois,

mais celui-ci parle de la nature même des maths. Alors, certes, quand on voit la preuve (disons du premier), on est un peu déçu parce que c'est des manipulations d'entiers etc. mais le fait est que le 2nd théorème est là et il n'y a rien qu'on puisse y faire.

La cohérence d'une théorie suffisamment forte, et utilisable, est donc complètement hors de portée de cette dernière, et donc la cohérence de l'édifice mathématique est elle aussi complètement hors de portée - et pas parce qu'on est bêtes 😁

Certaines personnes pensent même d'ailleurs que Peano et ZF(C) sont incohérentes (voire possiblement "pas trop" - on peut se poser la question des maths paraconsistentes, qui permettraient l'existence de contradictions sans que tout s'effondre. )

Ces théorèmes ont changé la face de la logique et de la théorie des ensembles après (ZF est criblée d'énoncés indécidables, bien plus intéressants que "je ne suis pas démontrable", même d'ailleurs en dehors de la théorie des ensembles pure)

et leur influence serait difficile à décrire sur twitter.

Un autre truc que je veux mentionner c'est une autre preuve du 1er théorème, essentiellement due à Turing - cf.

https://twitter.com/maxime_ramzi/status/1266011942604455936

En effet on peut démontrer le 1er thm de Gödel grâce à l'impossibilité de résoudre le problème de l'arrêt (c'est la même preuve, présentée différemment mais pour les informaticien-ne-s ça peut être intéressant): en effet si tout énoncé était réfutable ou prouvable,

on aurait une solution au problème de l'arrêt: tu me donnes un algorithme et une entrée, moi j'énumère toutes les preuves dans Peano et dès que je tombe sur une preuve de "M s'arrête sur cette entrée" ou de "M ne s'arrête pas sur cette entrée" (qui sont des énoncés arithmétiques!

), je m'arrête et je te renvoie la réponse.
Si Peano prouvait tous les énoncés, cet algorithme terminerait sur chaque entrée et ne se tromperait pas - bref, ça résoudrait le problème de l'arrêt, et ça, c'est facile à décrire à un grand public en parlant d'algorithmes

(je préfère d'ailleurs cette preuve 😁 mais je voulais mentionner l'originale néanmoins, ne serait-ce que pour avoir le 2nd thm "gratos")
Gödel, pour ces travaux est d'autre, est considéré comme le plus grand logicien de tous les temps (on dit parfois "depuis Aristote", mais

je ne connais pas les travaux de ce dernier)
Il faut voir à quel point ces résultats sont chamboulants pour des gens qui voulaient avoir des fondements solides aux mathématiques (après la crise des fondements), et se rendent compte que ce n'est simplement pas possible.

Je sais pas je trouve ça incroyable, et je trouve que c'est vraiment une réussite de l'esprit humain, d'entrevoir les limites de la logique - elle peut offrir plein de choses, et on a aperçu jusqu'où on pouvait aller.

Ces théorèmes ne sont pas un aveu d'échec, au contraire, c'est un succès d'arriver à de telles frontières, aux limites du raisonnement, de la notion de raisonnement. Ce n'est pas un "nous ne pouvons pas" - c'est "c'est impossible", et ça ça change tout !

Et puis, c'est une superbe formalisation (parallèle aux théorèmes de Cantor et de Russell) du paradoxe du menteur qu'on se traîne depuis des millénaires sans vraiment savoir son statut !
J'avoue manquer un peu de mots pour décrire mon émerveillement face à ces théorèmes,

il y a un attachement émotionnel en plus d'intellectuel - je pense que le fil aurait été meilleur sans ça 😁
Du coup je vais m'arrêter là, au risque de vous laisser sur votre faim (l'heure du dîner approche de toute façon)