Literatur
A. Whitehead und B. Russell, Principia Mathematica, 2. Aufl., Cambridge 1925. Zu den Axiomen des Systems PM rechnen wir insbesondere auch: Das Unendlichkeitsaxiom (in der Form: es gibt genau abzählbar viele Individuen), das Reduzibilitäts- und das Auswahlaxiom (für alle Typen).
Vgl. A. Fraenkel, Zehn Vorlesungen über die Grundlegung der Mengenlehre, Wissensch. u. Hyp. Bd. XXXI. J. v. Neumann, Die Axiomatisierung der Mengenlehre. Math. Zeitschr. 27, 1928. Journ. f. reine u. angew. Math. 154 (1925), 160 (1929). Wir bemerken, daß man zu den in der angeführten Literatur gegebenen mengentheoretischen Axiomen noch die Axiome und Schlußregeln des Logikkalküls hinzufügen muß, um die Formalisierung zu vollenden. — Die nachfolgenden Überlegungen gelten auch für die in den letzten Jahren von D. Hilbert und seinen Mitarbeitern aufgestellten formalen Systeme (soweit diese bisher vorliegen). Vgl. D. Hilbert, Math. Ann. 88, Abh. aus d. math. Sem. der Univ. Hamburg I (1922), VI (1928). P. Bernays, Math. Ann. 90. J.v.Neumann, Math. Zeitschr. 26 (1927). W. Ackermann, Math. Ann. 93.
Dabei werden in PM nur solche Axiome als verschieden gezählt, die aus einander nicht bloß durch Typenwechsel entstehen.
Wir verstehen hier und im folgenden unter “Formel aus PM” immer eine ohne Abkürzungen (d. h. ohne verwendung von Definitionen) geschriebene Formel. Definitionen dienen ja nur der kürzeren Schreibweise und sind daher prinzipiell überflüssig.
D. h. wir bilden die Grundzeichen in eineindeutiger Weise auf natürliche Zahlen ab. (Vgl. die Durchführung auf S. 179.)
D. h. eine Belegung eines Abschnittes der Zahlenreihe mit natürlichen Zahlen. (Zahlen können ja nicht in räumliche Anordnung gebracht werden.)
m. a. W.: Das oben beschriebene Verfahren liefert ein isomorphes Bild des Systems PM im Bereich der Arithmetik und man kann alle metamathematischen Überlegungen ebenso gut an diesem isomorphen Bild vornehmen. Dies geschieht in der folgenden Beweisskizze, d. h. unter “Formel”, “Satz”, “Variable” etc. sind immer die entsprechenden Gegenstände des isomorphen Bildes zu verstehen.
Es wäre sehr leicht (nur etwas umständlich), diese Formel tatsächlich hinzuschreiben.
Etwa nach steigender Gliedersumme und bei gleicher Summe lexikographisch.
Durch Überstreichen wird die Negation bezeichnet.
Es macht wieder nicht die geringsten Schwierigkeiten, die FormelS tatsächlich hinzuschreiben.
Man beachte, daß “[R (q); q]” (oder was dasselbe bedeutet “[S; q]”) bloß eine metamathematische Beschreibung des unentscheidbaren Satzes ist. Doch kann man, sobald man die FormelS ermittelt hat, natürlich auch die Zahlq bestimmen und damit den unentscheidbaren Satz selbst effektiv hinschreiben.
Es läßt sich überhaupt jede epistemologische Antinomie zu einem derartigen Unentscheidbarkeitsbeweis verwenden.
Ein solcher Satz hat entgegen dem Anschein nichts Zirkelhaftes an sich, denn er behauptet zunächst die Unbeweisbarkeit einer ganz bestimmten Formel (nämlich derq-ten in der lexikographischen Anordnung bei einer bestimmten Einsetzung), und erst nachträglich (gewissermaßen zufällig) stellt sich heraus, daß diese Formel gerade die ist, in der er eelbst ausgedrückt wurde.
Die Hinzufügung der Peanoschen Axime ebenso wie alle anderen am System PM angebrachten Abänderungen dienen lediglich zur Vereinfachung des Beweises und sind prinzipiell entbehrlich.
Es wird vorausgesetzt, daß für jeden Variablentypus abzählbar viele Zeichen zur Verfügung stehen.
Auch inhomogene Relationen können auf diese Weise definiert werden, z. B. eine Relation zwischen Individuen und Klassen als eine Klasse aus Elementen der Form: ((x 2), ((x 1),x 2)). Alle in den PM über Relationen beweisbaren Sätze sind, wie eine einfache Überlegung lehrt, auch bei dieser Behandlungsweise beweisbar.
xII(a) ist also auch dann eine Formel, wennx ina nicht oder nicht frei vorkommt. In diesem Fall bedeutetxII(a) natürlich dasselbe wiea.
Bez. dieser Definition (und analoger später vorkommender) vgl. J. Łukasiewicz und A. Tarski, Untersuchungen über den Aussagenkalkül, Comptes Rendus des séances de la Société des Sciences et des Lettres de Varsovie XXIII, 1930, Cl. III.
x 1=y 1 ist, wie in PM I, * 13 durchx 2II (x 2(x 1) ⊅x 2(y 1)) definiert zu denken (ebenso für die höheren Typen).
Um aus den angeschriebenen Schemata die Axiome zu erhalten, muß man also (in II, III, IV nach Ausführung der erlaubten Einsetzungen) noch 1. die Abkürzungen eliminieren, 2. die unterdrückten Klammern hinzufügen. Man beachte, daß die so entstehenden Ausdrücke “Formeln” in obigem Sinn sein müssen. (Vgl. auch die exakten Definitionen der metamathem. Begriffe S. 182 fg.)
e ist also entweder eine Variable oder O oder ein Zeichen der Formf...f u, wou entweder O oder eine Variable 1. Typs ist. Bez. des Begriffs “frei (gebunden) an einer Stelle vona” vgl. die in Fußnote24) zitierte Arbeit I A 5.
Die Einsetzungsregel wird dadurch überflüssig, daß wir alle möglichen Einsetzungen bereits in den Axiomen selbst vorgenommen haben (analog bei j. v. Neumann, Zur Hilbertschen Beweistheorie, Math. Zeitschr. 26, 1927).
D. h. ihr Definitionsbereich ist die Klasse der nicht negativen ganzen Zahlen (bzw. dern-tupel von solchen) und ihre Werte sind nicht negative ganze Zhalen.
Kleine lateinische Buchstaben (ev. mit Indizes) sind im folgenden immer Variable für nicht negative ganze Zahlen (falls nicht ausdrücklich das Gegeuteil bemerkt ist).
Klassen rechner wir mit zu den Relationen (einstellige Relationen). Rekursive RelationenR haben natürlich die Eigenschaft, daß man für jedes spezielle Zahlen-n-tupel entscheiden kann, obR (x 1...x n ) gilt oder nicht.
Für alle inhaltlichen (insbes. auch die metamathematischen) Überlegungen wird die Hilbertsche Symbolik verwendet. Vgl. Hilbert-Ackermann, Grundzüge der theoretischen Logik, Berlin 1928.
Wir setzen als bekannt voraus, daß die Funktionenx+y (Addition),x, y (Multiplikation) rekursiv sind.
Andere Werte als 0 und 1 kanna, wie aus der Definition für α ersichtlich ist, nicht annehmen.
Das Zeichen ≠ wird im Sinne von “Definitionsgleichheit” verwendet, vertritt also bei Definitionen entweder=oder } (im übrigen ist die Symbolik die Hilbertsche).
Überall, wo in den folgenden Definitionen eines der Zeichen(x), (Ex), εx auftritt, ist es von einer Abschätzung fürx gefolgt. Diese Abschätzung dient lediglich dazu, um die rekursive Natur des definierten Begriffs (vgl. Satz IV) zu sichern. Dagegen würde sich der Umfang der definierten Begriffe durch Weglassung dieser Abschätzung meistens nicht ändern.
Für 0<n≦z, wennz die Anzahl der verschiedenen inx aufgehenden Primzahlen ist. Man beachte, daß fürn=z+1nPrx=0 ist!
m, n≦x steht für:m≦x&n≦x (ebenso für mehr als 2 Variable).
DieVariablen u 1...u n können willkürlich vorgegeben werden. Es gibt z. B. immer einr mit denfrein Variablen 17, 19, 23... usw., für welches (3) und (4) gilt.
Satz V beruht natürlich darauf, daß bei einer rekursiven RelationR für jedesn-tupel von Zahlen aus den Axiomen des SystemsP entscheidbar ist, ob die RelationR besteht oder nicht.
Daraus folgt sofort seine Geltung für jede rekursive Relation, da eine solche gleichbedeutend ist mit 0=ϕ (x 1...x n ), wo ϕ rekursiv ist.
Bei der genauen Durchführung dieses Beweises wird natürlichr nicht auf dem Umweg über die inhaltliche Deutung, sondern durch seine rein formale Beschaffenheit definiert.
Welches also, inhaltlich gedeutet, das Bestehen dieser Relation ausdrückt.
r entsteht ja aus dem rekursivenRelationszeichen q durch Ersetzen einerVariablen durch eine bestimmte Zahl (p).
Die Operationen Gen,Sb sind natürlich immer vertauschbar, falls sie sich auf verschiedeneVariable beziehen.
x istz-beweisbar, soll bedeuten:x ε Flg (κ), was nach (7) dasselbe besagt wie: Bewκ (x).
Denn alle im Beweise vorkommenden Existentialbehauptungen beruhen auf Satz V, der, wie leicht zu sehen, intuitionistisch einwandfrei ist.
Die Existenz widerspruchsfreier und nicht ω-widerspruchsfreier κ ist damit natürlich nur unter der Voraussetzung bewiesen, daß es überhaupt widerspruchsfreie κ gibt (d. h. daßP widerspruchsfrei ist).
Der Beweis von Voraussetzung 1. gestaltet sich hier sogar einfacher als im Falle des SystemsP, da es nur eine Art von Grundvariablen gibt (bzw. zwei bei J. v. Neumann).
Vgl. Problem III in D. Hilberts Vortrag: Probleme der Grundlegung der Mathematik. Math. Ann. 102.
Der wahre Grund für die Unvollständigkeit, welche allen formalen. Systemen der Mathematik anhaftet, liegt, wie im II. Teil dieser Abhandlung gezeigt werden wird, darin, daß die Bildung immer höherer Typen sich ins Transfinite fortsetzen läßt. (Vgl. D. Hilbert, Über das Unendliche, Math. Ann. 95, S. 184), während in jedem formalen System höchstens abzählbar viele vorhanden sind. Man kann nämlich zeigen, daß die hier aufgestellten unentscheidbaren Sätze durch Adjunktion passender höherer Typen (z. B. des Typus ω zum SystemP) immer entscheidbar werden. Analoges gilt auch für das Axiomensystem der Mengenlehre.
Die Null wird hier und im folgenden immer mit zu den natürlichen Zahlen gerechnet.
Das Definiens eines solchen Begriffes muß sich also allein mittels der angeführten Zeichen, Variablen für natürlichen Zahlenx, y,... und den Zeichen 0, 1 aufbauen (Funktions- und Mengenvariable dürfen nicht vorkommen). (In den Präfixen darf stattx natürlich auch jede andere Zahlvariable stehen.)
f bedeutet hier eine Variable, deren Wertbereich die Folgen natürl. Zahlen sind. Mitf k wird dask+1-te Glied einer Folgef bezeichnet (mitf o das erste).
Das sind diejenigen ω-widerspruchsfreien Systeme, welche ausP durch Hinzufügung einer rekursiv definierbaren Klasse von Axiomen entstehen.
Vgl. Hilbert-Ackermann, Grundzüge der theoretischen Logik. Im SystemP 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.
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).
D. Hilbert und 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ßnote55) zitierte Arbeit).
Und zwar soll der Definitionsbereich immer der ganze Individuenbereich sein.
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.
D. h. die Konjunktion bildet.
Aus Satz X folgt z.B., daß das Fermatsche und das Goldbachsche Problem lösbar wären, wenn man das Entscheidungsproblem des e.F. gelöst hätte.
Satz IX gilt natürlich auch für das Axiomensystem der Mengenlehre und dessen Erweiterungen durch rekursiv definierbare ω-widerspruchsfreie Klassen von Axiomen, da es ja auch in diesen Systemen unentscheidbare Sätze der Form(x)F(x) (F rekursiv) gibt.
χ ist widerspruchsfrei (abgekürzt als Wid (χ)) wird folgendermaßen definiert: Wid(χ)≡(Ex) [Form (x)&Bewκ(x)].
Dies folgt, wenn man für χ die leere Klasse vonFormeln einsetzt.
r hängt natürlich (ebenso wiep) von κ ab.
Von der Definition für “rekursiv” auf Seite 179 bis zum Beweis von Satz VI inkl.
Daß aus (23) auf die Richtigkeit vonw Imp (17 Genr) geschlossen werden kann, beruht einfach darauf, daß der unentscheidbare Satz 17 Genr, wie gleich zu Anfang bemerkt, seine eigene Unbeweisbarkeit behauptet.
Vgl. J. v. Neumann, Zur Hilbertschen Beweistheorie, Math. Zeitschr. 26, 1927.
Author information
Authors and Affiliations
Additional information
Vgl. die im Anzeiger der Akad. d. Wiss. in Wien (math.-naturw. Kl.) 1930, Nr. 19 erschienene Zusammenfassung der Resultate dieser Arbeit.
Rights and permissions
About this article
Cite this article
Gödel, K. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatsh. f. Mathematik und Physik 38, 173–198 (1931). https://doi.org/10.1007/BF01700692
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01700692