En 1787, dans Critique de la raison pure, Immanuel Kant affirmait que la logique formelle n'a pas pu faire un seul pas en avant, et qu'ainsi, selon toute apparence, elle semble close et achevée. Malgré tout, Gottlob Frege fait faire des progrès à la logique en introduisant le calcul des prédicats et avec Grundgesetze der Arithmetik (fondements de l'arithmétique), il tente de dériver l'arithmétique de la logique. Mais en 1902, Bertrand Russell montre que le système formel de Frege était incohérent. On pensait alors qu'un système formel pourrait être complété en ajoutant un nombre fini d'axiomes pour le rendre complet. En 1931, Kurt Gödel met fin à cet espoir en effectuant la démonstration des deux théorèmes d'incomplétude. Comme le fait remarquer Douglas Hofstadter dans Gödel Escher Bach : Les Brins d'une guirlande éternelle, la version originale était en allemand, et vous trouverez peut-être que vous auriez tout aussi bien compris en allemand. L'article de Gödel Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme (Sur les propositions formellement indécidables des Principia Mathematica et des systèmes apparentés, traduit en anglais par On Formally Undecidable Propositions of Principia Mathematica and Related Systems) commence par :

Le développement des mathématiques vers plus d'exactitude a conduit, comme nous le savons, à en formaliser de larges secteurs, de telle sorte que la démonstration puisse s'y effectuer uniquement au moyen de quelques règles mécaniques. Les systèmes formels les plus complets établis jusqu'à ce jour sont, d'un côté, le système des Principia Mathematica; et, de l'autre, le système axiomatique de la théorie des ensembles établi par Zermelo-Fraenkel (et développé par J. von Neumann). Ces deux systèmes sont tellement larges que toutes les méthodes de démonstration utilisées aujourd'hui en mathématiques y sont formalisées, c'est-à-dire ramenées à quelques axiomes et règles d'inférence. On pourrait par conséquent supposer que ces axiomes et règles d'inférence suffisent pour décider de toute question mathématique qui pourrait s'exprimer formellement dans ces systèmes. Dans ce qui suit, nous montrerons que tel n'est pas le cas et qu'il existe au contraire dans ces deux systèmes des problèmes relativement simples concernant la théorie des entiers que l'on ne saurait trancher sur la base de ces axiomes. Cette situation n'est pas due, comme on pourrait le croire, à la nature spécifique des systèmes établis mais touche une très large classe de systèmes formels, à laquelle appartiennent en particulier tous les systèmes qui résultent des deux systèmes cités plus haut par addition d'un nombre fini d'axiomes, pourvu que, par ces axiomes, aucune proposition fausse ne devienne démontrable.

Les théorèmes d'incomplétude s'énoncent de la façon suivante :
  • Dans tout système formel consistant contenant une théorie des nombres finitaires relativement développée, il existe des propositions indécidables.
  • La consistance d'un tel système ne saurait être démontrée à l'intérieur de ce système.
Avec ces deux théorèmes, Gödel répond au deuxième problème de Hilbert : Peut-on prouver la consistance de l'arithmétique ?  En d'autres termes, peut-on démontrer que les axiomes de l'arithmétique ne sont pas contradictoires ?

Pour démontrer le théorème d'incomplétude, Gödel reprend le paradoxe du menteur qui énonce cette phrase est fausse. Si cette phrase est fausse, elle est vraie. Inversement, si elle fausse, elle est vraie. Gödel réussi à formaliser ce type de paradoxe pour l'arithmétique en remplaçant la notion de vérité par celle de démonstration.

Gödel va utiliser une numérotation qui consiste à attribuer un nombre unique à chaque symbole du langage formel considéré. Par exemple, 1 est associé à la négation, 2 au ou logique, 3 à l'implication,... La numérotation de Gödel permet alors de définir une injection du système formel dans l'ensemble des entiers naturels .

Par exemple, l'assertion , qui signifie il existe x tel que x soit le successeur de y, sera transformée en la suite de nombres : 8 4 11 9   8 11 5 7 13 9. Cette suite de nombres est transformée en un entier grâce à la règle suivante : à partir de la suite de 10 nombres ci-dessus, on forme un nombre unique produit des 10 premiers nombres premiers où chacun est élevé à la puissance égale au nombre de Gödel de même rang de la suite :

.

De même, il est aussi possible d'associer un nombre de Gödel à une suite d'assertions. Considérons une suite formée de deux assertions. À chacune de ces deux assertions correspond un nombre. La suite d'assertions est alors associée au produit des deux premiers nombres premiers qui sont chacun élevés à la puissance égale au nombre de Gödel de l'assertion correspondante. Ainsi si m est le nombre de Gödel de la première asertion et n celui  de la deuxième, le nombre associé à cette suite d'assertions sera : .

À toute expression du système formel, que ce soit un signe, une suite de signes ou une suite de formules, il est donc possible d'associer un nombre unique. Inversement, par l'unicité de la décomposition d'un nombre en facteurs premiers, à un nombre de Gödel correspond une expression du système formel.

Gödel définit ensuite la relation entre les nombres x et z, notée Dem(x,z), qui veut dire que la suite de formules associée au nombre de Gödel x est une démonstration de la formule de nombre de Gödel z.

On considère alors la formule G : . Cette formule veut dire qu'il n'existe pas de démonstration ayant pour nombre de Gödel x de la formule de nombre de Gödel z, c'est-à-dire que l'assertion qui porte le nombre de Gödel z n'est pas démontrable.

Gödel considère un cas particulier de cette assertion. Pour cela, on note sub(m,p,q) le nombre de Gödel de la formule obtenue en substituant à la variable de nombre de Gödel p dans la formule de nombre de Gödel m le nombre q. Ainsi, sub(n,13,n) est le nombre de Gödel obtenu à partir de la formule qui porte le nombre de Gödel n et dans laquelle on substitue à la variable de nombre 13 la variable n. Par exemple, si l'assertion possède le nombre de Gödel n, la variable qui possède le nombre 13, qui est y, est remplacée par le nombre n. L'assertion devient alors : .

Le cas particulier de G considéré par Gödel est :
.
Cette assertion signifie : pour tout nombre de Gödel x, la suite de formules associée au nombre de Gödel x ne démontre pas la formule obtenue en substituant le nombre n à la variable de nombre 13 dans la formule de nombre de  Gödel n. Ce qui veut dire aussi que l'assertion qui possède le nombre de Gödel sub(n,13,n) n'est pas démontrable.

Cette assertion particulière porte elle-même un nombre de Gödel. Le nombre de Gödel de G est sub(n,13,n). En effet, sub(n,13,n) est le nombre de Gödel de la formule obtenue à partir de la formule qui porte le nombre de Gödel n en substituant le chiffre n à la variable qui porte le nombre de Gödel 13 (c'est-à-dire la variable y). Or, la formule a été obtenue à partir de la formule qui porte le nombre n en substituant à la variable y le chiffre n. Donc le nombre de Gödel de l'asserttion G est bien sub(n,13,n).

Or, l'assertion G affirme que l'assertion qui possède le nombre de Gödel sub(n,13,n) n'est pas démontrable. Donc, l'assertion G dit d'elle-même qu'elle n'est pas démontrable.

Gödel démontre ensuite que si G est démontrable alors ~ G est aussi démontrable. Si G est démontrable, il existe un nombre de Gödel k tel que . On peut prouver que si la relation Dem(x,z) existe entre deux nombres alors cette relation est démontrable. Donc est démontrable et est démontrable. Cette dernière formule correspond à ~ G. Réciproquement, Gödel montre que si ~ G est démontrable, G l'est aussi. Le système formel est dons inconsistant.

De plus, l'assertion G est vraie. En effet, on a montré que l'assertion G n'est pas démontrable. Or, c'est justement ce qu'énonce G.

On vient de montrer que la consistance d'un système implique qu'il est incomplet, c'est-à-dire qu'il existe une formule vraie qui est indémontrable et dont la négation n'est pas non plus démontrable. La validité de cette formule ne pourra pas être déterminée dans le cadre du système formel.

Le second théorème de Gödel énonce que la consistance (ou la non-contradiction) du système formel, c'est-à-dire qu'aucune contradiction ne peut être prouvée à partir de ses axiomes, ne peut être démontrée à l'intérieur de ce système.

Avec le premier théorème d'incomplétude, on montre qu'à partir d'un système formel cohérent on aboutit à G. La consistance entraîne donc la formule G. Si on pouvait démontrer dans le système formel, la consistance, alors il s'en suivrait que G serait démontrable dans ce système formel. Or, la démonstration précédente montre que ce n'est pas le cas. Par conséquent, c'est qu'il est impossible de démontrer dans le système formel la consistance.

Mark Dominus donne une brève explication du théorème de Gödel en reprenant une idée de Raymond Smullyan. Pour plus de compléments sur le théorème de Gödel, on pourra lire les livres Le théorème de Gödel de Ernest Nagel, James R. Newman et Jean-Yves Girard qui réussit à vulgariser la démonstration du théorème de Gödel, ainsi que Gödel Escher Bach : Les Brins d'une guirlande éternelle de Douglas Hofstadter qui établit des parallèles entre les œuvres de Gödel, de l'artiste Maurits Cornelis Escher et du compositeur Johann Sebastian Bach. Les résumés de cours de Jacques Bouveresse au Collège de France de 2003 à 2006 sur Gödel sont disponibles : Kurt Gödel, mathématiques, logique et philosophie.