Beweise der gödelschen Unvollständigkeitssätze

Dieser Artikel skizziert Beweise der Gödelschen Unvollständigkeitssätze. Dabei handelt es sich um zwei mathematische Sätze, die zu den wichtigsten Ergebnissen der Logik gezählt werden und die von Kurt Gödel 1930 bewiesen wurden.

Der erste Unvollständigkeitssatz besagt, dass kein konsistentes Axiomensystem, dessen Theoreme von einem Algorithmus aufgezählt werden können, alle wahren Aussagen über natürliche Zahlen mit Addition und Multiplikation beweisen kann. Der zweite Unvollständigkeitssatz besagt, dass ein solches System die eigene Widerspruchsfreiheit nicht beweisen kann.

Erster Unvollständigkeitssatz

Der erste Unvollständigkeitssatz lässt sich wie folgt allgemein formulieren:

Sei

T

ein rekursiv aufzählbares und widerspruchsfreies formales System, in dem die Robinson-Arithmetik interpretierbar ist. Dann ist

T

unvollständig. (Es gibt also arithmetische Formeln, die in

T

weder beweisbar noch widerlegbar sind.)

Dabei ist die Robinson-Arithmetik (auch $Q$ ) eine schwache Form der Arithmetik in Prädikatenlogik erster Stufe. Diese verfügt über die Konstante ${\dot {0}}$ „null“, die Nachfolgerfunktion ${\dot {S}}$ , welche intuitiv zu einer gegebenen Zahl eins addiert, sowie die Funktionen ${\dot {+}}$ für Addition und ${\dot {\times }}$ für Multiplikation. Sie hat folgende Axiome, die elementare Eigenschaften der natürlichen Zahlen und der arithmetischen Operationen formalisieren:

Null hat keinen Vorgänger: $\neg ({\dot {S}}x\doteq {\dot {0}})$
Wenn x+1 = y+1 gilt, dann ist x=y: $({\dot {S}}x\doteq {\dot {S}}y)\rightarrow x\doteq y$
Jede Zahl ist gleich Null oder hat einen Vorgänger: $y\doteq {\dot {0}}\vee \exists x({\dot {S}}x\doteq y)$
Axiomatische Definition von Addition und Multiplikation:
- $x{\dot {+}}{\dot {0}}\doteq x$
- $x{\dot {+}}{\dot {S}}y\doteq {\dot {S}}(x{\dot {+}}y)$
- $x{\dot {\times }}{\dot {0}}\doteq {\dot {0}}$
- $x{\dot {\times }}{\dot {S}}y\doteq (x{\dot {\times }}y){\dot {+}}x$

Die Punkte über den Ausdrücken deuten hier und im weiteren Verlauf des Artikels an, dass diese Ausdrücke zu der betrachteten Sprache gehören. So ist ${\dot {Beweis}}(x,y)$ (s. u.) eine Formel des betrachteten formalen Systems, während $Beweis(n,m)$ eine Relation zwischen natürlichen Zahlen ist. Das "Numeral" einer natürlichen Zahl $n$ , die Repräsentierung der natürlichen Zahl im System, wird mit ${\dot {n}}$ bezeichnet, das Numeral von 4 ist z. B.der Term ${\dot {S}}{\dot {S}}{\dot {S}}{\dot {S}}{\dot {0}}$ .

Im Folgenden wird angenommen, dass $T$ die Robinson-Arithmetik selbst ist. Der Beweis lässt sich genauso für jedes andere System durchführen, in dem sich die Arithmetik so interpretieren lässt, dass sich alle Funktionen aus der Robinson-Arithmetik so durch Ausdrücke des neuen Systems definieren lassen, dass alle Theoreme der Robinson-Arithmetik in Theoreme des anderen Systems übergehen. Insbesondere wird davon ausgegangen, dass das Axiomensystem entscheidbar ist. Gödel bewies den Satz ursprünglich für das viel stärkere System der Principia Mathematica. Ebenso lässt sich der Beweis für die Zermelo-Fraenkel-Mengenlehre durchführen, die als einziges nichtlogisches Zeichen die Elementrelation $\in$ hat, in der Zahlen aber als Mengen interpretiert werden können, sodass alle Theoreme der Robinson-Arithmetik als Theoreme der Mengenlehre interpretierbar sind. Der Beweis lässt sich ebenfalls für ein lediglich aufzählbares Axiomensystem adaptieren.

Der Beweis zerfällt in vier Teile:

