On formally undecidable propositions of Principia Mathematica and related systems I.
(German: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.)
Kurt Gödel, Wien
[Section] 3.
Wir ziehen nun aus Satz VI weitere Folgerungen und geben zu diesem Zweck folgende Definition:
Eine Relation (Klasse) heißt arithmetisch, wenn sie sich allein mittels der Begriffe +, . [Addition und Multiplikation, bezogen auf natürliche Zahlen, (x), = definieren l Zahlen beziehen dürfen Entsprechend wird der Begriff "arithmetischer Satz" definiert. Insbesondere sind z.B. Die Relationen "größer" und "kongruent nach einem Modul" arithmetisch, denn as gilt: x > y ~(Ez) [y = x + z]
x º y (mod n) ~(Ez) [(x
= y + z & n) Ú (y = x + z & n)] Es gilt der
Satz VII: Jede
rekursive Relation ist arithmetisch.
Wir beweisen den Satz in der Gestalt: Jede Relation der Form x0 = j (x1 ... xn) wo j rekursiv ist, ist arithmetisch, und wenden vollständige Induktion nach der Stufe von j an. j habe die s-te Stufe (s > 1). Dann gilt entweder:
1. j (x1 ...
xn) = r [c1 (x1 … xn), c2 (x1 … xn),
… cm (x1 … xn)]5 (wo r und sämtliche ci kleinere Stufe haben als s) oder:
2. j (0, x2
... xn) = y (x2 … xn)
j (k + 1, x2 ... xn) = m [k, j (k, x2 … xn),
x2 … xn]
(wo y, m niedrigere Stufe
als s haben).
Im ersten Falle
gilt:
x0 =
j (x1 … xn) ~(E y1 … ym) [R (x0,
x1 … xn) & S1(y1, x1
… xn) & ... & Sm(ym x1 … xn)]
wo R bzw. Si die
nach induktiver Annahme existierenden mit x0 = r (y1 … ym) bzw. y = ci(x1 ... xn)
äquivalenten arithmetischen Relationen sind. Daher ist x0 = j (x1 … xn) in diesem Fall arithmetisch.
Im zweiten Fall
wenden wir folgendes Verfahren an: Man kann die Relation x0 = (x1 …
xn) mit Hilfe des
Begriffes „Folge von Zahlen“ (f)52
folgendermaßen ausdrücken:
x0 = j (x1 … xn)
~(E f) {f0 = y (x2 … xn) & (k) [k <
x1 Þ fk+1 = (k, fk,
x2 … xn)] & x0 = fx1}
Wenn S (y, x2 … xn) bzw. T (z, x1
… xn + 1) die nach
induktiver Annahme existierenden mit y = (x2 … xn)
bzw. z = (x1 … xn + 1)
äquivalenten arithmetische Relationen sind, gilt daher:
x0 = j (x1 … xn)
~(E f) {S (f0 = (x2
… xn) & (k) [k < x1 Þ T (fk+1, k, fk, x2
… xn)] & x0 = fx1}
Nun ersetzen wir den Begriff “Folge von Zahlen” durch
“Paar von Zahlen”, indem wir dem
Zahlenpaar n, d die Zahlenfolge f(n, d) (fk(n,
d) = [n]1 + (k + 1) d) zuordnen, wobei [n]p den
kleinsten nicht negativen Rest von n
modulo p bedeutet.
Es gilt
dann der
Hilfssatz
1: Ist f eine beliebige Folge natürlicher Zahlen und k eine
beliebige natiirliche Zahl, so gibt es
ein Paar von natürlichen Zahlen n, d, so daß f(n, d) und f in
den ersten k Gliedern
übereinstimmen.
Beweis:
Sei l die größte der Zahlen k, f0, f1, … fk
- 1. Man bestimme n so, daß:
n º fi [mod (1 + (i + 1) l!)] für i = 0, 1, ... k - 1
was möglich ist, da je zwei der Zahlen 1 + (i + 1) l! (i = 0, 1, ... k – 1) relativ prim sind. Denn eine in zwei von diesen Zahlen enthaltene Primzahl müßte auch in der Differenz (i1 – i2) l! und daher wegen |i1 - i2| < l in l! enthalten sein, was unmöglich ist. Das Zahlenpaar n, l! leistet dann das Verlangte.
Da die
Relation x = [n]p durch:
x º n (mod p) & x < p
definiert
und daher arithmetisch ist, so ist auch die folgendermaßen definierte Relation
P (x0, xl … xn):
P (x0
... xn) º
(E n,
d) {S[([n]d + 1, x2 ... xn)
& (k) [k < x1 Þ T ([n]1 + d (k + 2),
k, [n]1 + d (k + 1), (x2 … xn)] & x0 = [n]1
+ d (x1 + 1)}
arithmetisch,
welche nach (17) und Hilfssatz 1 mit: x0 = j (x1 … xn) äquivalent ist (es kommt bei der Folge f in (17) nur auf ihren
Verlauf bis zum x1 + 1-ten Glied an). Damit ist Satz VII bewiesen.
Gemäß
Satz VII gibt es zu jedem Problem der Form (x)F(x) (F rekursiv) ein
äquivalentes arithmetisches Problem und
da der ganze Beweis von Satz VII sich (für jedes spezielle F) innerhalb
des
Systems P formalisieren läßt, ist diese Äquivalenz in P beweisbar. Daher gilt:
Satz
VIII: In jedem der in Satz VI genannten formalen Systeme53
gibt es unentscheidbare arithmetische Sätze.
Dasselbe
gilt (nach der Bemerkung auf Seite 190) für das Axiomensystem der Mengenlehre
und dessen Erweiterungen durch v-widerspruchsfreie rekursive
Klassen von Axiomen.
Wir leiten schließlich noch folgendes Resultat hier:
Satz IX: In allen in Satz VI genannten formalen Systemen (53) gibt es unentscheidbare Probleme des engeren Funktionenkalküls54 (d. h. Formeln des engeren Funktionenkalküls, für die weder Allgemeingültigkeit noch Existenz eines Gegenbeispiels beweisbar ist)55.
Dies
beruht auf:
Satz X:
Jedes Problem der Form (x)F(x) (F rekursiv) läßt sich zurückführen auf die
Frage nach der Erfüllbarkeit einer
Formel des engeren Funktionenkalküls (d.h. zu jedem rekursiven F kann man eine Formel des engeren Funktionenkalküls
angeben deren Erfüllbarkeit mit der Richtigkeit von (x)F(x) äquivalent ist).
Zum
engeren Funktionenkalkül (e. F.) rechnen wir diejenigen Formeln, welche sich
aus den Grundzeichen: ~, Ú, (x), =; x, y ... (Individuenvariable)
F (x), G (x, y), H (x, y, z)... (Eigenschafts-
und Relationsvariable) aufbauen56,
wobei (x) und = sich nur auf Individuen beziehen dürfen. Wir fügen zu diesen Zeichen noch eine dritte Art
von Variablen j (x), w (x, y), c (x, y, z) etc.
hinzu, die Gegenstandsfunktionen
vertreten (d. h. j (x), w (x, y) etc.) bezeichnen eindeutige Funktionen, deren Argumente und Werte Individuen sind57. Eine Formel, die außer den zuerst
angeführten Zeichen des e. F. noch Variable dritter Art j ( (x), w (x, y) ... etc.)
enthält, soll eine Formel im weiteren Sinne (i. w. S.) heißen58. Die Begriffe "erfüllbar",
"allgemeingültig" übertragen sich ohneweiters auf Formeln i. w. S.
und es gilt der Satz, daß man zu jeder Formel i. w. S. A eine gewöhnliche
Formel des e. F. B angeben kann, so daß
die Erfüllbarkeit von A mit der von B äquivalent ist. B erhält man aus A, indem man die in A vorkommenden Variablen
dritter Art j (x), w (x, y) ... durch Ausdrücke der
Form: (i, z) F (z, x), (i, z) G (z, x, y) ... ersetzt, die "beschreibenden" Funktionen im
Sinne der PM. I * 14 auflöst und die so
erhaltene Formel mit einem Ausdruck logisch multipliziert59,
der besagt, daß sämtliche an Stelle der j, w .. gesetzte F, G .. hinsichtlich der ersten Leerstelle genau eindeutig
sind.
Wir
zeigen nun, daß es zu jedem Problem der Form (x)F(x) (F rekursiv) ein
äquivalentes betreffend die
Erfüllbarkeit einer Formel i.w.S. Gibt, woraus nach der eben gemachten
Bemerkung Satz X folgt.
Da F
rekursiv ist, gibt es eine rekursive Funktion F (x), so daß F(x) ~[F (x) = 0], und für F gibt es eine Reihe von Funktionen F1, F2 ... Fn, so daß: Fn = F, F1 (x) = x + 1 und für jedes Fk (1 < k ≦ n)
entweder:
1. (x2,
... xm) [Fk (0, x2 ... xm) = Fp (x2 ... xm)]
(18)
(x, x2
... xm) {Fk [F1 (x), x2
... xm] = Fq [x, Fk (x, x2 ... xm), x2
... xm]}
p, q < k
oder:
r < k, iʋ < k (für ʋ = l, 2 ... s)
oder:
3. (x1 ... xm)
[Fk (x1 ... xm)] = F1 (F1 ... F1 (0))] (20)
Ferner bilden wir die Sätze:
(x) F1 (x) = 0 & (x, y)
[F1 (x) = F1 (y) Þ x = y] (21)
(x)
[Fn (x) = 0] (22)
Wir
ersetzen nun in allen Formeln (18), (19), (20) (für k = 2, 3 . . . n) und in
(21) (22) die Funktionen i durch
Funktionsvariable i, die Zahl 0 durch eine sonst nicht vorkommende
Individuenvariable 0 und bilden die Konjunktion C sämtlicher so erhaltener
Formeln.
Die
Formel (E x0) C hat dann die verlangte Eigenschaft, d. b.
1. Wenn (x) [ (x) = 0] gilt, ist (E x0) C erfüllbar, denn die Funktionen F1, F2 ... Fn ergeben dann offenbar in (E x0) C für 1,
2 ... n eingesetzt einen richtigen Satz.
2. Wenn (E x0) C erfüllbar ist, gilt (x) [F (x) = 0].
Beweis: Seien Ψ1,
Ψ2 ... Ψn die
nach Voraussetzung existierenden Funktionen, welche in (E x0) C für φ1, φ2 ... φn eingesetzt einen richtigen Satz liefern. Ihr
Individuenbereich sei Á. Wegen der Richtigkeit von (E x0)
C für die Funktionen Ψi
gibt es ein Individuum a (aus Á), so daß sämtliche Formeln (18) bis
(22) bei Ersetzung der Fi durch Ψi und von 0 durch a in richtige Sätze (18') bis (22') übergehen. Wir bilden nun die kleinste
Teilklasse von Á, welche a enthält und gegen die Operation Ψ1
(x) abgeschlossen ist. Diese Teilklasse
(Á) hat die Eigenschaft, daß jede der Funktionen Ψi, auf Elemente
aus Á angewendet wieder Elemente aus Á ergibt. Denn für Ψ1 gilt dies
nach Definition von Á und wegen (18'), (19'), (20') überträgt sich diese Eigenschaft von Ψi mit niedrigerem Index auf solche mit höherem. Die Funktionen, welche
aus Ψi durch Beschränkung
auf den Individuenbereich Á entstehen, nennen wir Ψi'. Auch für diese Funktion
gelten sämtliche Formeln (18) bis (22)
(bei der Ersetzung von 0 durch a und Fi durch Ψi').
Wegen der Richtigkeit
von (21) für Ψ1' und a
kann man die Individuen aus Á eineindeutig auf die natürlichen Zahlen
abbilden u. zw. so, daß a in 0 und
die Funktion Ψ1' in die Nachfolgerfunktion F1 übergeht.
Durch diese Abbildung gehen aber sämtliche Funktionen Ψi' in die Funktionen Fi über und wegen der Richtigkeit von (22)
für Ψnʹ und a gilt (x) [Fn (x) = 0], oder (x) [F (x) = 0], was
zu beweisen war61.
Da man die Überlegungen, welche zu Satz X führen, (für jedes spezielle F)
auch innerhalb des Systems P durchführen kann, so ist die Äquivalenz zwischen
einem Satz der Form (x) F (x) (F rekursiv) und der Erfüllbarkeit der entsprechenden
Formel des e. F. in P beweisbar und daher folgt aus der Unentscheidbarkeit des
einen die des anderen, womit Satz IX bewiesen ist.[61]
[Section] 4.
Aus den Ergebnissen von Abschnitt 2 folgt Bin merkwürdiges Resultat, bezüglich
eines Widerspruchslosigkeitsbeweises des Systems P (und seiner Erweiterungen),
das durch folgenden Satz ausgesprochen wird:
Satz XI: Sei x eine beliebige
rekursive widerspruchsfreie[62] Klasse von
Formeln, dann gilt: Die Satzformel,
welche besagt, daß x widerspruchsfrei
ist, ist nicht x-beweisbar;
insbesondere ist die Widerspruchsfreiheit von P in P unbeweisbar[63],
vorausgesetzt, daß P widerspruchsfrei ist (im entgegengesetzten Fall ist natürlich
jede Aussage beweisbar).
Der Beweis ist
(in Umrissen skizziert) der folgende: Sei x
eine beliebige für die folgenden Betrachtungen ein für allemal gewählte
rekursive Klasse von Formeln (im
einfachsten Falle die leere Klasse). Zum
Beweise der Tatsache, daß 17 Gen r nicht
x-beweisbar ist[64], wurde,
wie aus 1. Seite 189 hervorgeht, nur die
Widerspruchsfreiheit von x benutzt,
d, h. es gilt:
Wid (x) Þ Bewx (17 Gen r) (23)
d. h. nach (6·1):
Wid (x) Þ (x) x
Bx (17 Gen r)
Nach (13) ist
17 Gen r = S b (p (19 / Z(p))) und daher:
Wid (x) Þ (x) x Bx S b (p
(19 / p Z(p)))
d. h. nach (8·1):
Wid (x) Þ (x) Q (x, p) (24)
Wir stellen nun folgendes fest: Sämtliche
in Abschnitt 266 und Abschnitt 4 bisher
definierte Begriffe (bzw. bewiesene Behauptungen) sind auch in P ausdrückbar
(bzw. beweisbar). Denn es wurden überall nur die gewöhnlichen Definitions- und
Beweismethoden der klassischen Mathematik verwendet, wie sie im System P
formalisiert sind. Insbesondere ist z (wie jede rekursive Klasse) in P
definierbar. Seit w die Satzformel, durch welche in P Wid (x)
ausgedrückt wird. Die Relation Q (x, y) wird gemäß (8·1), (9), (10) durch das Relationszeichen
q ausgedrückt, folglich Q (x,
p) durch r [ da nach (12) r = S b (q (19 / Z(p))] und der
Satz (x) Q (x, p) durch 17 Gen r.
Wegen (24) ist
also w Imp (17 Gen r) in P beweisbar67 (um so mehr x-beweisbar). Wäre
nun v x-beweisbar, so wäre auch 17 Gen r x-beweisbar
und daraus würde nach (23) folgen, daß x nicht widerspruchsfrei ist.
Es sei bemerkt,
daß auch dieser Beweis konstruktiv ist, d. h. er gestattet, falls ein Beweis aus x für w vorgelegt ist, einen Widerspruch aus x effektiv herzuleiten. Der ganze Beweis
für Satz XI läßt sich wörtlieh auch auf
das Axiomensystem der Mengenlehre M und der klassischen Mathematik68 A übertragen und liefert auch hier das
Resultat: Es gibt keinen Widerspruchslosigkeitsbeweis für M bzw. A, der
innerhalb von M bzw. A formalisiert werden könnte, vorausgesetzt daß M bzw. A
widerspruchsfrei ist. Es sei ausdrücklich bemerkt, daß Satz XI (und die entsprechenden
Resultate über M, A) in keinem Widerspruch
zum Hilbertschen formalistischen Standpunkt stehen. Denn dieser setzt nur die
Existenz eines mit finiten Mitteln geführten Widerspruchsfreiheitsbeweises
voraus und es wäre denkbar, daß es finite Beweise gibt, die sich in P (bzw. M,
A) nicht darstellen lassen.
Da für jede
widerspruchsfreie Klasse x, v nicht x-beweisbar ist, so gibt es
schon immer dann (aus x) unentscheidbare Sätze (nämlich w), wenn Neg (w) nicht x-beweisbar ist; m. a. W. man kann in Satz VI
die Voraussetzung der v-Widerspruchsfreiheit ersetzen durch die folgende: Die Aussage "x ist widerspruchsvoll" ist nicht x-beweisbar.
(Man beachte, daß
es widerspruchsfreie x gibt, für die diese Aussage x-beweisbar ist.)
Wir haben uns in
dieser Arbeit im wesentlichen auf das System P beschränkt und die
Anwendungen auf andere Systeme nur
angedeutet. In voller Allgemeinheit werden die Resultate in einer demnächst erscheinenden Fortsetzung
ausgesprochen und bewiesen werden. In dieser Arbeit wird auch der nur skizzenhaft geführte Beweis von
Satz XI ausführlich dargestellt werden.
(Eingelangt: 17. XI.
1930.)
___________
Temporary
note: The szmbol, Á, has been used incorrectly in the above text
and I am to replace it with something like ʒ´, Ҙ´, or
Ӡ´, whereof the last is probably the best. - Olsnes-Lea, the provider for this!
Notes:49 Die Null wird hier und im folgenden immer mit zu den natarlichen
Zahlen gerechnet.
50 Das Definiens eines solchen Begriffes muß sich
also allein mittels der
angeführten Zeichen, Variablen für
natürliche Zahlen x, y, . . . und den Zeiehen
0, 1 aufbauen (Funktions- und
Mengenvariable dürfen nicht vorkommen). (In den
Präfixen darf statt x natürlich auch jede
andere Zahlvariable stehen.)
51 Es
brauchen natürlich nicht alle x1 . . . xn in den ci tatsächlich vorzukommen
[vgl. das Beispiel in Fußnote 27].
52 f
bedeutet hier eine Variable, deren Wertbereich die Folgen natürl. Zahlen sind.
Mit fk wird das k + 1-te Glied einer Folge f bezeichnet (mit f0 das erste).
53 Das sind diejenigen v-widerspruchsfreien
Systeme, welche aus P durch Hinzufügung einer rekursiv definierbaren Klasse von
Axiomen entstehen.
54 Vgl. Hilbert-Ackermann, Grundzüge der
theoretischen Logik.
Im System P sind unter Formeln des engeren
Funktionenkalküls diejenigen zu verstehen, welche aus den Formeln des engeren
Funktionenkalküls der PM durch die auf S.176 angedeutete Ersetzung der
Relationen durch Klassen höheren Typs entstehen.
55 In meiner Arbeit: Die Vollständigkeit der
Axiome des logischen Funktionenkalküls, Monatsh. f. Math. u. Phys. XXXVII, 2, habe ich gezeigt, daß jede Formel
des engeren Funktionenkalküls entweder als allgemeingültig nachweisbar ist oder ein Gegenbeispiel
existiert; die Existenz dieses Gegenbeispiels ist aber nach Satz IX nicht
immer nachweisbar (in den angeführten
formalen Systemen).
56 D. Hilbert and W. Ackermann rechnen in dem eben
zitierten Buch das Zeichen = nicht zum
engeren Funktionenkalkül. Es gibt aber zu jeder Formel, in der das
Zeichen = vorkommt, eine solche ohne
dieses Zeichen, die mit der ursprünglichen gleichzeitig erfüllbar ist (vgl. die
in Fußnote 55) zitierte
Arbeit).
57 Und zwar soll der Definitionsbereich immer der
ganze Individuenbereich sein.
58 Variable dritter Art dürfen
dabei an allen Leerstellen für Individuenvariable stehen, z.B.: y = (x),
F(x, (y)), G [(x, (y)), x] : usw.
59 D.h. die Konjunktion bildet.
60 Ái (i = l .. s) vertreten irgend welche Komplexe der Variablen x1, x2 ... xm, z. B.: x1 x3 x2.
61 Aus Satz X folgt z. B., daß das Fermatsche und das Goldbachsche Problem 1ösbar wären, wenn man das Entscheidungsproblem des e. F. gelöst hätte.
62 Satz IX gilt natürlich auch für das Axiomensystem der Mengenlehre und dessen Erweiterungen durch rekursiv definierbare w-widerspruchsfreie Klassen von Axiomen, da es ja auch in diesen Systemen unentscheidbare Sätze der Form (x) F (x) (F rekursiv) gibt.
66 Von der Definition für "rekursiv" auf Seite 179 bis zum
Beweis von Satz VI inkl.60 Ái (i = l .. s) vertreten irgend welche Komplexe der Variablen x1, x2 ... xm, z. B.: x1 x3 x2.
61 Aus Satz X folgt z. B., daß das Fermatsche und das Goldbachsche Problem 1ösbar wären, wenn man das Entscheidungsproblem des e. F. gelöst hätte.
62 Satz IX gilt natürlich auch für das Axiomensystem der Mengenlehre und dessen Erweiterungen durch rekursiv definierbare w-widerspruchsfreie Klassen von Axiomen, da es ja auch in diesen Systemen unentscheidbare Sätze der Form (x) F (x) (F rekursiv) gibt.
63 x ist widerspruchsfrei
(abgekürzt als Wid (x)) wird folgendermaßen definiert: Wid (x) ≡ (E x) [Form (x) & Bewx (x)].
64 Dies folgt, wenn man
für x die leere Klasse von Formeln einsetzt.
65 r hängt natürlich (ebenso wie p) von x ab.
67 Daß aus (23) auf die Riehtigkeit von v Imp (17 Gen r)
geschlossen werden kann, beruht einfach darauf, daß der unentscheidbare Satz 17
Gen r, wie gleich zu Anfang bemerkt, seine eigene Unbeweisbarkeit
behauptet.
68 Vgl. J. v. Neumann, Zur Hilbertschen Beweistheorie, Math. Zeitschr.
26, 1927.
The rest is coming (section 3 and 4), wholly translated! Notes are now in.
Hirzel's paper: Hirzel, Martin, 2000, On formally undecidable propositions of Principia Mathematica and related systems I., successful, I think.
I am no novice and I hold credits, respects, as achievements, the Fitch
presentation of Gödel's Ontological Argument, now damn clear, and for resetting
the above mentioned paper totally new and toward completeness myself, countering
this paper and envisioning a new angle toward investigations to completeness
instead, introducing the two levels of axioms and logical results as basis for
this! Cheers!
