Accueil

Les théorèmes d'incomplétude de Gödel

Au cours de notre exploration de la logique classique, on a jeté les bases d'un système logique, en séparant ses aspects déductifs et sémantiques: le premier fixe les règles de manipulation qui permettent de passer "déductivement" d'une proposition (vue comme tas de symboles) à la suivante, et permet de prouver certaines propositions à partir d'autres; le second confère un sens à ces symboles, et permet de parler de propositions "vraies" ou "fausses". On avait établi un théorème de complétude, dû à Gödel, qui affirme que l'on peut prouver (au sens déductif) toute affirmation logique vraie (au sens sémantique).

Ce résultat était de bon augure pour Hilbert et les formalistes, qui souhaitaient l'étendre aux mathématiques: en ajoutant au système logique quelques axiomes mathématiques, comme Euclide l'avait fait pour la géométrie, on devrait pouvoir en déduire toute affirmation mathématique vraie.

Mais ce n'est pas pour ce résultat rassurant que Gödel est le plus connu. Vous avez peut-être plutôt entendu parler de ses théorèmes d'incomplétude, armés desquels il réduisit à néant les espoirs de Hilbert de trouver une fondation rigoureuse, cohérente et complète pour le spectaculaire édifice des mathématiques.

Fig.1 - Gödel contre les piliers des maths (vue d'artiste).

Mais ne vient-on pas de dire que le système logique était complet ? La distinction ici vient du fait qu'on s'intéresse maintenant aux mathématiques, et plus seulement à la logique. On ne peut pas décemment prétendre faire des mathématiques si on ne dispose pas, au moins, d'une façon de compter; plus pompeusement, on veut au moins pouvoir faire de l'arithmétique de base. On s'intéresse donc au langage formel de la théorie des nombres, $\mathcal L_{NT}$, déja introduit à l'épisode précédent et basé sur les symboles:

$$K_{NT}=\{0,S,+,\cdot\ ,<\}$$

On le munit de son interprétation usuelle, $\mathfrak N$, dont les objets sont les entiers et les opérations sont dotées de leur "sens" habituel. Comme il faut bien démarrer les déductions par quelque chose, on a besoin d'un ensemble d'axiomes $\Sigma$, qui soient:

  • d'une part, vrais dans notre modèle (c'est mieux), autrement dit $\mathfrak N \models \Sigma$;

  • d'autre part, suffisamment robustes pour pouvoir démontrer tout ce qui est vrai; autrement dit, tels que si $\mathfrak N \models \sigma$, alors $\Sigma \vdash \sigma$. Puisqu'une proposition $\sigma$ est soit vraie, soit fausse dans $\mathfrak N$ (c'est à-dire $\mathfrak N \models \sigma$ ou $\mathfrak N \models \neg \sigma$), ceci implique que pour toute proposition $\sigma$ du langage $\mathcal L_{NT}$, soit $\Sigma \vdash \sigma$ soit $\Sigma \nvdash \sigma$. Dans ce cas, on dit qe le système d'axiomes $\Sigma$ est complet.

Mais alors, pourrait dire un gros malin, je pose $Th(\mathfrak N)$ l'ensemble des propositions vraies dans $\mathfrak N$, et mon système d'axiomes, c'est $Th(\mathfrak N)$. Là, pour être complet, pas de problème, on est complet !

Quel est le problème avec cette solution ? On a envie de dire que c'est là un système d'axiome déraisonnable, beacuoup trop gros. Et pourquoi est-ce un problème ? Parce que si je donne au gros malin une proposition arithmétique, par exemple Il existe une infinité de paires de nombres premiers de la forme $(p, p+2)$", il aura du mal à me dire si c'est un axiome ou pas.

Un système d'axiomes raisonnable devrait être décidable, c'est-à-dire qu'on doit disposer d'une procédure qui nous permette de déterminer si une proposition est un axiome ou pas, et avant l'heure du thé, s'il vous plaît.

Ce qu'affirme le premier théorème d'incomplétude de Gödel, c'est que pour tout système d'axiomes $A$ décidable, cohérent, et suffisamment complexe pour nous permettre de compter efficacement des patates, il existe une proposition $\sigma$, telle que $\mathfrak N \vDash \sigma$ (vraie dans $\mathfrak N$, donc), et telle que $A\nvdash \sigma$ ($A$ ne démontre pas $\sigma$).

Comment prouve-t-on une chose pareille ? L'idée de génie de Gödel est de construire dans le langage $\mathcal L_{NT}$ une proposition $\theta$ qui affirme "je ne suis pas démontrable". Pour cela, il nous faut deux choses:

  • Premièrement, une façon de parler à l'intérieur du langage $\mathcal L_{NT}$ de ce qui est démontrable à partir de $A$.
  • Deuxièmement, une façon de faire dire "je" à une formule d'arithmétique.

L'idée de génie suivante est de remarquer que, puisque l'arithmétique est outillée pour parler des entiers, on devrait essayer de représenter "je" et "démontrable" à l'aide d'entiers. C'est à dire, on va mettre au point un code qui nous permette d'associer, à chaque formule, axiome ou déduction, un (grand) entier. Ainsi, $\theta$ pourra parler de son propre code, et affirmer qu'il ne fait pas partie de l'ensemble des entiers qui codent pour des propositions démontrables.

La suite de cette page va tenter d'expliquer les grandes lignes de la preuve du premier théorème d'incomplétude, en cachant au maximum sous le tapis tout ce qui est trop technique. Avant de commencer, une distinction essentielle s'impose:

Puisque l'on cherche une proposition vraie (au sens sémantique) mais non prouvable (au sens déductif), il va être crucial de séparer le langage $\mathcal L_{NT}$ de son interprétation. Ainsi, "42" est un élément de l'interprétation sémantique $\mathfrak N$, mais ne signifie rien dans $\mathcal L_{NT}$: ce n'est ni une constante (seul 0 est une constante de ce langage), ni une variable. Dans le langage $\mathcal L_{NT}$, ce que l'on interprète dans $\mathfrak N$ comme 42 est le terme

$$\underbrace{SS\dots SS}_{42 \text{ fois}}0$$

ce qui est, pour le dire poliment, un peu lourd. On notera donc ce terme $\overline{42}$ et plus généralement, pour un entier $a$, on notera

$$\bar a := \underbrace{SS\dots SS}_{a \text{ fois}}0$$

L'une des difficultés de la preuve (ou disons, de la version édulcorée présentée ici) est de garder en tête à tout moment la distinction entre l'entier $a$ et le terme du langage $\bar a$.

Le système d'axiomes $N$

Tout d'abord, on va préciser ce que l'on entend par "faire de l'arithmétique simple". C'est à dire qu'on va considérer un système d'axiomes (non-logiques; voir la page sur les systèmes déductifs pour une liste des axiomes logiques) qui donne aux symboles 0, $S$ ("successeur"), +, et $\cdot$ les propriétés qu'on attend d'eux. On appelera $N$ ce système, consistant en les propositions suivantes:

  1. 0 n'est le successeur de personne: $(\forall x) \neg Sx = 0$
  2. Deux entiers qui ont le même successeur sont égaux: $\forall x,\ \forall y,(Sx= Sy \Rightarrow x=y)$
  3. Additionner 0 ne change rien: $\forall x, (x+0 = x)$
  4. Définition de l'addition par récurrence (comment déduire $x+Sy$ de $x+y$): $\forall x,\ \forall y,(x+ Sy =S(x+y))$
  5. Multiplier par 0 donne toujours 0: $\forall x,\ x\cdot 0 = 0$
  6. Définition de la multiplication par récurrence: $\forall x,\ \forall y,(x \cdot Sy = x\cdot y + x)$
  7. Aucun élément n'est plus petit que 0: $\forall x,\ \neg x<0$
  8. Définition "par récurrence" de l'ordre: $\forall x,\ \forall y,(x< Sy \Leftrightarrow (x=y \text{ ou } x< y))$
  9. On peut toujours utiliser $<$ pour comparer deux éléments différents: $\forall x,\ \forall y,(x< y \text{ ou } x=y \text{ ou } y< x)$

Le slogan est donc, clairement, "si on a pas ça, on n'a pas grand chose". Puisque toutes ces propositions énoncent des choses vraies sur les entiers tels qu'on les connaît, toute axiomatisation intéressante $A$ va certainement récupérer ces propriétés, autrement dit, $A\vdash N$, et donc toutes les conséquences de $N$.

Que peut-on déduire de $N$, au juste ? Pour commencer, si $a=b$ (dans $\mathfrak N$, donc), alors on a bien $N \vdash \bar{a} = \bar{b}$, et de même si $a< b$. Les opérations de bases ont aussi bien les interprétations que l'on souhaite:

$$\begin{align} N &\vdash \bar a + \bar b = \overline{a+b}\\ N &\vdash \bar a \cdot \bar b = \overline{a\cdot b} \end{align} $$

Toutefois, $N$ demeure assez limité: par exemple, il ne suffit pas à prouver qu'on peut additioner des enters dans l'ordre qu'on veut; autrement dit, $N \nvdash \forall x, \forall y,\ x+y = y+x$. C'est à dire que $N$ peut démontrer $\bar a + \bar b = \bar b + \bar a$ pour toute paire spécifique d'entiers, mais pas démontrer la propriété générale.

Puisque c'est précisément ce que $N$ peut démontrer ou pas qui nous intéresse, essayons de le comprendre un peu mieux. On va trier les propositions en fonction de leur complexité, et on verra à partir de quel niveau de complexité $N$ commence à s'essouffler.

Complexité des propositions

Puisque $N$ gère très bien les paires d'entiers spécifiques, on s'attend à ce que des propositions portant sur un entier, ou un nombre fini d'entre eux, ne lui posent pas trop de problèmes. De fait, la distinction essentielle entre formules "simples" et formules "compliquées" va distinguer les quantificateurs bornés, tels que $\forall x< t$ ou $\exists x < t$, et les quantificateurs non bornés comme $\forall y$, qui portent sur tous les entiers. L'existence non bornée $\exists x$ va avoir un statut ambigu: pour montrer une telle propriété, il suffit d'exhiber le bon $x$: s'il existe, cela se fait en temps fini, mais sinon, on peut chercher longtemps...ce quantificateur, intuitivement, donnera des formules plus faciles à montrer si elles sont vraies qu'à réfuter si elles sont fausses.

On va donner des noms à ces différents types de formules. Comme on l'a massivement fait précédemment, on va procéder par récurrence sur nombre de symboles logiques utilisés. On commence par les formules "faciles à démontrer, difficiles à réfuter".

On dira que $\phi$ est une $\Sigma$-formule si:

  • $\phi$ est une formule atomique;
  • $\phi$ est la négation d'une formule atomique;
  • $\phi$ est de la forme $\alpha \vee \beta$ ou $\alpha \& \beta$ pour deux $\Sigma$-formules $\alpha$ et $\beta$;
  • $\phi$ est de la forme $\exists x < t, \alpha$, $\forall x < t, \alpha$,$\exists x \leq t, \alpha$,$\forall x \leq t, \alpha$, où $\alpha$ est une $\Sigma$-formule, et $x$ une variable n'apparaissant nulle part dans le terme $t$;
  • $\phi = \exists x \alpha$, où $\alpha$ est une $\Sigma$-formule et $x$ une variable.

Les formules difficiles seront donc les négations des $\Sigma$-formules. On les définit comme suit:

On dira que $\phi$ est une $\Pi$-formule si:

  • $\phi$ est une formule atomique;
  • $\phi$ est la négation d'une formule atomique;
  • $\phi$ est de la forme $\alpha \vee \beta$ ou $\alpha \& \beta$ pour deux $\Pi$-formules $\alpha$ et $\beta$;
  • $\phi$ est de la forme $\exists x < t, \alpha$, $\forall x < t, \alpha$,$\exists x \leq t, \alpha$,$\forall x \leq t, \alpha$, où $\alpha$ est une $\Pi$-formule, et $x$ une variable n'apparaissant nulle part dans le terme $t$;
  • $\phi = \forall x \alpha$, où $\alpha$ est une $\Pi$-formule et $x$ une variable.

Enfin, les formules les plus gentilles sont celles où tous les quantificateurs sont bornés: ce sont les $\Delta$-formules, celles qui sont à la fois $\Sigma$ et $\Pi$.

Codage

Une façon commune, vers 12 ans, d'encrypter d'une façon impénétrable d'importantes communications sur qui est le plus mignon de la classe, est tout simplement de remplacer chaque lettre par un nombre, par exemple sa place dans l'alphabet. Ainsi,

$$22\ 9\ 3\ 20\ 15\ 18$$

signifie "Victor". En supprimant les espaces, on obtient un (gros) entier 2293201518, qui fait partie du domaine de $\mathfrak N$: autrement dit, on peut, à l'intérieur de notre langage, énoncer des propriétés de cet entier. Par exemple, appartient-il à l'ensemble des entiers pairs ? des entiers premiers ? Et si l'on pouvait caractériser l'ensemble des nombres qui codent des propositions déductibles du système d'axiomes $A$, on pourrait se demander si notre entier en fait partie, et donc s'il représente un théorème de $A$.

Gödel, qui n'avait, semble-t-il, pas d'avis sur le plus mignon, préférait coder des propositions arithmétiques, aussi attribue-t-il un code pour chaque symbole du langage $\mathcal L_{NT}$:

Symbole Code Symbole Code
$\neg$ 1 + 13
$\vee$ 3 $\cdot$ 15
$\forall$ 5 < 17
= 7 ( 19
0 9 ) 21
S 11 $x_i$ $2i$

Comme les tableaux en HTML, c'est pénible, on réduit le langage à sa plus simple expression: ainsi, puisque les "et" sont logiquement équivalents à des négations de "ou", et les "$\exists$" à des négations de "$\forall$", on a juste besoin de ces derniers. Aussi, on considère que l'ensemble des variables est donné par $Var=\{x_1, x_2,\dots\}$.

Ainsi, une formule -qui n'est jamais qu'une suite de symboles- sera représentée par une suite d'entiers. Ainsi, "$S0 = 0$" donne (11,9,7,9). Pour former un unique entier à partir de là, on pourrait simplement retirer les virgules, mais cela poserait des problèmes de décodage: 11979 représente-t-il "$S0=0$" ou "$\neg (=0$"?

Gödel, qui décidément aimait beaucoup l'arithmétique, se sort de là en utilisant le Théorème Fondamental de l'Arithmétique: tout entier naturel $n$ admet une unique décomposition en facteurs premiers. Autrement dit, tout entier $n$ peut s'écrire

$$n = 2^{\alpha_1} \cdot 3^{\alpha_2}\cdot 5^{\alpha_3}\dots$$

et les exposants $\alpha_i$ sont entièrement définis par $n$: si on connaît $n$, on peut retrouver les $\alpha_i$. Donc, en reprenant notre séquence (11,9,7,9), on peut lui associer l'entier

$$[11,9,7,9]:=2^{11}3^9 5^7 7^9 = 127084807452960000000$$

En utilisant cette notation, on va encoder les formules en procédant, comme toujours, par induction sur leur degré dé complication. Si $\phi$ est une suite de symboles, on lui associe son entier de Gödel $[\phi]$ comme suit:

$$ [\phi] := \begin{cases} [1,[\alpha]] \text{ si } \phi : \neg \alpha\\ [3,[\alpha], [\beta]] \text{ si } \phi : \alpha \vee \beta\\ [5,[x_i],[\alpha]] \text{ si } \phi : \forall x_i \alpha\\ [7,[t_1],[t_2]] \text{ si } \phi : t_1 = t_2 \\ [9] \text{ si } \phi: 0\\ [11,[t]] \text{ si } \phi : St\\ [13,[t_1],[t_2]] \text{ si } \phi : t_1 + t_2\\ [15,[t_1],[t_2]] \text{ si } \phi : t_1 \cdot t_2\\ [17,[t_1],[t_2]] \text{ si } \phi : t_1 < t_2\\ [2i] \text{ si } \phi \text{ est la variable }x_i\\ 3, \text{ dans tous les autres cas.} \end{cases} $$

Et inversement, si on nous donne un entier $n$, il "suffira" de le décomposer en ses facteurs premiers. Alors, soit tous les nombres premiers jusqu'à $p_k$ apparaissent dans la décomposition, par exemple

$$n= 2^7\cdot 3^{512} \cdot 5^{512}$$

où apparaissent 2,3, et 5, et donc tous les nombres premiers jusqu'à 5 apparaissent; soit il en manque, par exemple

$$n=3^4 \cdot 7^2$$

où il "manque" 2 et 5. Dans le premier cas, $n$ représente une formule, en l'occurence $0 = 0$; dans le second, ce n'est pas le cas (sinon, le premier symbole de cette formule donnerait un $2^{\text{quelque chose}}$ au début de la décomposition de $n$, donc il ne peut pas ne pas y avoir 2).

Ce système donne très vite de très, TRES grands nombres: par exemple, la formule "$\neg 0=S0$" est encodée par

$$\begin{align} [\neg 0=S0] &= [1,[0=S0]]=2\cdot 3^{[0=S0]} = 2\cdot 3^{[7,[0], [S0]]} = 2\cdot 3^{[7,2^9, 2^{11}\cdot 3^{2^9}]}\\ &=2 \cdot 3^{2^7\cdot 3^{2^9}\cdot 5^{2^{11}\cdot 3^{2^9}}} \end{align} $$

Ensembles représentables

Mais la question n'est pas tant de savoir si nous pouvons reconnaître et décoder les entiers représentant des formules, que de savoir si notre système d'axiome le peut. Autrement dit, peut-on déduire des axiomes de $N$ qu'un entier donné, $\overline{127084807452960000000} $ par exemple, appartient à l'ensemble des entiers codant une formule ?

Cette question nous amène à considérer les ensembles d'entiers, et à nous demander lesquels $N$ "reconnaît". On les appellera des ensembles "représentables". Plus précisément, un ensemble $E\subset \mathbb N$ est représentable s'il existe une formule $\phi$ de $\mathcal L_{NT}$ telle que:

$$\begin{cases} \forall a \in E,&\ N\vdash \phi(\overline{a}) \\ \forall b \notin E,&\ N\vdash \neg \phi(\overline{b}) \end{cases}$$

Autrement dit, la formule $\phi(\bar a)$ est démontrable à partir des axiomes de $N$ si l'entier $a$ est bien dans l'ensemble $E$, et réfutable dans le cas contraire.

L'équivalent sémantique, ce sont les ensembles dont on sait "parler": on les appellera les ensembles définissables. Plus précisément, un sous-ensemble $E$ de $\mathbb N$ est définissable s'il existe une formule $\phi$ de $\mathcal L_{NT}$ telle que:

$$\begin{cases} \forall a \in E,&\ \mathfrak N\vDash \phi(\overline{a}) \\ \forall b \notin E,&\mathfrak N\nvDash \neg \phi(\overline{b}) \end{cases}$$

En particulier, tous les ensembles représentables sont définissables, par la formule qui les représente. En revanche, l'inverse n'est pas vrai en général. La question se pose donc: quels ensembles définissables sont aussi représentables ? Et ceci nous ramène à la distinction entre propositions vraies et propositions démontrables à partir de $N$, et aux $\Sigma, \Pi$ et $\Delta$-formules introduites un peu plus haut.

Une étape importante de la preuve consiste à prouver que $N$ est assez puissant pour démontrer toutes les $\Sigma$-formules vraies: dit plus "rigoureusement", si $\phi(x)$ est une $\Sigma$-formule, dépendant de variables $x=(x_{i_1}\dots x_{i_k})$, et si $t=(t_{i_1}\dots t_{i_k})$, alors, si $\mathfrak N \vDash \phi(t)$, $N \vdash \phi(t)$.

La définition des $\Sigma$-formules étant inductive, on prouve ce résultat par induction sur le nombre d'étapes utilisées pour construire $\phi$ à partir de formules atomiques (ce type de preuve a été massivement utilisé dans l'épisode précédent). Quant aux formules atomiques, qui sont de la forme $x_1 < x_{38}$ ou encore $S0 + S0 = SS0$, on les traite individuellement à partir des axiomes de $N$.

