En attendant Gödel

David Olivier · June 2019

J'ai le projet de comprendre les théorèmes d'incomplétude de Gödel. De les comprendre bien, dans les détails, pas juste comme dans les vulgarisations que j'ai lues.

J'ai l'impression qu'il faut que je commence par bien maîtriser les notions de systèmes formels de calculs propositionnels, de logique de 1er ordre, etc. J'ai cru qu'en étudiant ZFC, on me présenterait ça, mais j'ai lu et étudié Halmos, Naive Set Theory, et il y a bien tous les axiomes, et des raisonnements rigoureux, ça m'a beaucoup intéressé et appris, mais je n'y ai pas trouvé la formalisation que j'attendais - genre chaînes de signes, règles de transformations, etc. Or si je comprends bien, Gödel se base sur ce genre de formalisation, avec numérotation des signes. (Pas forcément sur ZFC, d'ailleurs, si j'ai bien compris - j'ai lu que ses théorèmes sont valables dans des systèmes d'axiomes plus faibles.)

J'ai trouvé un document, Gilles Dowek, Teaching Gödel's incompleteness theorems, qui a l'air de confirmer qu'il y a un parcours un minimum ardu pour parvenir à vraiment maîtriser le sujet:

«It is impossible to reach, in a few weeks, the second incompleteness theorem and Löb’s theorem with students who have never been exposed to the basics of predicate logic, exactly in the same way that it is impossible to reach in a few weeks the notion of analytic function with students who have never had been exposed to the notions of function and complex number.»

J'ai envie pourtant de m'y essayer, mais ce document est pour les enseignants, et il parle de beaucoup de choses qui me sont obscures.

Est-ce que quelqu'un peut me conseiller comment démarrer; soit un livre entièrement sur le sujet (mais partant de mon niveau), soit quelque chose pour démarrer sur la logique et sa formalisation, dans la perspective d'arriver à Gödel? (En français ou en anglais, de préférence.)

Merci.

Maxtimax · June 2019

Comme d'habitude quand on demande des références de logique, je conseille Logique Mathématique, de Cori et Lascar. Tout n'y traite pas de Gödel, mais Gödel y est traité. Tu peux regarder le sommaire : Gödel est traité dans le tome 2, mais il y a des prérequis du tome 1, si tu les as, pas la peine de le lire.

David Olivier · June 2019

Merci. Heu... Il y a aussi une question de prix.

S'il y avait une bonne intro déjà aux bases, pour pas trop cher, ou un pdf bien bâti...

Foys · June 2019

