Der Satz, der besagt, dass keine konsistente, effektiv axiomatisierte formale Theorie, die genügend Arithmetik repräsentieren kann, ihre eigene Konsistenz beweisen kann, wenn Konsistenz innerhalb der Theorie formalisiert wird; kurz: ein System kann seine eigene Widerspruchsfreiheit nicht mit den ihm zur Verfügung stehenden internen Mitteln zertifizieren.

Prinzip

Indem man ein Provabilitätsprädikat formalisiert und dieselben Diagonalisierungstechniken wie im ersten Satz verwendet, zeigt man: Würde eine Theorie T Con(T) beweisen (eine Formel, die 'es gibt keinen Beweis für einen Widerspruch in T' formalisiert), so könnte T eine Formel beweisen, die nach dem ersten Satz nicht beweisbar sein sollte, und es ergäbe sich Inkonsistenz.

Demonstration

In der Peano-Arithmetik repräsentiert man das Prädikat 'x ist ein Beweis in PA' und formuliert Con(PA). Gödelsches Argument produziert einen Satz G derart, dass falls PA Con(PA) beweist, PA auch G beweisen würde und damit der Schluss des ersten Satzes umgangen würde; daher kann PA bei Konsistenz Con(PA) nicht beweisen.

Fehlanwendung

Zu behaupten, der Satz verbiete jegliche externe oder stärkere Systembeweise der Konsistenz — tatsächlich verhindert der Satz nur, dass eine Theorie ihre eigene Konsistenz mit intern formalisierten Mitteln beweist; er schließt nicht aus, dass eine stärkere Metatheorie Con(T) beweisen kann.

Konsequenz

Konsistenzbeweise für eine Theorie müssen entweder aus stärkeren Theorien stammen, nicht-formalen Methoden folgen oder Annahmen enthalten, die in der Theorie selbst nicht formalisiert werden können; dies formt die Hierarchie der fundamentalen Rechtfertigungen und zeigt die Relativität von Konsistenzbehauptungen.

Umkehrung

Die Kontraposition lautet oft: Wenn eine Theorie T Con(T) beweist, dann ist T inkonsistent; somit ist das Beweisen der eigenen Konsistenz innerhalb desselben formalen Systems gleichbedeutend mit Inkonsistenz unter den Voraussetzungen des Theorems.

Abgrenzung

Voraussetzung ist effektive Axiomatisierbarkeit und hinreichende Arithmetik zur Darstellung von Provabilität und Beweisprädikaten; es gilt nicht für Systeme, die diese syntaktischen Begriffe nicht repräsentieren können, oder für Rahmen, die die Formalisierung von Konsistenz verändern.

Semantische Spannung

Erzeugt Spannung zwischen interner und externer Sicht auf Beweis: Interne Beweisbarkeit von Con(T) ist ausgeschlossen, während sie extern in einer stärkeren Metatheorie beweisbar sein kann; dies trennt syntaktische Selbstbestätigung von metatheoretischer Validierung.

Synthese

Gödels zweiter Satz formalisiert die Intuition, dass ein System mit seinen eigenen formalen Mitteln nicht beweisen kann, dass diese Mittel niemals zu einem Widerspruch führen: Durch Kodierung von Beweisen und Provabilität und Anwendung diagonal-argumentativer Methoden zeigt er, dass ein solcher interner Beweis in Inkonsistenz münden würde.