Arithmetisierung der Syntax: Jedem Ausdruck der Theorie wird eine Zahl, die sogenannte Gödelnummer, zugewiesen, aus der sich die Formel wieder effektiv rekonstruieren lässt. Diese Nummerierung wird auf endliche Folgen von Formeln erweitert.
Arithmetisierung der Beweisbarkeitsrelation: Eine Formel ${\dot {Beweis}}(x,y)$ wird konstruiert, sodass für jedes Paar von Zahlen $n$ und $m$ , ${\dot {Beweis}}({\dot {n}},{\dot {m}})$ genau dann beweisbar ist, wenn $n$ die Gödelnummer eines Beweises einer Formel ist, deren Gödelnummer $m$ ist.
Konstruktion des Gödelsatzes: Es wird eine Formel konstruiert, die informell besagt „Ich bin nicht beweisbar.“, der sogenannte Gödelsatz.
Nachweis der Unbeweisbarkeit: Es wird gezeigt, dass der Gödelsatz weder bewiesen noch widerlegt werden kann.

Arithmetisierung der Syntax

Das Hauptproblem bei der Ausführung des oben beschriebenen Beweises scheint zunächst darin zu liegen, dass bei der Konstruktion einer Aussage $p$ , die äquivalent zu „ $p$ ist unbeweisbar“, $p$ eine Referenz auf $p$ enthalten muss. Gödels Lösung ist, zu zeigen, dass Aussagen auf eine solche Weise Zahlen zugewiesen werden können, dass das Beweisen einer Aussage dadurch ersetzt werden kann, dass überprüft wird, ob die der Aussage zugewiesene Zahl eine gewisse arithmetische Eigenschaft hat. Dies ermöglicht die Konstruktion einer selbstbezüglichen Formel, die unendlichen Regress vermeidet.

Der erste Schritt des Beweises besteht somit darin, Formeln und endliche Folgen von Formeln (injektiv) auf natürliche Zahlen abzubilden. Diese Zahlen heißen Gödelnummern der Formeln. Zunächst wird jedem Symbol der Sprache der Arithmetik eine Zahl zugeordnet, ähnlich dem ASCII-Code, der jedem Buchstaben eine eindeutige Zahl zuordnet. Es gibt verschiedene Möglichkeiten dazu, hier wird direkt jedem Zeichen eine Ziffernfolge zugeordnet.

Nummer	Symbol	Bedeutung
11	${\dot {0}}$	null
12	${\dot {S}}$	Nachfolgerfunktion
13	$\doteq$	Gleichheit
14	${\dot {+}}$	Addition
15	${\dot {\times }}$	Multiplikation
16	(	linke Klammer
17	)	rechte Klammer

Nummer	Symbol	Bedeutung
18	$x$	eine Variable
19	$'$	Strich (für weitere Variablen x', x'', …)
21	$\exists$	Existenzquantor
22	$\forall$	Allquantor
23	$\land$	logisches und
24	$\lor$	logisches oder
25	$\neg$	Negation

Man sieht hier, dass das im 2. Axiom benutzte Symbol für Implikation ( $\to$ ) fehlt; bekanntlich ist $p\to q$ aber äquivalent zu $\neg p\vee q$ (zumindest in der klassischen Logik).

Die Gödelnummer einer Formel erhält man durch Aneinanderreihung der Gödelnummern für jedes Symbol der Formel. Jede Formel kann eindeutig aus ihrer Gödelnummer rekonstruiert werden. Die Gödelnummer einer Formel $F$ wird mit $G(F)$ bezeichnet.

Mit dieser Gödelnummerierung erhält beispielsweise der Satz, der das Kommutativgesetz der Addition ausdrückt, $\forall x\forall x'(x{\dot {+}}x'\doteq x'{\dot {+}}x)$ die Nummer:

22 18 22 19 16 18 14 19 13 19 14 18 17

(die Leerzeichen dienen nur der Lesbarkeit.) Nicht alle Zahlen repräsentieren Formeln, beispielsweise steht

13 22 14 18

für " $\doteq \forall {\dot {+}}x$ ", was keine korrekte Formel ist.

Im System wird jede natürliche Zahl n durch ihr Numeral repräsentiert. Umgekehrt hat auch jedes Numeral eine Gödelnummer, so ist die Gödelnummer für ${\dot {S}}{\dot {S}}{\dot {S}}{\dot {S}}{\dot {0}}$ gleich:

12 12 12 12 11.

Die Zuweisung von Gödelnummern kann auf endliche Folgen von Formeln erweitert werden. Um die Gödelnummer einer endlichen Folge von Formeln zu erhalten, werden die Nummern der Formeln hintereinander geschrieben und jeweils durch eine Null getrennt. Da die Gödelnummer einer einzelnen Formel nie eine Null enthält, kann jede Formel der Folge eindeutig rekonstruiert werden.