Le message ci-dessous a pour but de présenter un des ingrédients de la preuve du second théorème de Gödel (parfois évoqué informellement en disant "qu'une théorie consistante ne démontre pas sa consistance"), à savoir le théorème de Löb. L'idée est d'alléger la lecture ultérieure d'une démonstration complète de ce résultat en montrant les buts intermédiaires à atteindre (en l'espèce 7 hypothèses plus bas)et comment s'en servir.
Sauf erreur il y a un exposé détaillé dans le livre "Théorie des ensembles" de P.Dehornoy. (à confirmer car je n'ai pas ce livre, je l'ai seulement feuilleté très très vite). Sinon il y a Smullyan: Forever undecided.
Parmi les hypothèses (i) à (vii) ci-dessous, (i),(ii) et (iii) expriment des propriétés logiques banales des théories formalisées, (v) est un résultat "de point fixe" important (il intervient de manière cruciale dans la preuve du premier théorème d'incomplétude de Gödel), (iv) et (vi) disent que $\Box$ exprime la prouvabilité d'une formule - (iv) (resp vii) exprime le fait que le résultat (i) (resp vi) est exprimable et est un théorème à l'intérieur de la théorie étudiée elle-même.
Cf. https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_conditions
Noter que pour être applicable aux théories courantes des mathématiques (arithmétique, théorie des ensembles...), il importe de définir $\Box$ et de démontrer complètement les hypothèses (i) à (vii) mais ces dernières sont difficiles et très techniques- il faut tout formaliser en détail, d'où la longueur des exposés des traités qui sont consacrés à ce sujet.

$\newcommand{\t}{\vdash}$
$\newcommand{\b}{\Box}$
$\newcommand{\c}{\supset}$
Dans ce message, on considère des "formules" (peu importe ce que ça veut dire).
Quelles que soient les formules $e,f,g$, on a d'autres formules $\b e$ et $f \c g$.
Certaines formules seront des "théorèmes".

Conventions de notation: on conviendra de l'associativité à droite pour les parenthèses, i.e. $a \c b \c c$ désignera toujours $a \c (b \c c)$ et non pas $(a \c b) \c c$ pour tous $a,b,c$.
"$\c$" est prioritaire sur"$\b$" (ainsi $\b x \c y$ désigne $(\b x) \c y$ et non pas $\b(x \c y)$) pour tous $x,y$.
On abrègera pour toute formule $x$, "$x$ est un théorème" par ""$\t x$ ".
On abrègera pour toutes formules $m,n$, "$\t m \c n$ et $\t n \c m$" par $m \equiv n$ (et on dira aussi le cas échéant, que "$m$ et $n$ sont équivalentes")

Dans toute la suite on fait les hypothèses suivantes:

(i) pour toutes formules $x,y$, si $\t x$ et $\t x \c y$ alors $\t y$
(ii) pour toutes formules $x,y,z$, $\t (x \c y \c z) \c (x \c y) \c x \c z$
(iii) pour toutes formules $x,y,z$, $\t(x \c y) \c (y \c z) \c x \c z$
(iv) pour toutes formules $x,y$, $\t \b (x \c y) \c \b x \c \b y$
(v) pour toute formule $p$, il existe $f\in A$ tel que $f \equiv \b f \c p$ ("point fixe")
(vi) pour toute formule $x$, si $\t x$ alors $\t \b x$
(vii) pour toute formule $x$, $\t \b x \c \b \b x$.

Lorsque ces 7 hypothèses sont satisfaites, on a le Théorème de Löb:
Pour toute formule $p$, si $\t \b p \c p$, alors $\t p$.

Preuve:
Soit $p$ une formule telle que $\t \b p \c p$.
D'après (v), il existe une formule $x$ tel que $x \equiv \b x \c p$ autrement dit (abréviations)
1° $\t x \c \b x \c p$ et
2° $\t (\b x \c p) \c x$.

Puis on a successivement:

3° $\t \b ( x \c \b x \c p )$ [(vi) appliqué à 1°]
4° $\t \b ( x \c \b x \c p ) \c \b x \c \b (\b x \c p)$ [(iv)]
5° $\t \b x \c \b (\b x \c p)$ [(i) appliqué à 3° et 4°]
6° $\t \b (\b x \c p) \c \b \b x \c \b p$ [(iv)]
7° $\t \left (\b x \c \b (\b x \c p) \right ) \c \left ( \b (\b x \c p) \c \b \b x \c \b p\right ) \c \b x \c \b \b x \c \b p$ [(iii)]
8° $ \t \left ( \b (\b x \c p) \c \b \b x \c \b p\right ) \c \b x \c \b \b x \c \b p$ [(i) appliqué à 5° et 7°]
9° $\t \b x \c \b \b x \c \b p$ [(i) appliqué à 6° et 8°]
10° $\t (\b x \c \b \b x \c \b p) \c (\b x \c \b \b x) \c \b x \c \b p$ [(ii)]
11° $\t (\b x \c \b \b x) \c \b x \c \b p$ [(i) appliqué à 9° et 10°]
12° $\t \b x \c \b \b x$ [(vii)]
13° $\t \b x \c \b p$ [(i) appliqué à 12° et 11°]
14° $\t \b p \c p$ [supposition de l'énoncé]
15° $\t (\b x \c \b p) \c (\b p \c p) \c \b x \c p$ [(iii)]
16° $\t (\b p \c p) \c \b x \c p$ [(i) appliqué à 13° et 15°]
17° $\t \b x \c p$ [(i) appliqué à 14° et 16°]
18° $\t x$ [(i) appliqué à 17° et 2°]
19° $\t \b x$ [(vi) appliqué à 18°]
20° $\t p$ [(i) appliqué à 19° et 17°]

CQFD.

***********

Application: On suppose maintenant (en plus de toutes les hypothèses précédentes) qu'il y a une formule particulière "$\perp$", et que pour toute formule $a$, il a une formule (notée $\neg a$) qui est équivalente (cf intro en marron) à $a \c \perp$.
Pour le côté intuitif, $\perp$ se lit "faux" (ou parfois: "tout est vrai", cf règle "ex falso sequitur quod libet" des logiciens), pour toute formule $y$, $\neg y$ se lit "non $y$" ou "négation de $y$" et enfin $\b y$ se lit "$y$ est prouvable"

Alors la formule $\neg (\b \perp)$ se lit "la théorie ambiante est consistante" (elle exprime que $\perp$ n'est pas prouvable).
Et bien si la théorie est vraiment consistante, ce fait ne pourra pas être un théorème (et donc on ne peut pas le prouver car en maths un théorème est par définition un énoncé prouvable).
En effet si $\neg (\b \perp)$ est un théorème, alors $\b \perp \c \perp$ aussi(*) donc $\perp$ aussi par Löb.

[size=x-small](*) En effet, l'hypothèse (i) entraîne que si deux formules sont équivalentes et si l'une est un théorème alors l'autre aussi[/size].

christophe c · June 2019

C'est une erreur de fond de croire que ce que tu appelles "vulgarisation" ne te donne pas une preuve formelle.

À la différence de "je suis fausse" qui est une phrase égale à sa négation la phrase G:= "je ne suis pas prouvable" est tout ce qu'il y a de plus classique et mathématique.

À la condition bien sûr de préciser ce veut dire "prouvable" formellement pour u.e suite quelconque de symboles.

Dans Peano ce qui fait le taf c'est qu'on peut parler de SUITES FINIES via le théorème chinois. Le reste est trivial.

Un conseil aussi: tu peux passer par l'informatique. Les phrases prouvables (dans tes théories préférées) sont générées par des programmes très simples. Tu as alors que la phrase G affirme qu'elle ne sera énumérée par ledit programme et comme tu vois ça "fait concrètement sens" :-D

De mon téléphone

Martial · June 2019

@David : ce que dit Christophe au début de son dernier post est parfaitement juste. Heuristiquement, la preuve du 1er théorème d'incomplétude tient en 2 lignes :
Soit G la formule "je ne suis pas prouvable".
Si G est fausse, elle est prouvable, donc la théorie démontre un truc faux, elle est contradictoire.
Donc G est vraie, et par conséquent non prouvable.
(Bon, ça fait 3 lignes).
Après, toute la difficulté consiste à arithmétiser la syntaxe pour montrer qu'une telle formule existe bien dans le langage de l'arithmétique.
Et c'est là que je rejoins le point de vue de Maxtimax : un jour j'ai lu un bouquin de vulgarisation sur les théorèmes de Gödel, je n'y ai rien compris. Après j'ai lu le Cori Lascar, et les choses se sont éclairées.
C'est vraiment la référence de base dans le domaine.
Maintenant, si c'est une question de thunes tu peux peut-être l'emprunter dans une bibliothèque (universitaire ou autre) ou le trouver d'occase chez amazon, Price Minister, EBay etc (je ne fais pas de pub, c'est juste une suggestion).
Quant à l'existence d'un pdf clair, en français et téléchargeable gratos sur la question, j'ai un doute. Je n'en ai jamais trouvé au cours de mes pérégrinations internautiques, mais cela ne veut pas dire qu'il n'en existe pas.
Bon courage
Martial

christophe c · June 2019

Si tu ne veux pas acheter de livre, tu implémentes Godel en lambda-calcul présenté sous la forme "logique combinatoire".

Les points fixes s'implémentent comme suit : $$

a:=(x\mapsto f(x(x)))

$$ puis, $$

p:=a(a)

$$ Ce qui te donne $a(a)=f(a(a))$.

En particulier avec $f:=(x\mapsto (NonProuvable(x)))$, tu as ta phrase cherchée, et tu peux jouer à volonté avec différents "NonProuvable" issus de tes caprices.

L'avantage de cette présentation est qu'elle s'implémente très bien et dans des sous-théories de Peano assez rudimentaires. Le point crucial, comme déjà dit, c'est le théorème chinois, qui te dit que pour toute suite $u$ d'entiers, et tout entier $n$, il existe $a,b,c$ entiers tels que $\forall i<n: $ le reste de $a$ par $b+ic$ est $u(i)$.

Maintenant, c'est un peu dommage de te prendre la tête, si tu veux juste prouver l'incomplétude de ZF, puisqu'il est trivial que ZF + "il existe un inaccessible" est strictement plus fort que ZF (ie que "il existe un inaccessible" n'est pas prouvable from ZF). Et aucune des classifications godéliennes n'est nécessaire pour le voir.

christophe c · June 2019

Remarque, il est mieux de passer par des pointeurs récursifs francs que par l'usage "consommateur" du lambda-calcul (qui a juste le mérite d'exister) pour créer un point fixe.