En particulier, toutes les formules ne faisant intervenir que des quantificateurs bornés (les $\Delta$-formules) sont démontrables dès lors qu'elles sont vraies. Comme la négation d'une $\Delta$-formule est aussi une $\Delta$-formule, on en déduit que non seulement les $\Delta$-formules vraies sont démontrables, mais de plus, les $\Delta$-formules fausses sont réfutables: si $\mathfrak N \vDash \neg \phi(t)$, alors $N \vdash \neg \phi(t)$.

En particulier, pour revenir aux ensembles dont $N$ peut déterminer les membres, si $E$ est défini (au sens de définissable, comme ci-dessus) par une $\Delta$-formule, alors il est représentable.

Puisque les $\Delta$-formules, et leurs quantificateurs bornés, sont décidément très sympathiques, il va s'avérer crucial de trouver des bornes. Par exemple, supposons que l'on veuille décrire les entiers pairs. La première formule qui vient à l'esprit pour affirmer que $x$ est pair serait

$$\phi(x):\ \exists y,\ x=y+y$$

C'est une $\Sigma$-formule, ce qui est déjà pas mal; mais on peut faire mieux en observant que $y$ est forcément plus petit que $x$, donc $\phi(x)$ est équivalente à:

$$\text{EstPair}(x):\ \exists y\leq x,\ x=y+y$$