Es ist wichtig, dass die formale Arithmetik einige einfache Tatsachen beweisen kann. Insbesondere muss sie beweisen können, dass jede Zahl eine Gödelnummer hat. Ebenso muss sie beweisen, dass es für die Gödelnummer einer Formel $F(x)$ , die eine freie Variable besitzt, und für eine Zahl $m$ die Gödelnummer einer Formel $F(m)$ , in der alle Vorkommen von $x$ durch die Gödelnummer von $m$ ersetzt wurden, gibt, und dass man diese Gödelnummer aus der ersten durch eine effektive Prozedur erhalten kann.

Die Beweisbarkeitsrelation

Das formale System besitzt Axiome und Schlussregeln, aus denen die Formeln des Systems bewiesen werden können. Ein formaler Beweis im System ist somit eine Kette von Formeln, in der jede entweder ein Axiom ist oder sich durch eine Schlussregel aus früheren Formeln gewinnen lässt.

Da das formale System entscheidbar ist, kann man effektiv entscheiden, ob eine gegebene Zahl Gödelnummer eines Axioms ist. Im Falle des endlich axiomatisierten Systems $Q$ genügt es sogar, zu überprüfen, ob die Zahl zur Gödelnummer einer der sieben Axiome gleich ist.

Schlussregeln können als binäre Relationen zwischen Gödelnummern von Folgen von Formeln repräsentiert werden. So gibt es beispielsweise eine Schlussregel $D_{1}$ , durch die man aus den Formeln $S_{1},S_{2}$ die Formel $S_{1}\wedge S_{2}$ erhält. Dann besagt die Relation $R_{1}$ zu dieser Ableitungsregel, dass $n$ genau dann in Relation zu $m$ steht ( $nR_{1}m$ gilt), wenn $n$ die Gödelnummer einer Liste von Formeln ist, die $S_{1}$ und $S_{2}$ enthält, und $m$ die Gödelnummer einer Liste von Formeln ist, die aus den Formeln in der von $n$ kodierten Liste besteht und zusätzlich $S_{1}\wedge S_{2}$ enthält. Da jede Ableitungsregel eine einfache formale Vorschrift ist, ist es möglich, effektiv zu entscheiden, ob zwei Zahlen $n$ und $m$ in Relation $R_{1}$ stehen.

Der zweite Schritt ist, zu zeigen, dass diese Gödelnummerierung benutzt werden kann, um den Begriff der Beweisbarkeit auszudrücken. Ein Beweis einer Formel $S$ ist eine Kette von Formeln, in denen jede ein Axiom ist oder aus früheren Aussagen durch eine Ableitungsregel entsteht, und in der die letzte Aussage $S$ ist. Damit lässt sich die Gödelnummer eines Beweises mit der oben angegebenen Methode zur Kodierung endlicher Folgen von Formeln definieren. Zudem lässt sich eine Relation $Beweis(x,y)$ definieren, die für zwei Zahlen $x$ and $y$ genau dann wahr (und beweisbar) ist, wenn $x$ die Gödelnummer eines Beweises von $S$ ist, und $y=G(S)$ ist.

$Beweis(x,y)$ ist eine arithmetische Relation, ebenso wie etwa „ $x+y=6$ “, nur viel komplizierter. Für alle spezifischen Zahlen $n$ und $m$ ist entweder die Formel ${\dot {Beweis}}(m,n)$ oder ihre Negation $\lnot {\dot {Beweis}}(m,n)$ beweisbar (aber nicht beide). Dies liegt daran, dass die Relation zwischen den Zahlen auf einfache Weise „überprüft“ werden kann. Die Konstruktion der Formel ${\dot {Beweis}}$ hängt entscheidend davon ab, dass das Axiomensystem entscheidbar ist; ohne diese Annahme wäre die Formel nicht konstruierbar.

Damit lässt sich nun eine Relation ${\dot {Beweisbar}}(y)$ definieren, die die metasprachliche Aussage „ $F$ ist beweisbar“ repräsentiert: $F$ ist beweisbar, wenn es eine Zahl $x$ gibt, die einen Beweis für $F$ kodiert:

{\dot {Beweisbar}}(y)=\exists x({\dot {Beweis}}(x,y))

Dabei ist " ${\dot {Beweisbar}}(y)$ " ebenso wie " ${\dot {Beweis}}(x,y)$ " nur eine Abkürzung für eine bestimmte, sehr lange, arithmetische Formel; die Symbole " ${\dot {Beweis}}$ " und " ${\dot {Beweisbar}}$ " selbst gehören nicht zur Sprache des Systems.

