Le théorème qui affirme qu'aucune théorie formelle consistante et effectivement axiomatisée capable de représenter suffisamment d'arithmétique ne peut démontrer sa propre consistance, lorsque la consistance est formalisée à l'intérieur de la théorie elle-même ; en bref, une théorie ne peut pas certifier par ses propres moyens qu'elle est exempte de contradiction.

Principe

En formalisant un prédicat de démontrabilité et en utilisant les mêmes techniques de diagonalisation que pour le premier théorème, on montre que si une théorie T prouvait Con(T) (une phrase formalisant «il n'existe pas de preuve d'une contradiction dans T»), alors T prouverait une phrase qu'elle ne peut démontrer de façon consistante, entraînant l'inconsistance.

Démonstration

Dans l'arithmétique de Peano on représente le prédicat «x est une preuve dans PA» et on formule une phrase Con(PA). Le raisonnement à la Gödel produit une phrase G telle que si PA prouvait Con(PA), alors PA prouverait G et contredirait la conclusion du premier théorème ; ainsi, si PA est consistante elle ne peut prouver Con(PA).

Mauvaise application

Affirmer que le théorème interdit toute démonstration externe ou dans un système plus fort de la consistance — le théorème n'empêche qu'une théorie de prouver sa propre consistance par des moyens formalisables en elle-même ; il n'exclut pas des preuves méta-mathématiques ou dans des systèmes plus puissants.

Conséquence

Les preuves de consistance d'une théorie doivent provenir d'une théorie plus forte, de méthodes non formelles ou d'hypothèses non formalisables dans la théorie elle-même ; cela structure la hiérarchie des justifications fondationnelles et montre la relativisation inévitable des affirmations de consistance.

Inversion

La conséquence contraposée s'énonce souvent ainsi : si une théorie T prouve Con(T) alors T est inconsistante ; prouver sa propre consistance à l'intérieur d'un même système équivaut donc à l'inconsistance sous les hypothèses formelles du théorème.

Limite

Exige l'axiomatisation effective et une arithmétique suffisante pour représenter la démontrabilité et les prédicats de preuve ; il ne s'applique pas aux systèmes incapables de représenter ces notions syntaxiques ni aux cadres modifiant la formalisation de la consistance.

Tension sémantique

Crée une tension entre perspectives internes et externes sur la preuve : la démonstration interne de Con(T) est exclue, alors que, de l'extérieur (dans une méta-théorie plus forte), on peut prouver Con(T) ; cela distingue l'auto-certification syntaxique de la validation méta-théorique.

Synthèse

Le second théorème de Gödel formalise l'intuition selon laquelle un système ne peut, par ses propres ressources formelles, établir qu'elles ne produisent jamais de contradiction : en codant preuves et démontrabilité à l'intérieur de la théorie et en appliquant des arguments diagonaux, on montre qu'une telle preuve interne conduit à l'inconsistance.