Le programme est :

[large]let a():= f(a())[/large]

Difficile de faire plus court.

Les gens s'en méfient (enfin s'en méfiaient, en 2019, je ne suis plus trop sûr) à cause du platonisme, mais ça "c'était avant" l'usage intensif de pointeurs bouclant.

David Olivier · June 2019

Merci pour vos réponses. J'ai lu et à peu près compris une esquisse de démonstration de Gödel dans Penrose, Les ombres de l'esprit; mais d'abord ce n'est qu'une esquisse, puis ça s'appuie sur les machines de Turing universelles - dont il ne démontre pas, je crois, l'existence - et enfin le résultat est en termes d'algorithmes, et je cherche à comprendre aussi l'approche en termes de systèmes d'axiomes.

J'ai l'impression que quand on a compris un domaine, on en fait facilement et spontanément des petits résumés comme ceux que vous faites ci-dessous, qui vous semblent clairs et significatifs mais qui n'apportent pas grand chose à qui n'a pas, justement, compris le domaine. Je pense par exemple au lemme de Zorn; avant d'étudier sa démonstration en bonne et due forme, je lisais de-ci de-là des explications en termes de «s'il n'y a pas d'élément maximal on peut continuer indéfiniment à agrandir la chaîne et ça devient trop grand pour tenir dans un ensemble». Ou encore «c'est comme les ordinaux, on ne peut pas les faire tenir dans un ensemble». Maintenant que j'ai compris (avec sueur) une vraie démonstration, ces explications me parlent et me semblent justes; mais avant, non, elles ne me parlaient pas, ou seulement de manière superficielle.