qui nous donne une $\Delta$-formule définissant l'ensemble des entiers pairs. On peut de même définir des $\Delta$-formules qui reconnaissent les entiers pairs, ou encore une $\Delta$-formule PremiersSuccessifs$(x,y)$ qui reconnaît les paires d'entiers premiers consécutifs $(x,y)$ ou EstDivisible$(x,y)$ qui est vraie si $x$ divise $y$.

Plus en rapport avec notre problème, un peu d'astuce nous donne $\Delta$-formule qui détecte les codes de formules:

$$\begin{align} &\text{EstUnCode}(c) = \text{EstDivisible}(SS0,c)\ \& \\ & \forall z< c,\ \forall y< z, \\ & (\text{EstPremier}(z) \& \text{EstDivisible}(z,c) \& \text{PremiersSuccessifs}(y,z)) \Rightarrow \text{EstDivisible}(y,c)) \end{align}$$


Avec un peu d'astuce, on peut décrire une formule de "décodage" $\text{i-èmeElément}(a,i,c)$ qui vérifie si $e$ est le i-ème élément d'une suite d'entiers encodée par $c$ selon ce procédé (en tant qu'exposant du i-ème nombre premier).

On a aussi très facilement une formule permettant de reconnaître les codes des variables $x_i$, puisqu'ils sont de la forme $2^{2i}$. Plus généralement, pour reconnaître un entier qui encode un terme de $\mathcal L_{NT}$, on utilise une fois encore le principe d'induction sur la complexité. Etant donné un terme $t$, par exemple $0+Sx_1$, on lui associe une "suite de construction": une suite de termes de plus en plus complexes qui décrivent comment on "construit" $t$. Ici, par exemple, une suite de construction pour $t$ serait