Ein wichtiges Merkmal der Formel ${\dot {Beweisbar}}(y)$ ist, dass ${\dot {Beweisbar}}(G(p))$ beweisbar ist, wenn $p$ beweisbar ist. Denn wenn $p$ beweisbar ist, dann existiert ein Beweis mit Gödelnummer $n$ . Dann ist ${\dot {Beweis}}({\dot {n}},G(p))$ wahr und, wie oben dargelegt, beweisbar. Damit ist erst recht die schwächere Existenzaussage $\exists x{\dot {Beweis}}(x,G(p))$ beweisbar.

Formalisiert lassen sich die Ergebnisse dieses Abschnitts mit Hilfe des Ableitbarkeitssymbols $\vdash$ zusammenfassen:

${\text{Falls Beweis(n,m) dann T}}\vdash {\dot {Beweis}}({\dot {n}},{\dot {m}})$
${\text{Falls non Beweis(n,m) dann T}}\vdash \neg {\dot {Beweis}}({\dot {n}},{\dot {m}})$
${\text{Falls Beweisbar(n) dann T}}\vdash {\dot {Beweisbar}}({\dot {n}})$

Diagonalisierung

Der nächste Schritt besteht darin, eine Aussage zu konstruieren, die ihre eigene Unbeweisbarkeit behauptet. Hierzu lässt sich das Diagonallemma anwenden. Dieses besagt, dass es in der Arithmetik und stärkeren formalen Systemen für jede Formel $F(x)$ mit freier Variable $x$ eine Aussage $p$ gibt, sodass das System die Äquivalenz

p\Leftrightarrow F(G(p)).

beweist. Man erhält also eine Formel mit der intuitiven Bedeutung „Ich habe die Eigenschaft $F(x)$ .“ Wenn man für $F$ die Negation von $Beweisbar(x)$ einsetzt, erhält man die Aussage $p$ mit der Bedeutung „Meine Gödelnummer ist die Gödelnummer einer unbeweisbaren Formel“, also „Ich bin unbeweisbar“.

Die Formel $p$ ist nicht direkt gleich zu $\neg {\dot {Beweisbar}}(G(p))$ ; vielmehr besagt $p$ , dass man, wenn man eine gewisse Berechnung ausführt, die Nummer einer unbeweisbaren Aussage erhält. Wenn man nun diese Berechnung durchführt, zeigt sich aber, dass die entstehende Zahl die Gödelnummer von $p$ selbst ist. Diese Konstruktion ähnelt folgender natürlichsprachigen Aussage:

"ist in Anführungszeichen und gefolgt von sich selbst unbeweisbar." ist in Anführungszeichen und gefolgt von sich selbst unbeweisbar.

Dieser Satz bezieht sich nicht direkt auf sich selbst, aber man erhält die ursprüngliche Aussage, wenn man die angegebene Umformung durchführt, und damit behauptet der Satz seine eigene Unbeweisbarkeit. Der Beweis des Diagonallemmas benutzt eine ähnliche Methode.

Beweis der Unabhängigkeit des Gödelsatzes

Man nehme nun an, dass das formale System ω-konsistent, und damit konsistent, ist. Sei $p$ die Aussage, die im vorangehenden Abschnitt konstruiert wurde.

Wenn $p$ beweisbar wäre, dann wäre ${\dot {Beweisbar}}(G(p))$ beweisbar. Aber $p$ ist äquivalent zur Negation von ${\dot {Beweisbar}}(G(p))$ . Damit wäre das System inkonsistent, da es eine Aussage und ihre Negation beweisen würde. Also kann $p$ nicht beweisbar sein, da die Theorie nach Voraussetzung konsistent ist.

Wenn die Negation von $p$ beweisbar wäre, folgt aus der Konsistenz des Systems, dass $p$ nicht beweisbar ist. Daher kann keine natürliche Zahl $n$ die Gödelnummer eines Beweises von $p$ sein. Gleichzeitig ist die Negation von $p$ äquivalent zu ${\dot {Beweisbar}}(G(p))$ . Damit beweist das System einerseits die Existenz einer Zahl mit einer bestimmten Eigenschaft, aber beweist andererseits für jede Ziffer ${\dot {n}}$ , dass sie diese Eigenschaft nicht hat. Dies ist in einem $\omega$ -konsistenten System unmöglich. Damit ist die Negation von $p$ nicht beweisbar.

