Le théorème qui affirme que toute théorie formelle consistante, effectivement axiomatisée et capable de représenter un fragment suffisant de l'arithmétique contient des énoncés vrais qui ne sont pas démontrables dans cette théorie ; il établit un écart nécessaire entre la vérité sémantique et la démontrabilité pour de tels systèmes.

Principe

L'arithmétisation de la syntaxe, le lemme du point fixe (diagonalisation) et la représentabilité des fonctions récursives permettent de construire une phrase G qui affirme sa propre non-démontrabilité ; à partir de la consistance on déduit que G n'est pas démontrable, donc la théorie est incomplète si elle est consistante.

Démonstration

Dans l'arithmétique de Peano du premier ordre on construit une phrase G telle que PA prouve G ↔ «G n'est pas démontrable dans PA». Si PA était à la fois consistante et complète, prouver G ou sa négation entraînerait une contradiction ; la consistance implique que PA ne peut pas prouver G, et si PA ne peut réfuter G alors G est une assertion arithmétique vraie mais indémontrable.

Mauvaise application

Interpréter le théorème comme prouvant que «les mathématiques dans leur ensemble» sont incomplètes de façon informelle ou nihiliste, ou confondre la non-démontrabilité dans un système formel donné avec l'inaccessibilité absolue ; ou l'utiliser pour affirmer que toute théorie non formalisée doit être incomplète sans vérifier les conditions d'expressivité et d'effectivité.

Conséquence

Toute théorie suffisamment expressive et effectivement axiomatisée et consistante ne peut être à la fois complète et récursive ; il existera toujours des énoncés arithmétiques indécidables relativement à cette théorie, ce qui oblige à des méthodes méta-théoriques ou à des systèmes plus puissants pour les trancher.

Inversion

La réversion naïve — «si une théorie prouve chaque énoncé arithmétique vrai alors elle doit être inconsistante» — est inexacte ; le théorème implique plutôt qu'aucune théorie récursivement axiomatisable de ce type ne peut être complète ; la complétude conjuguée à l'effectivité des axiomes contredit la consistance sous les hypothèses du théorème.

Limite

S'applique aux systèmes formels qui sont consistants, énumérables récursivement (effectivement axiomatisés) et capables de représenter suffisamment l'arithmétique (par exemple Q de Robinson) ; il ne concerne pas les systèmes faibles incapables de coder la syntaxe requise ni les systèmes non effectifs ou essentiellement sémantiques.

Tension sémantique

Met en évidence la tension entre la vérité (vérité arithmétique dans le modèle standard) et la démontrabilité formelle : une phrase peut être vraie mais indémontrable dans une théorie donnée ; cela entre en conflit avec les intuitions informelles qui assimilent démonstration et vérité.

Synthèse

Le premier théorème de Gödel utilise l'autoréférence et la formalisation de la notion de démontrabilité pour montrer que toute théorie consistante et effectivement axiomatisée capable d'arithmétique de base doit laisser des énoncés arithmétiques vrais indémontrables, révélant ainsi une limite intrinsèque des systèmes axiomatiques formels.