Der Satz, dass jede konsistente, effektiv axiomatisierte formale Theorie, die ein hinreichendes Fragment der Arithmetik darstellen kann, wahre Sätze enthält, die in dieser Theorie nicht beweisbar sind; er stellt eine notwendige Lücke zwischen semantischer Wahrheit und Beweisbarkeit solcher Systeme fest.

Prinzip

Arithmetisierung der Syntax zusammen mit dem Diagonal- (Fixpunkt-)Lemma und der Repräsentierbarkeit rekursiver Funktionen erzeugen einen Satz G, der seine eigene Unbeweisbarkeit behauptet; aus der Konsistenz folgt, dass G nicht beweisbar ist, und somit ist die Theorie bei Konsistenz unvollständig.

Demonstration

In der ersten Ordnung Peano-Arithmetik konstruiert man einen Satz G mit PA ⊢ (G ↔ 'G ist in PA nicht beweisbar'). Wäre PA sowohl konsistent als auch vollständig, würde das Beweisen von G oder seiner Negation zu einem Widerspruch führen; Konsistenz impliziert, dass PA G nicht beweisen kann, und wenn PA G nicht widerlegen kann, dann ist G ein wahres, aber unbeweisbares arithmetisches Statement.

Fehlanwendung

Den Satz so zu interpretieren, dass ‚die Mathematik insgesamt‘ im informellen Sinn unvollständig oder wertlos sei, oder die Unbeweisbarkeit in einem bestimmten formalen System mit absoluter Unzugänglichkeit zu verwechseln; ebenso falsch ist anzunehmen, der Satz gelte ohne Prüfung der Expressivität- und Effektivitätsbedingungen für jedes System.

Konsequenz

Jede hinreichend ausdrucksstarke, effektiv axiomatisierbare konsistente Theorie kann nicht zugleich vollständig und rekursiv sein; es gibt bezüglich dieser Theorie stets unentscheidbare arithmetische Sätze, weshalb metatheoretische Methoden oder stärkere Systeme erforderlich sind, um sie zu entscheiden.

Umkehrung

Die naive Umkehrung — ‚wenn eine Theorie jeden wahren arithmetischen Satz beweist, muss sie inkonsistent sein‘ — ist falsch; korrekter ist: Unter den Voraussetzungen des Theorems kann keine rekursiv axiomatisierbare Theorie vollständig sein, da Vollständigkeit zusammen mit effektiver Axiomatisierbarkeit der Konsistenz widerspräche.

Abgrenzung

Gilt für formale Systeme, die konsistent, rekursiv aufzählbar (effektiv axiomatisiert) und in der Lage sind, genügend Arithmetik zu repräsentieren (z. B. Robinsons Q); es gilt nicht für schwache Systeme, die die nötige Kodierung nicht leisten können, noch für nicht-effektive oder im Wesentlichen semantische Systeme.

Semantische Spannung

Hebt die Spannung zwischen Wahrheit (arithmetische Wahrheit im Standardmodell) und formaler Beweisbarkeit hervor: Ein Satz kann wahr, aber innerhalb einer Theorie unbeweisbar sein; das widerspricht informellen Auffassungen, die Beweisbarkeit mit Wahrheit gleichsetzen.

Synthese

Gödels erster Satz nutzt Selbstbezüglichkeit und die Formalisierung von Beweisbarkeit, um zu zeigen, dass jede konsistente, effektiv axiomatisierte Theorie mit grundsätzlicher Arithmetik wahre, aber unbeweisbare arithmetische Sätze enthält und damit eine fundamentale Grenze formaler Axiomensysteme aufzeigt.