David Olivier · June 2019

Pour le bouquin (celui de Cori et Lascar), j'ai trouvé le second volume en PDF, mais pas le premier. Mais je l'ai repéré à l'ENS de Lyon, où ma femme pourra me l'emprunter. (Malheureusement, des fois les bibliothèques n'aiment pas qu'on gribouille sur les livres :-P.)

C'est pas que je ne veux pas dépenser les 43€ correspondants pour chaque volume dans l'absolu, mais je veux commencer par voir si c'est vraiment le bon livre pour moi. Si oui, je demanderai au Père Noël.

Foys · June 2019

Soit $\mathcal E$ un ensemble, $(A,B) \mapsto A \bullet B$ une loi de composition interne sur $\mathcal E$, $\sim$ une relation binaire sur $\mathcal E$ et $X \mapsto \ulcorner X \urcorner $ une fonction de $\mathcal E$ dans $\mathcal E$ (un "encodage" ou "numérotation de Gödel").

On suppose que pour tout $F\in \mathcal E$, il existe $F^* \in \mathcal E$ tel que pour tout $X\in \mathcal E$, $$F^* \bullet \ulcorner X\urcorner \sim F \bullet \ulcorner X \bullet \ulcorner X \urcorner \urcorner \tag{$\dagger$}$$.
Alors pour tout $G\in \mathcal E$, il existe $E \in \mathcal E$ tel que $E \sim G \bullet \ulcorner E\urcorner$.

