Ein selbstbezüglicher Satz G, konstruiert (mittels des Fixpunkt-/Diagonal-Lemmas) für eine gegebene formale Theorie T, der effektiv aussagt 'G ist in T nicht beweisbar'; seine Existenz ist zentral für Unvollständigkeitsbeweise, weil unter natürlichen Voraussetzungen weder G noch seine Negation in T beweisbar sind.

Prinzip

Verwende das Fixpunkt-/Diagonal-Lemma, um einen Satz zu erzeugen, der seinen eigenen Beweisbarkeitsstatus benennt, indem syntaktische Begriffe in die Arithmetik kodiert werden; der Satz ist so konstruiert, dass die Beweisbarkeit von G in T der Konsistenz von T widersprechen würde und damit Unentscheidbarkeit hervorruft.

Demonstration

Für eine rekursiv axiomatisierte Theorie T, die Provabilität repräsentiert, konstruiert man das Formel-Prov_T(x) und wendet das Diagonal-Lemma an, um G mit T ⊢ (G ↔ ¬Prov_T(⌜G⌝)) zu erhalten. Ist T konsistent, kann T G nicht beweisen; ist T hinreichend wohlverhalten, kann es auch ¬G nicht beweisen, womit G in T unentscheidbar ist.

Fehlanwendung

Einen Gödel-Satz mit einem semantischen Paradoxon (z. B. dem Lügner) zu verwechseln oder zu behaupten, jeder selbstreferentielle Satz sei ein Gödel-Satz; ebenso falsch ist es, irgendeinen unbeweisbaren Satz als 'den' Gödel-Satz zu bezeichnen ohne Bezug auf die verwendete Theorie und Kodierung.

Konsequenz

Er liefert explizite Beispiele für in der Theorie unentscheidbare Sätze und macht die Kluft zwischen syntaktischer Beweisbarkeit und semantischer Wahrheit sichtbar; im Standardmodell ist ein solcher Gödel-Satz genau dann wahr, wenn die Theorie konsistent ist.

Umkehrung

Die Negation des Gödel-Satzes ergibt einen Satz, dessen Beweisbarkeit in T typischerweise die Inkonsistenz von T zur Folge hätte; der Beweis von ¬G innerhalb von T ist unter den üblichen Voraussetzungen ein Inkonsistenzzeugnis.

Abgrenzung

Voraussetzung ist, dass die Theorie syntaktische Begriffe und Provabilität repräsentieren kann; unterschiedliche Codierungen und Entscheidungen erzeugen nicht-unique Gödel-Sätze, die Konstruktion hängt also vom formalen Aufbau ab und ist nicht kanonisch jenseits beweisbarer Äquivalenz in reicheren Metatheorien.

Semantische Spannung

Steht zwischen den Begriffen semantischer Wahrheit, syntaktischer Beweisbarkeit und paradoxaler Selbstbezüglichkeit: formal ähnelt er dem Lügner, unterscheidet sich jedoch dadurch, dass seine Konstruktion arithmetisiert ist und seine Unbeweisbarkeit sich aus Konsistenz ergibt, nicht aus einem semantischen Paradoxon.

Synthese

Ein Gödel-Satz ist eine arithmetisierte selbstreferentielle Konstruktion, welche ihre eigene Nicht-Beweisbarkeit in einer gegebenen Theorie behauptet; durch Diagonalisierung verwandelt sie Syntaxkodierung in einen expliziten unentscheidbaren arithmetischen Satz unter der Konsistenzannahme der Theorie.