$$(x_1, Sx_1, 0, 0+Sx_1)$$

auquel on associe la suite d'entiers de Gödel

$$([x_1], [Sx_1], [0], [0+Sx_1])$$

qui est elle-même codée par

$$[[x_1], [Sx_1], [0], [0+Sx_1]]$$

Avertissement: tenter de se représenter ce genre de nombres peut occasionner une crampe à l'hypothalamus.

En utilisant la fonction de décodage, on peut alors écrire une $\Delta$-formule qui pique un peu les yeux mais reconnaît si un entier $c$ code une suite de construction pour un terme codé par $a$:

$$\begin{align} &\text{ConstructionTerme}(c,a) = \text{EstUnCode}(c)\ \& \exists l< c \\ & \bigg[ \text{Longueur}(c)=l \& \text{ i-èmeElément}(a,l,c) \& \\ &\forall e< c\ \forall i \leq l \bigg(\text{i-èmeElement}(e,i,c) \Rightarrow\text{Variable}(e) \vee\ e=\bar 2^{\bar{9}}\ \vee\ (\exists j< i\ \exists k< i\ \exists e_j < c\ \exists e_k < c \\ &(\text{i-èmeElément}(e_j,j,c)\ \& \text{i-èmeElément}(e_k,k,c) \& \\ &[e=e_j \vee e=\bar2^{\bar 11}\cdot \bar 3^{e_j} \ \vee \ e = \bar 2^{\bar{13}}\cdot \bar 3^{e_j} \cdot \bar 5^{e_k} \vee e = \bar2^{\bar{15}}\cdot \bar 3^{e_j} \cdot \bar 5^{e_k} ]))\bigg) \bigg] \end{align}$$


