Une phrase autoréférentielle G construite (via le lemme du point fixe) pour une théorie formelle donnée T qui affirme effectivement «G n'est pas démontrable dans T» ; son existence est centrale dans les preuves d'incomplétude car, sous des hypothèses naturelles, ni G ni sa négation ne sont démontrables dans T.

Principe

Utiliser le lemme du point fixe/diagonal pour produire une phrase qui désigne son propre statut de démontrabilité en encodant des notions syntaxiques dans l'arithmétique ; la phrase est conçue de sorte que la démonstrabilité de G dans T contredirait la consistance de T, produisant l'indécidabilité.

Démonstration

Pour une théorie T récursivement axiomatisée qui représente la démontrabilité, on construit une formule Prov_T(x) et on applique le lemme du point fixe pour obtenir G avec T ⊢ (G ↔ ¬Prov_T(⌜G⌝)). Si T est consistante, T ne peut pas prouver G ; si T est suffisamment bien comportée, elle ne peut pas non plus prouver ¬G, rendant G indécidable dans T.

Mauvaise application

Confondre un énoncé de Gödel avec un paradoxe sémantique (par ex. le menteur) ou prétendre que toute phrase autoréférentielle est un énoncé de Gödel ; aussi appeler toute phrase indémontrable «l'énoncé de Gödel» sans préciser la théorie et le codage utilisés.

Conséquence

Fournit des exemples explicites d'énoncés indécidables dans la théorie et met en lumière l'écart entre démontrabilité syntaxique et vérité sémantique ; dans le modèle standard un tel énoncé de Gödel sera vrai chaque fois que la théorie est consistante.

Inversion

La négation de l'énoncé de Gödel produit une phrase dont la démontrabilité dans T implique typiquement que T est inconsistante ; ainsi la preuve de ¬G à l'intérieur de T est un témoin d'inconsistance sous les hypothèses usuelles.

Limite

Exige que la théorie puisse représenter des notions syntaxiques et la démontrabilité ; différents codages et choix produisent des énoncés de Gödel non uniques, donc la construction dépend du formalisme choisi et n'est pas canonique au-delà d'une équivalence démontrable dans des méta-théories plus riches.

Tension sémantique

Se situe entre les notions de vérité sémantique, de démontrabilité syntaxique et d'autoréférence paradoxale : il ressemble à la phrase du menteur par la forme mais diffère car sa construction est arithmétisée et son indémontrabilité découle de la consistance plutôt que d'un paradoxe sémantique.

Synthèse

Un énoncé de Gödel est une construction arithmétisée autoréférentielle qui affirme sa propre non-démontrabilité dans une théorie donnée ; par diagonalisation il convertit le codage syntaxique en une phrase arithmétique indécidable explicite sous l'hypothèse de consistance de la théorie.