Le premier théorème d’incomplétude repose sur la capacité d’un système formel $T$ (suffisamment puissant) à parler de sa propre démontrabilité via la numérotation de Gödel. Le second théorème pousse cette idée plus loin en formalisant la notion de consistance.
Un système $T$ est consistant s’il ne peut pas démontrer de contradiction. Une contradiction est une formule de la forme « $P \land \neg P$ », qui est équivalente à une formule toujours fausse, notée $\bot$ (par exemple, « 0=1 »).
L’énoncé « Le système T est consistant » peut être traduit en une formule arithmétique. Cette formule, notée $Cons(T)$, exprime l’idée suivante :
« Il n’existe aucune démonstration de la contradiction $\bot$ dans le système T. »
En utilisant le prédicat de démontrabilité $Dem(y,x)$ du premier théorème, cette formule s’écrit : $Cons(T) \equiv \neg(\exists y, Dem(y, g_\bot))$, où $g_\bot$ est le numéro de Gödel de la formule $\bot$.
Pour tout système formel $T$ consistant et récursivement axiomatisable, suffisamment puissant pour formaliser l’arithmétique des entiers, le système $T$ ne peut pas démontrer son propre énoncé de consistance. $$ \text{Si T est consistant, alors } T \not\vdash Cons(T) $$
En d’autres termes, aucun système formel (suffisamment riche) ne peut prouver sa propre cohérence en utilisant uniquement ses propres axiomes et règles.
Esquisse de la Démonstration
La démonstration du second théorème est une formalisation, à l’intérieur du système lui-même, de la démonstration du premier théorème.
Étape 1 : Formalisation de la Preuve du Premier Théorème
Rappelons l’énoncé de Gödel $G$ qui dit « Je ne suis pas démontrable ». La preuve du premier théorème établit l’implication suivante (au niveau méta-mathématique) : $$ \text{Si T est consistant, alors G n’est pas démontrable dans T.} $$ L’idée cruciale de Gödel est que cette démonstration, qui est une suite de raisonnements logiques, peut elle-même être « traduite » et menée à l’intérieur du système T. Le système T est assez puissant pour formaliser sa propre syntaxe et ses propres règles de déduction.
Le système T peut donc prouver l’implication qui correspond à notre raisonnement. Cela donne le théorème suivant, qui est démontrable *dans* T : $$ T \vdash (Cons(T) \implies G) $$ Cet énoncé se lit : « T peut démontrer que ‘Si T est consistant, alors l’énoncé de Gödel G est vrai (c’est-à-dire indémontrable)’. »
Étape 2 : L’Argument par l’Absurde
Maintenant, raisonnons par l’absurde. Supposons que le second théorème soit faux, c’est-à-dire qu’un système T consistant puisse prouver sa propre consistance.
- Hypothèse : Supposons que $T \vdash Cons(T)$. (Le système prouve qu’il est consistant).
- Fait établi à l’étape 1 : Nous savons que $T \vdash (Cons(T) \implies G)$.
- Application du Modus Ponens : Tout système logique standard possède la règle du modus ponens : si on a prouvé « A » et qu’on a prouvé « A implique B », alors on peut en déduire une preuve de « B ». En appliquant cette règle à nos deux énoncés démontrables, le système T pourrait conclure : $$ T \vdash G $$
- Contradiction : Mais le premier théorème d’incomplétude nous a précisément appris que si T est consistant, alors $T \not\vdash G$ (G n’est pas démontrable). Notre hypothèse (que T peut prouver sa consistance) nous a menés à la conclusion que T peut prouver G, ce qui, d’après le premier théorème, implique que T est inconsistant.
Conclusion : L’hypothèse de départ (« T peut prouver sa propre consistance ») conduit à une contradiction avec l’hypothèse initiale que T est consistant. Par conséquent, cette hypothèse doit être fausse.
Si un système est consistant, il ne peut donc pas démontrer l’énoncé qui formalise sa propre consistance.
Implications Philosophiques et sur les Fondements des Mathématiques
Ce théorème a eu un impact dévastateur sur le programme de Hilbert, qui visait à fonder toutes les mathématiques sur un ensemble fini d’axiomes et à prouver la consistance de ce système par des moyens « finitistes » (c’est-à-dire des méthodes simples et sûres, contenues dans l’arithmétique elle-même). Le second théorème de Gödel montre que cet objectif est inatteignable : pour prouver la consistance de l’arithmétique, il faut nécessairement utiliser des axiomes « plus forts » que ceux de l’arithmétique, dont la consistance sera elle-même encore plus incertaine.