Une fois passé le déni, la colère et le désespoir, on atteint une phase d'acceptation lorsqu'on s'aperçoit que cette formule vérifie que $c$ encode une suite d'entiers de longueur $l$, dont le dernier encode $a$, et tel que, si $e$ est en position $i$, alors $e$ encode $0$, une variable, un terme précédemment recontré (on autorise les suites de construction à se répéter), ou alors résulte de l'application de $S$, + ou $\cdot$ à des termes précédents. Et on peut borner tous les quantificateurs.

Maintenant que l'on sait reconnaître des constructions de termes, on peut aussi reconnaître les codes des termes eux-mêmes: ce sont les paquets de symboles pour lesquels il existe une suite de construction, autrement dit les $a$ tels que $ \exists c,\ \text{ConstructionTerme}(c,a)$.

Mais cette dernière formule est une $\Sigma$-formule: on peut mieux faire, si on arrive à borner le quantificateur $\exists c$. Un peu d'astuce et beaucoup de calculs montrent que l'on peut effectivement borner le nombre de membres de la plus petite formule de construction possible pour un terme $t$, en fonction de $[t]$. En utilisant cette borne, on obtient une $\Delta$-formule qui est vraie si $a$ code pour un terme:

$$\text{EstUnTerme(a)}= \exists c < ((\bar 2^{a^a})^{a^\bar{2}+ a}),\ \text{ConstructionTerme}(c,a)$$

Cette idée des suites de constructions permet d'exploiter la nature récursive de la plupart des définitions de la logique classique. On l'utilise aussi pour définir une formule $\text{Num}(a,y)$ qui est vraie si $y=[\bar{a}]$ (c'est-à-dire si $y$ est le code pour le nombre de Gödel du terme qui représente l'entier $a$ dans $\mathcal{L}_{NT}$), via la séquence de construction $$(0, S0, SS0\dots, \underbrace{S\dots S}_{a\text{ fois}}0 )$$.

On peut aussi l'utiliser, d'une façon plus créative, pour générer une formule $\text{Substitution}([\alpha],[x],[t],y)$ qui est vraie si $y=[\alpha(x|t)]$, autrement dit si $y$ encode la formule $\alpha$ où l'on a substitué le terme $t$ partout où apparaissait la variable $x$.

On ne donnera pas la formule ici, car ce serait du pur sadisme, mais l'idée est de partir d'une suite de construction de $\alpha$, de substituer $t$ partout où $x$ apparaît, et de faire précéder le tout d'une suite de construction pour $t$ (afin qu'au total, on obtienne une suite de construction pour $\alpha(x|t)$). On applique alors le même procédé que pour $\text{EstUnTerme}$ et $\text{Num}$: on trouve une borne pour la longueur totale de la suite obtenue en fonction de $\alpha$, $x$ et $t$, et on reconnaît une substitution quand il existe une suite de construction correspondante.