Damit ist die Aussage $p$ unentscheidbar: Sie kann im gewählten System weder bewiesen noch widerlegt werden. Damit ist das System $\omega$ -inkonsistent oder unvollständig. Diese Argumentation lässt sich auf jedes formale System, das die Voraussetzungen erfüllt, anwenden. Damit sind alle formalen Systeme, die die Voraussetzungen erfüllen, $\omega$ -inkonsistent oder unvollständig.

Dabei ist zu bemerken, dass $p$ auch dann nicht beweisbar ist, wenn das System konsistent und $\omega$ -inkonsistent ist. Die Annahme der $\omega$ -Konsistenz ist nur dazu nötig, zu zeigen, dass die Negation von $p$ nicht beweisbar ist.

Wenn man versucht, die Unvollständigkeit zu beseitigen, indem man eine der unbeweisbaren Formeln $p$ oder nicht $p$ als Axiom hinzufügt, erhält man ein neues formales System. Auf dieses lässt sich der gleiche Prozess anwenden und man erhält wieder eine Aussage der Form „Ich bin im neuen System nicht beweisbar.“ und das neue System ist wieder $\omega$ -inkonsistent oder unvollständig.

Verallgemeinerung von Rosser

Wie im vorangehenden Abschnitt gezeigt, erlaubt die Konstruktion des Gödelsatzes zunächst nur den Beweis der Unvollständigkeit für $\omega$ -konsistente Systeme. John Barkley Rosser zeigte 1936, dass sich mit der gleichen Technik die Unvollständigkeit auch für konsistente, aber $\omega$ -inkonsistente Systeme zeigen lässt.

Durch das Diagonallemma lässt sich ein Satz konstruieren, der die metasprachliche Bedeutung „Wenn es einen Beweis für mich gibt, dann gibt es einen kürzeren Beweis für meine Negation.“ hat. Dieser Satz wird auch als Rossersatz $R$ bezeichnet:

T\vdash R\leftrightarrow \forall y({\dot {Beweis}}(y,\mathbf {G} (R))\rightarrow \exists z{\dot {<}}y{\dot {Beweis}}(z,\mathbf {G} (\neg R)))

Angenommen das System ist konsistent und $R$ ist beweisbar, wobei es einen Beweis mit Gödelnummer $n$ gibt. Dann beweist das System $\exists z{\dot {<}}{\dot {n}}{\dot {Beweis}}(z,\mathbf {G} (\neg R)))$ und somit das äquivalente ${\dot {Beweis}}({\dot {0}},\mathbf {G} (\neg R)))\vee {\dot {Beweis}}({\dot {1}},\mathbf {G} (\neg R)))\vee ...\vee {\dot {Beweis}}({\dot {n-1}},\mathbf {G} (\neg R)))$ . Da ${\dot {Beweis}}(x,y)$ für alle Einsetzungen entscheidbar ist und das System nach Annahme konsistent ist, ist diese Aussage auch wahr in $\mathbb {N}$ . Damit gibt es eine Zahl $m<n$ , die Gödelnummer eines Beweises der Negation von $R$ ist. Damit beweist das formale System einen Satz und seine Negation, ist also inkonsistent, Widerspruch.

Nun nehme man an, das System sei konsistent und der Rossersatz sei widerlegbar, wobei es einen Beweis für die Negation mit Gödelnummer $n$ gibt. Da das System konsistent ist, ist $R$ nicht beweisbar. Dann ist beweisbar:

T\vdash \forall y(y{\dot {\leq }}{\dot {n}}\rightarrow \neg {\dot {Beweis}}(y,\mathbf {G} (R)))

Da es keinen Beweis für

R

gibt, gibt es auch keinen Beweis mit Gödelnummer kleiner gleich

n

. Damit ist die Formel wahr. Da es nur endlich viele Zahlen kleiner

n

gibt, ist die Formel äquivalent zu einer quantorenfreien Formel

(\neg {\dot {Beweis}}({\dot {0}},\mathbf {G} (R)))\wedge (\neg {\dot {Beweis}}({\dot {1}},\mathbf {G} (R)))\wedge ...\wedge (\neg {\dot {Beweis}}({\dot {n}},\mathbf {G} (R)))

und damit auch beweisbar.

T\vdash \forall y(n{\dot {<}}y\rightarrow \exists z{\dot {<}}y\ {\dot {Beweis}}(z,\mathbf {G} (\neg R)))

Für jede Zahl größer

n

findet man eine kleinere Zahl, die Nummer eines Beweises von

\neg R

ist. Dies folgt direkt daraus, dass

m

eine solche Nummer ist.

Damit lässt sich aber durch Kontraposition und Modus ponens beweisen:

T\vdash \forall y({\dot {Beweis}}(y,\mathbf {G} (R))\rightarrow \exists z{\dot {<}}y{\dot {Beweis}}(z,\mathbf {G} (\neg R)))