Il suffit de prendre $E:= G^* \bullet \ulcorner G^* \urcorner$ et d'appliquer $(\dagger)$.

********************

C'est juste ça le théorème de point fixe (de Kleene...) et il a des milliers de déclinaisons dans la littérature.
Dans le cas de Gödel, $\mathcal E$ est l'ensemble des expressions écrites avec des symboles mathématiques, $\sim$ est une relation qui signifie "équivalents si ce sont des formules logiques", $F \bullet G$ est, lorsque $F$ est une formule à une seule variable libre (i.e. une propriété formalisable, ou "prédicat unaire"), la formule obtenue en remplaçant (sans capture) cette variable par $G$ et n'importe quoi sinon (par ex $F$...), et enfin, $\ulcorner X \urcorner$ est un codage de $X$ écrit avec des chiffres (par ex si les éléments de $\mathcal E$ sont écrits avec 1000 symboles différents $s_1,s_2,s_3 \ldots s_{999}, s_{1000}$, $\ulcorner s_{k_1}s_{k_2}\ldots s_{k_n} \urcorner = \overline{k_1 k_ 2 k_3 \ldots k_n}= \sum_{p=1}^n 10^{3(n-p)} k_p$).
L'idée étant que étant donné une propriété formalisable $F$, la théorie ambiante traite l'arithmétique de base de façon suffisamment fine pour construire une propriété $F^*$ à une variable libre $x$ (le nom de son argument) qui dit "s'il existe un $m$ dont $x$ est l'encodage alors $\ulcorner m \cdot \ulcorner m \urcorner\urcorner$ a la propriété $F$".
On a alors via le théorème de point fixe plus haut, pour toute propriété $G$, une formule $E$ qui dit "la formule d'encodage $\ulcorner E \urcorner$ vérifie la propriété $G$".

Lorsque $G(x)$ dit "la formule de numéro $x$ n'est pas prouvable", on a donc une formule qui dit d'elle même qu'elle n'est pas prouvable.
Noter aussi le théorème de Tarski qui dit que la vérité n'est pas définissable en arithmétique. Soit $V$ une propriété formalisable quelconque. Posons $G:= \neg V$. Alors il existe une formule $E$ qui dit "le numéro de $E$ n'a pas la propriété $V$" (ainsi $V$ ne pourra jamais signifier convenablement "ce nombre est celui d'une formule vraie").

************************

Le théorème de point fixe s'applique en informatique. Ici $A\bullet B$ désigne l'application de $A$ (vu comme un programme) à $B$ et $ \ulcorner X \urcorner $ est grosso modo la mise de $X$ sous forme de donnée non exécutable (guillemets ou autre... Penser à "(quote X)" dans scheme). "$\sim$" signifie "renvoient la même chose".
Alors on peut pour chaque programme $G$, construire un programme $E$ tel que $G \bullet \ulcorner E \urcorner$ font la même chose. (des "Quines" par exemple).

David Olivier · June 2019

Foys, je te remercie pour tes efforts pour m'éclairer, mais ça me passe nettement au-dessus

Romyna · June 2019