En utilisant cette dernière fonction, et beaucoup d'aspirine, on montre que l'ensemble des nombres de Gödel des axiomes logiques et règles d'inférence est lui aussi représentable (par une formule que seul Nyarlathotep, Grand Ancien du Chaos Rampant, ne peut contempler sans que ses yeux ne fondent).

Plus reposant: puisque les axiomes de N sont en nombre fini, ils sont représentés par un ensemble fini d'entiers de Gödel qui est, bien sûr, représentable (Devinette: pourquoi ?).

Toutefois, on ne souhaite pas se restreindre à N, mais envisager des systèmes d'axiomes qui sont au moins aussi forts. On avait aussi évoqué en introduction le fait que c'est quand même pas mal de pouvoir déterminer si une proposition donnée est ou pas un axiome. C'est le moment de formaliser cette idée: on dira qu'un système d'axiomes $A$ est "pas déconnant" si l'ensemble $\{[\alpha], \alpha \in A \}$ est représentable.

Et si l'on peut reconnaître les nombres de Gödel, des propositions d'une part, et des axiomes et règles de déduction d'autre part, alors on doit pouvoir coder les démonstrations valides dans N d'une façon qui, elle aussi, sera représentable.

Plus précisément, considérons une suite $D=(\phi_1,\dots,\phi_n)$ de propositions. On lui associe la suite d'entiers $([\phi_1],\dots,[\phi_n])$, et on va associer un code à cette suite. On sait reconnaître les formules valides car elles font intervenir tous les nombres premiers à partir de 2, et les tas de symboles sans signification car ils commencent par 3. Pour les codes de déduction, on va donc commencer par 5:

$$[D]=5^{[\phi_1]}\cdot 7^{[\phi_2]}\cdot 11^{[\phi_3]}\dots$$

Il ne nous reste plus alors qu'à définir une formule $\text{Déduction}(n,a)$ (dont on dit que l'énoncer à haute voix a causé la chute de civilisations entières) qui, étant donné un entier $n$, est vraie si cet entier encode une suite de propositions qui sont soit des axiomes, soit obtenues à partir des précédentes en appliquant les règles d'induction, et dont la dernière est codée par $a$.

Mais une déduction, c'est en quelque sorte une suite de construction pour un théorème. En répétant le procédé, on peut alors définir une formule

$$\text{EstUnThéorème}(a): \exists c,\text{Déduction}(c,a)$$

Mais cette formule n'est pas une $\Delta$-formule: son quantificateur n'est pas borné, et aucun degré d'astuce ne nous permettra de le faire: il n'y a pas de taille maximum à la longueur d'une démonstration (à la grande détresse de moult mathématiciens).

La preuve de Gödel (en gros)

Maintenant, en utilisant ce qu'on a construit jusqu'ici, on va être en mesure de construire cette fameuse formule qui dit "je ne suis pas un théorème". On a déjà obtenu la partie "pas un théorème" à la section précédente: c'est la négation de $\text{EstUnThéorème}$ (observons au passage que $\text{EstUnThéorème}$ est une $\Sigma$-formule, donc sa négation est une $\Pi$-formule, comme on s'y attendait).

Il nous reste à donner à une formule un moyen de dire "je": c'est ce que fait le lemme d'autoréférence de Gödel.


Plus précisément, ce lemme s'énonce comme suit:

Si $\psi(x_1)$ est une formule dont la seule variable libre est $x_1$, alors il existe une formule $\phi$ telle que $N\vdash \phi \Leftrightarrow \psi(\overline{[\phi]})$.


Autrement dit, si $\psi$ est une des nombreuses formules vues jusqu'ici qui décrivent des propriétés des propositions à partir de leur nombre de Gödel, alors $\phi$ est une formule qui dit "je vérifie $\psi$".

On va utiliser nos formules $\text{Num}(a,y)$, vraie si $y=[\bar{a}]$ et $\text{Substitution}([\alpha],[x],[t],y)$, vraie si $y=[\alpha(x|t)]$. Considérons la formule $\gamma(x_1)$ définie par $$\gamma(x_1): \forall y \forall z(\text{Num}(x_1,y) \& \text{Substitution}(x_1,\bar 4,y,z)) \Rightarrow \psi(z),$$ où, rappelons-le, 4 est le code pour $x_1$. Que dit $\gamma(n)$ si $n$ code une proposition $\alpha$? La première hypothèse de l'implication dit que $y= [\overline{[\alpha]}]$, et la seconde que $z=[\alpha(x_1|\overline{[\alpha]})]$. Autrement dit, $z$ est le nombre de Gödel de la proposition obtenue en remplaçant tous les $x_1$ dans $\alpha$ par $[\alpha]$.
Choisissons maintenant $m=[\gamma(x_1)]$ et posons $\phi=\gamma(\bar{m})$. Alors, $\text{Substitution}(m,\bar 4,[\bar{m}],z))$ est vraie ssi $z$ code pour la proposition $\gamma(x_1)(x_1|\bar{m})= \gamma(\bar{m}) = \phi$. Avec ceci en tête, on obtient: $$\begin{align} \phi &\Leftrightarrow \forall y \forall z(\text{Num}(\bar{m},y) \& \text{Substitution}(m,\bar 4,y,z)) \Rightarrow \psi(z) \\ &\Leftrightarrow \forall y \forall z(y=[\overline{[m]}] \& \text{Substitution}(m,\bar 4,y,z)) \Rightarrow \psi(z)\\ &\Leftrightarrow \forall z(\text{Substitution}(m,\bar 4,[\overline{[m]}],z)) \Rightarrow \psi(z)\\ &\Leftrightarrow \forall z(z=[\phi]) \Rightarrow \psi(z)\\ &\Leftrightarrow \psi([\phi]), \end{align}$$ comme on le souhaitait.