was dem Rossersatz $R$ entspricht. Dies ist ein Widerspruch, da $R$ nach Annahme nicht beweisbar sein kann. Also ist der Rossersatz in einem konsistenten System nicht widerlegbar.

Zweiter Unvollständigkeitssatz

Der zweite Unvollständigkeitssatz besagt:

Jedes hinreichend mächtige konsistente System kann die eigene Konsistenz nicht beweisen.

Eine hinreichende Bedingung für „hinreichend mächtig“ ist, dass der Beweis des ersten Unvollständigkeitssatzes im System formalisiert werden kann. Dazu muss es eine Formel $Bew(x)$ besitzen, die die Beweisbarkeit in diesem System ausdrückt. Zudem muss diese Formel den sogenannten Bernays-Löb-Axiomen genügen. Diese fordern, dass für alle Formeln $F$ und $H$ folgende Bedingungen gelten:

Wenn $T\vdash F$ , dann $T\vdash {\dot {Bew}}(\mathbf {G} (F))$
$T\vdash {\dot {Bew}}(\mathbf {G} (F\rightarrow H))\rightarrow ({\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} (H)))$
$T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {Bew}}(\mathbf {G} (F))))$

Dies ist zwar im System $Q$ , für das sich der erste Unvollständigkeitssatz bereits zeigen lässt, noch nicht erfüllt, aber bereits in der Primitiv Rekursiven Arithmetik (PRA), und erst recht in stärkeren Theorien wie der Peano-Arithmetik und der Mengenlehre.

Mithilfe dieser Eigenschaften lässt sich nun wie folgt der erste Unvollständigkeitssatz formalisieren.^[1] Sei $F$ die beim Beweis des ersten Satzes konstruierte Aussage mit der Bedeutung „Ich bin nicht beweisbar.“ Dann lassen sich folgende drei Aussagen ableiten:

$T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {Bew}}(\mathbf {G} (F))))$ (nach Axiom 3)
$T\vdash {\dot {Bew}}(\mathbf {G} (Bew(\mathbf {G} (F))))\rightarrow {\dot {Bew}}(\mathbf {G} (\neg F))$ (nach der Definition von F)
$T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow ({\dot {Bew}}(\mathbf {G} (\neg F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))$ (aus der Tautologie $T\vdash F\rightarrow (\neg F\rightarrow {\dot {0}}\doteq {\dot {1}})$ nach Axiom 1 und 2)

Durch Kontraposition erhält man aus diesen drei Sätzen folgenden Satz, der dem ersten Unvollständigkeitssatz entspricht:

$T\vdash \neg {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))\rightarrow \neg {\dot {Bew}}(\mathbf {G} (F))$

Um einen Widerspruch zu erzeugen, nehme man nun an, dass T seine Konsistenz beweist, das heißt $T\vdash \neg {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))$ . Damit gilt $T\vdash \neg {\dot {Bew}}(\mathbf {G} (F))$ , also $T\vdash F$ . Nach Axiom 1 gilt dann $T\vdash {\dot {Bew}}(\mathbf {G} (F))$ . Dann wäre aber T inkonsistent, da es sowohl ${\dot {Bew}}(\mathbf {G} (F))$ als auch $\neg {\dot {Bew}}(\mathbf {G} (F))$ beweist. Also kann T, wenn es konsistent ist, die eigene Konsistenz nicht beweisen.

Alternativ lässt sich der zweite Unvollständigkeitssatz auch durch den Satz von Löb beweisen. Nach diesem gilt für ein System $T$ , das die Bernays-Löb-Axiome erfüllt, die Aussage $T\vdash {\dot {Bew}}(\mathbf {G} (P))\rightarrow P$ nur dann, wenn auch $T\vdash P$ gilt. Wenn nun $T$ seine eigene Konsistenz beweist, gilt $T\vdash \neg {\dot {Bew}}(\mathbf {G} \bot )$ und damit $T\vdash ({\dot {Bew}}(\mathbf {G} \bot )\rightarrow \bot )$ . Nach dem Satz von Löb gilt also $T\vdash \bot$ , also ist $T$ inkonsistent.

Alternative Beweise

Es sind verschiedene andere Beweise des Unvollständigkeitssatzes bekannt, die im Gegensatz zu Gödels Beweis keine selbstbezügliche Formel benötigen. Direkte Beweise des ersten Unvollständigkeitssatzes für spezielle mächtige Systeme wie die Peano-Arithmetik oder die Zermelo-Fraenkel-Mengenlehre erhält man durch verschiedene Unbeweisbarkeitsresultate für mathematische Aussagen. Zudem gibt es auch verschiedene Beweise, die wie Gödels Beweis durch Formalisierung von Paradoxien die Unvollständigkeit aller ausreichend mächtigen formalen Systeme zeigen.