Gödel = $\nexists \{axiome_1, axiome_2, \ldots, axiome_i, \ldots, axiome_\infty\}$

christophe c · June 2019

@David, ce que foys essaie de te dire c'est que tu peux tout faire seul "assez facilement". Ca représente tout de même un sacré avantage de faire les choses soi-même, quand on peut.

Rien ne t'interdit de créer ta petite théorie proche de l'arithmétique, dans laquelle tu intègres la programmation.

La seule chose est que l'opération "exécute (n)" doit avoir quelques petites propriétés très connues et très simples à décrire.

Je te rappelle qu'implémente le paradigme informatique, c'est juste donner une fonction partielle de $\N\to \N$ (je prends les entiers puisque tu les aimes).

Tu as alors que le programme $n$ s'exécute comme suit:

$n;f(n);f(f(n));\dots$. C'est vraiment primitif.

Il s'arrête ssi l'un des $f^p(n)$ n'est pas dans l'ensemble de définition de $f$. L'entier sur lequel il s'arrête est le RESULTAT , et tu le notes $eval(n)$ (s'il ne s'arrête pas, tu dis qu'il boucle, ou tu inventes un autre mot).

Tu peux très bien voir tes programmes comme des fonctions comme suit:

$$ n[p] := ComposantImpair(eval (2^n(2p+1)))$$

La fonction $f$ est juste la fonction "hardware" qui indique ce qui se passe pour un cycle d'horloge (c'est la "ONE-STEP évolution" si tu veux)

Je pense que tu t'égares en croyant que la rigueur absente des exposés va t'apporter quelque chose. Rien à voir avec Zorn: la plupart des profs et de lycées et de fac et de prepa rameraient devant l'exercice

soit $f:\R\to \R$ définie sur $\R$, prouver qu'il existe une suite $u$ telle que $\forall n : u(n+1) = f(u(n))$ .

Mais là, rien de tel. Au contraire, non seulement il n'y a pas de surajout intuitif, mais il y a même du surretrait :-D

christophe c · June 2019

Et à toutes fins utiles, je te rappelle que $P$ est un théorème ssi il existe un axiome $A$ tel qu'on peut obtenir $P$ en partant de $A$ et en rabotant, où raboter veut juste dire:

si $X$ est de la forme $H\to Y$ avec $H$ axiome, on peut passer à $Y$ et continuer (ou s'arrêter). Sinon, $X$ n'est pas rabotable.

C'est tout ce qu'il y a de plus formel et même "scriptural" :-D et te ramène juste à la question d'implémenter .. les axiomes qui te font monter au rideau.

David Olivier · June 2019

Je l'ai!

(Le bouquin de Cori et l'autre Lascar, je veux dire, tome 1)

Merci pour vos conseils, ça me semble effectivement ce qu'il me faut!

christophe c · June 2019

Je te redonne une information que j'ai souvent mentionnée dans d'autres fils. J'appelle "sans façon" $T$ l'ensemble des théorèmes de maths. (En fait c'est une notion dynamique quand on change de théorie, mais peu importe, ça ne consiste qu'à ajouter ou retirer des axiomes à ZF). Je note $E$ l'ensemble des évidences (ie des conjonctions formelles d'axiomes).

$$ P\in T \iff (\exists X: [X\in E\ et\ ((X\to P)\in E)]) $$

Or les programmes qui reconnaissent les évidences se codent en 1h30 chrono, même par un débutant un programmation.

L'appel récursif $Q:= [\exists X: (X\in E\ et\ ([X\to nonQ]\in E)) ]$

te donne donc une phrase $Q$ telle que:

$Q$ dit qu'il existe une évidence $X$ telle que $X\to nonQ$ est aussi une évidence.

Les formalités qu'il y a à ajouter à ça sont quasiment et sans inspiration l'affaire de 2 à 3H, même pour un novice. Ce sera dommage que tu n'essaies pas ce "pèlerinage" une fois dans ta vie, non?