On est enfin en mesure d'énoncer et de démontrer le Premier Théorème d'Incomplétude de Gödel.

Si A est un ensemble d'axiomes du langage $\mathcal L_{NT}$ qui soit cohérent et pas déconnant au sens défini plus haut, alors il existe une proposition $\theta$ telle que $\mathfrak N \vDash \theta$ mais $A \nvdash \theta$.

On suppose que A est assez fort pour démontrer les axiomes de N (si ce n'est pas le cas, on prend pour $\theta$ l'un de ces axiomes que A ne démontre pas). Rappelons qu'on a une formule qui détecte les théorèmes: la formule $\text{EstUnThéorème}(a)$ dont la construction a été évoquée, non sans un certain mal aux cheveux, dans la section précédente. Mais alors, d'après le lemme d'autoréférence, il existe une formule $\theta$ telle que $$N \vdash(\theta \Leftrightarrow \neg\text{EstUnThéorème}([\theta]))$$ Autrement dit, $\theta$ affirme fièrement "je ne suis pas un théorème". Puisque cette équivalence est démontrable, elle doit être vraie, comme on l'a vu ici; autrement dit $$\mathfrak N \vDash(\theta \Leftrightarrow \neg\text{EstUnThéorème}([\theta]))$$ Alors, $$\begin{align} \mathfrak N \vDash \theta &\text{ ssi } \mathfrak N \vDash \neg\text{EstUnThéorème}([\theta]) \\ &\text{ ssi } \mathfrak N \nvDash \text{EstUnThéorème}([\theta])\\ &\text{ ssi } [\theta] \text{ ne code pas une proposition démontrable,} \end{align}$$ ce qui est vrai si, et seulement si $A\nvdash \theta$. Donc, soit $\theta$ est vraie dans $\mathfrak N$ et on ne peut pas la démontrer à partir de A, soit $\theta$ est fausse dans $\mathfrak N$ et $A \vdash \theta$.
Or, dans ce dernier cas, $\text{EstUnThéorème}([\theta])$ est une $\Sigma$-formule qui est vraie dans $\mathfrak N$. On a vu que N peut démontrer les $\Sigma$-formules vraies, donc $N \vdash \text{EstUnThéorème}([\theta])$. Mais alors, $N \vdash \neg \theta$, par définition de $\theta$, et donc, comme A est plus fort, $A \vdash \neg \theta$. Mais on a supposé que $A \vdash \theta$: A démontre donc une contradiction, autrement dit, il est incohérent.
Au final, soit A n'est pas cohérent, soit $\theta$ est vraie, mais pas démontrable à partir de A.

Le second théorème d'incomplétude

Un formaliste optimiste pourrait tenter de réparer les dégâts en admettant que bon, très bien, aucun système d'axiomes n'est complètement complet. Mais quand même, cette formule qui dit "je ne suis pas un théorème", il a fallu aller la chercher dans les tréfonds de ce qui est autorisé dans le langage, à grands coups de lemme d'autoréférence. Mais les propositions intéressantes, qui parlent de maths, et pas d'elles-mêmes, sont certainement prouvables, non ?

Une proposition particulièrement intéressante pour Hilbert est celle de la cohérence des mathématiques. Si on la prouve, cela signifie que les mathématiques ne contiennent pas de contradiction. Un talisman contre le barbier de Russell et ses rejetons infernaux. Cette preuve devrait fonctionner notamment pour le système d'axiomes de Peano, le plus couramment utilisé comme base de l'arithmétique.

Ce système d'axiome contient les axiomes de $N$ et lui ajoute le principe de récurrence, utilisé si souvent qu'on en vient à oublier sa puissance. Ce principe dit qu'une propriété $\phi$ qui est vérifiée par l'entier 0, et telle que, si elle est vérifiée par $n$, l'est aussi par $Sn = n+1$, alors elle est vraie pour tous les entiers. Plus formellement:

$$\left[\phi(0)\ \&\ \, \forall x (\phi(x) \Rightarrow \phi(Sx))\right] \Rightarrow \forall x \ \phi(x)$$

C'est alors que Gödel arrive juché sur un second bulldozer: le second théorème d'incomplétude. Il annihile cet espoir, en démontrant que, parmi les propositions vraies mais non démontrables d'un système d'axiome au moins aussi fort que celui de Peano, figure l'affirmation de sa propre cohérence.