Halteproblem

Alan Turing zeigte 1937,^[2] dass sich der erste Unvollständigkeitssatz durch Mittel der Berechenbarkeitstheorie zeigen lässt.

Das Halteproblem ist die Menge der Gödelnummern von Paaren aus Turingmaschinen $T$ und Wörtern $w$ , sodass $T$ auf Eingabe $w$ nach endlich vielen Schritten anhält. Analog lässt sich das Halteproblem auch für andere Berechenbarkeitsmodelle definieren. Turing zeigte, dass das Halteproblem nicht entscheidbar ist. Es lässt sich zeigen, dass das Halteproblem arithmetisch repräsentierbar ist, es also eine arithmetische Formel $A(x,y)$ gibt, so dass $A(\mathbf {G} (T),\mathbf {G} (w))$ genau dann wahr ist, wenn $T$ auf Eingabe $w$ hält. Angenommen, die betrachtete Theorie ist vollständig und beweist nur arithmetisch wahre Formeln. Sei eine Turingmaschine $T$ und ein Wort $w$ gegeben. Dann kann man alle Beweise der Theorie systematisch durchsuchen, bis man einen Beweis für $A(\mathbf {G} (T),\mathbf {G} (w))$ oder $\neg A(\mathbf {G} (T),\mathbf {G} (w))$ findet. Da die Theorie vollständig ist, ist genau eine der beiden Formeln tatsächlich beweisbar. Damit ließe sich aber das Halteproblem entscheiden, Widerspruch. Also gibt es Turingmaschinen $T$ und Wörter $w$ , sodass $A(\mathbf {G} (T),\mathbf {G} (w))$ weder beweisbar noch widerlegbar ist.

Berry-Paradoxon

George Boolos zeigte 1989,^[3] dass sich der erste Unvollständigkeitssatz durch eine Formalisierung des Berry-Paradoxons beweisen lässt. Dieses besteht aus folgendem natürlichsprachigen Ausdruck:

„Die kleinste natürliche Zahl, die nicht mit weniger als vierzehn Worten definierbar ist.“

Da jede nichtleere Menge natürlicher Zahlen ein kleinstes Element hat und weil nur endlich viele Zahlen mit weniger als vierzehn Wörtern definiert werden können, definiert dieser Ausdruck eine Zahl. Das Paradoxon besteht nun darin, dass die benannte Zahl angeblich nicht in weniger als vierzehn Wörtern benannt werden kann, der Ausdruck aber nur dreizehn Wörter hat.

Dieses Paradoxon wird von Boolos wie folgt formalisiert. Eine Formel $F(x)$ benennt die Zahl $n$ , wenn das betrachtete System $T$ beweist, dass $n$ die einzige Zahl mit Eigenschaft $F(x)$ ist:

T\vdash \forall x(F(x)\leftrightarrow x\doteq {\dot {n}})

Nun gibt es ein arithmetisch definierbares Prädikat $C(x,z)$ , das genau dann wahr ist, wenn eine arithmetische Formel mit Länge $z$ die Zahl $x$ benennt. Damit lassen sich dann folgende Prädikate definieren:

B(x,y)\leftrightarrow \exists z(z<y\wedge C(x,z))

. „x kann mit weniger als y Symbolen benannt werden“

A(x,y)\leftrightarrow \neg B(x,y)\wedge \forall a(a{\dot {<}}x\rightarrow B(a,y))

„

x

ist die kleinste Zahl, die sich nicht mit weniger als

y

Symbolen definieren lässt“

Sei nun $k$ die Länge der Formel $A(x,y)$ . Dann betrachte man die Formel $A(x,{\dot {10}}{\dot {\times }}{\dot {k}})$ „ $x$ ist die kleinste Zahl, die sich nicht mit weniger als $10\times k$ Symbolen definieren lässt.“ Da nur endlich viele Zahlen mit weniger als $10\times k$ Symbolen definierbar sind, muss es eine Zahl $n$ geben, sodass $A(n,{\dot {10}}{\dot {\times }}{\dot {k}})$ wahr ist, und da es genau eine kleinste Zahl gibt, ist auch $\forall x(A(x,{\dot {10}}{\dot {\times }}{\dot {k}})\leftrightarrow x\doteq {\dot {n}})$ wahr. Wäre diese Formel beweisbar, dann würde $A(x,{\dot {10}}{\dot {\times }}{\dot {k}})$ die Zahl n benennen. Die Formel $A(x,{\dot {10}}{\dot {\times }}{\dot {k}})$ hat aber viel weniger Zeichen als 10·k, damit kann die Formel $\forall x(A(x,{\dot {10}}{\dot {\times }}{\dot {k}})\leftrightarrow x\doteq {\dot {n}})$ nicht beweisbar sein.

Gregory Chaitin zeigte 1974^[4] durch eine ähnliche Formalisierung des Berry-Paradoxons, dass es für jedes formale System, das keine falschen arithmetischen Aussagen beweist, eine Zahl $n$ gibt, sodass das System für keine Zahl beweisen kann, dass ihre Kolmogorow-Komplexität größer als $n$ ist.

Grelling-Nelson-Antinomie

Ein anderer Beweis lässt sich aus der Grelling-Nelson-Antinomie gewinnen.^[5] Eine Formel $F(x)$ mit freier Variable heiße autologisch, wenn $F({\bf {G}}(F(x)))$ beweisbar ist. Nun existiert eine arithmetische Formel $GG(x)$ (für „Gödel-Grelling-Formel“) mit der Bedeutung: „ $x$ ist nicht die Gödelnummer einer autologischen Formel.“ Nun betrachte man die Formel $GG({\bf {G}}(GG(x)))$ mit der Bedeutung „Die Formel $GG(x)$ ist nicht autologisch.“ Angenommen, die Formel sei beweisbar. Dann ist aber nach Definition $GG(x)$ autologisch und das System ist inkonsistent. Also ist die Formel $GG({\bf {G}}(GG(x)))$ unbeweisbar, aber, da sie ebendiese Unbeweisbarkeit behauptet, auch wahr. Wäre die Formel widerlegbar, dann wäre das System ähnlich wie bei Gödels Beweis $\omega$ -inkonsistent, würde also eine falsche Aussage beweisen.

Literatur

Kurt Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 1931, S. 173–198, doi:10.1007/BF01700692. Zentralblatt MATH.
Kurt Gödel: Diskussion zur Grundlegung der Mathematik: Erkenntnis 2. Monatshefte für Math. und Physik, 1931–32, S. 147–148.
J. Barkley Rosser: Extensions of some theorems of Gödel and Church. In: Journal of Symbolic Logic. Band 1, 1936, S. 87–91.

Einzelnachweise

↑ Die Beweisskizze folgt: Peter G. Hinman: Fundamentals of Mathematical Logic. A K Peters, 2005. , Seite 421–423.
↑ Alan Turing: On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, 2, 42 (1937), S. 230–265. Online-Fassung@1@2 (Seite nicht mehr abrufbar, festgestellt im Oktober 2022. Suche in Webarchiven)
↑ George Boolos: A New Proof of the Gödel Incompleteness Theorem. In: Notices of the American Mathematical Society. Band 36, 1989, S. 388–390 und 676. , Nachdruck in George Boolos: Logic, Logic, and Logic. Harvard University Press, 1998, ISBN 0-674-53766-1.
↑ Gregory Chaitin: Information-theoretic limitations of formal systems. In: Journal of the ACM (JACM). Band 21, Nr. 3. ACM, 1974, S. 403–424.
↑ George Boolos, John P. Burgess und Richard Jeffrey: Computability and Logic. 4. Auflage. Cambridge University Press, 2002, ISBN 0-521-70146-5. , Seite 227

Weblinks

Wikiversity: Kurs:Einführung in die mathematische Logik (Osnabrück 2011-2012) – Kursmaterialien

[1] Die Beweisskizze folgt: Peter G. Hinman: Fundamentals of Mathematical Logic. A K Peters, 2005. , Seite 421–423.

[2] Alan Turing: On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, 2, 42 (1937), S. 230–265. Online-Fassung@1@2 (Seite nicht mehr abrufbar, festgestellt im Oktober 2022. Suche in Webarchiven)

[3] George Boolos: A New Proof of the Gödel Incompleteness Theorem. In: Notices of the American Mathematical Society. Band 36, 1989, S. 388–390 und 676. , Nachdruck in George Boolos: Logic, Logic, and Logic. Harvard University Press, 1998, ISBN 0-674-53766-1.

[4] Gregory Chaitin: Information-theoretic limitations of formal systems. In: Journal of the ACM (JACM). Band 21, Nr. 3. ACM, 1974, S. 403–424.

[5] George Boolos, John P. Burgess und Richard Jeffrey: Computability and Logic. 4. Auflage. Cambridge University Press, 2002, ISBN 0-521-70146-5. , Seite 227

[1]

[2]

[3]

[4]

[5]