Ce qui enterre l'arithmétique de Peano, c'est en fait sa propre puissance. Un théorème crucial, dû à Löb, montre que le système de Peano (qu'on notera PA), est assez fort pour démontrer certains faits à propos de sa propre force. Plus précisément, pour toute formule $\phi$:

  1. D1: Si PA permet de démontrer $\phi$, alors PA peut démontrer qu'il peut démontrer $\phi$. Avec le codage de Gödel: si $PA \vdash \phi$, alors $PA \vdash EstUnThéorème_{PA}(\overline{[\phi]})$.
  2. D2: PA permet de démontrer que s'il y a une preuve de $\phi$, alors il y a une preuve qu'il y a une preuve de $\phi$. Autrement dit, $PA \vdash EstUnThéorème_{PA}(\overline{[\phi]}) \Rightarrow EstUnThéorème_{PA}(\overline{[EstUnThéorème_{PA}(\overline{[\phi]}]})$.
  3. D3:Enfin, PA montre que, s'il existe une preuve de $\phi$ et une preuve que $\phi \Rightarrow \psi$, alors il existe une preuve de $\psi$. Formellement, $PA \vdash \bigg(EstUnThéorème_{PA}(\overline{[\phi]})\, \&\, EstUnThéorème_{PA}(\overline{[\phi\Rightarrow \psi]})\bigg) \Rightarrow EstUnThéorème_{PA}(\overline{[\psi]})$.

En quoi le fait que PA se connaisse si bien lui-même est-il un problème ? En manipulant habilement ces 3 conditions, on montre que la proposition $\theta$ "je ne suis pas un théorème" fournie par le premier théorème de Gödel est équivalente à l'affirmation de la cohérence de PA; alors, si on avait une preuve de la cohérence, D3 nous fournirait une preuve de $\theta$...donc non.

Pour raffiner cette idée, commençons par formaliser l'affirmation de cohérence. On notera $\perp$ une contradiction quelconque, par exemple $\perp: (0=0)\&\neg(0=0)$. Alors la cohérence, c'est de ne pas pouvoir aboutir à $\perp$ par une déduction. Autrement dit, c'est la proposition $Coh_{PA}: \neg EstUnThéorème_{PA}(\overline{[\perp]})$.

Le second théorème de Gödel affirme alors que, si le système de Peano est cohérent, alors $PA \nvdash Coh_{PA}$. Pour montrer cela, on applique le premier théorème de Gödel à PA, qui nous donne une formule $\theta$ affirmant "je ne suis pas démontrable dans PA", ou, plus formellement, qui vérifie $PA \vdash \big[\theta \Leftrightarrow \neg EstUnThéorème_{PA}(\overline{[\theta])}\big]$. Ensuite, en utilisant D1, D2 et D3, on montre que $PA \vdash \theta \Leftrightarrow Coh_{PA}$:

On commence par utiliser ce fait très utile de la logique classique, qu'une proposition fausse implique tout et n'importe quoi; en particulier $PA \vdash \perp \Rightarrow \theta$. D'après D1, on a donc $$PA \vdash EstUnThéorème_{PA}(\overline{[\perp \Rightarrow \theta]}),$$ donc par D3, $$PA \vdash EstUnThéorème_{PA}(\overline{[\perp]}) \Rightarrow EstUnThéorème_{PA}(\overline{[\theta]}),$$ soit, par contraposée, $$PA \vdash \neg EstUnThéorème_{PA}(\overline{[\theta]}) \Rightarrow \neg EstUnThéorème_{PA}(\overline{[\perp]}).$$ Or, $PA \vdash \neg EstUnThéorème_{PA}(\overline{[\theta]}) \Leftrightarrow \theta$ et $\neg EstUnThéorème_{PA}(\overline{[\perp]})$ est exactement $Coh_{PA}$, donc on a bien $$PA \vdash \theta \Rightarrow Coh_{PA}.$$

Pour l'autre sens, en utilisant D2, on voit que $$PA \vdash EstUnThéorème_{PA}(\overline{[\theta]}) \Rightarrow EstUnThéorème_{PA}(\overline{[EstUnThéorème_{PA}(\overline{[\theta]}]}),$$ et, par contraposée de $$PA \vdash \big[\theta \Rightarrow \neg EstUnThéorème_{PA}(\overline{[\theta])}\big],$$ on voit que la proposition $EstUnThéorème_{PA}(\overline{[EstUnThéorème_{PA}(\overline{[\theta])} \Rightarrow \neg \theta]})$ est une $\Sigma$-formule vraie. Or, N, donc PA, est assez fort pour prouver ces formules; autrement dit, $$ PA \vdash EstUnThéorème_{PA}(\overline{[EstUnThéorème_{PA}(\overline{[\theta])}) \Rightarrow \neg \theta]})$$ Donc, par D3, $$PA \vdash EstUnThéorème_{PA}(\overline{[EstUnThéorème_{PA}(\overline{[\theta]})}) \Rightarrow EstUnThéorème_{PA}(\overline{[ \neg \theta]})$$ En combinant avec la première ligne, on a donc, $$PA \vdash EstUnThéorème_{PA}(\overline{[\theta]}) \Rightarrow EstUnThéorème_{PA}(\overline{ [\neg \theta]}).$$ Gardons cela en tête, et remarquons que la proposition $\theta \Rightarrow (\neg \theta \Rightarrow \perp)$ est toujours vraie, donc $EstUnThéorème_{PA}(\overline{[\theta \Rightarrow (\neg \theta \Rightarrow \perp)]})$ est une $\Sigma$-formule vraie, donc on peut la démontrer dans PA. En appliquant deux fois D3 pour détricoter les implications, on obtient: $$PA \vdash EstUnThéorème_{PA}(\overline{[\theta]}) \Rightarrow \left(EstUnThéorème_{PA}(\overline{ [\neg \theta]}) \Rightarrow EstUnThéorème_{PA}(\overline{[\perp]})\right),$$ donc, en combinant avec ce qu'on avait sous le coude, $$PA \vdash EstUnThéorème_{PA}(\overline{[\theta]}) \Rightarrow EstUnThéorème_{PA}(\overline{[\perp]}).$$ La contraposée de ceci s'écrit: $$PA \vdash \neg EstUnThéorème_{PA}(\overline{[\perp]}) \Rightarrow \neg EstUnThéorème_{PA}(\overline{[\theta]}),$$ autrement dit, $$PA \vdash Coh_{PA} \Rightarrow \theta.$$

Du coup, si on avait une preuve de $Coh_{PA}$, cette équivalence nous fournirait une preuve de $\theta$ dans la foulée, et puisque PA est cohérent, ce n'est pas possible.

Références:

  • A Friendly Introduction to Mathematical Logic, de Christopher Leary, chapitres 4,5 et 6
  • C'est l'facteur, sur les difficultés de factorisation en facteurs premiers, sur le blog d'El Jj.
  •