Zusammenfassung
Die erste wichtige Publikation Gerhard Gentzens ist seine 1934 erschienene Dissertation. In ihr wird zwar noch nicht der berühmte Beweis der Widerspruchsfreiheit der Zahlentheorie vorgelegt, die Arbeit enthält jedoch äußerst wichtige Vorarbeiten dazu. Daher soll ihr im Folgenden zuerst die Aufmerksamkeit zugewendet werden (4.1, S. 276). Gentzen hat seinen ersten Widerspruchsfreiheitsbeweis für die Zahlentheorie kurz vor der Publikation 1936 in wichtigen Passagen geändert. Es wird im Folgenden zuerst die ursprüngliche Fassung von 1935 behandelt, die von Paul Bernays posthum 1974 veröffentlicht wurde (4.2, S. 285), und dann die erste publizierte Version von 1936 (4.3, S. 299).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Gentzen, Untersuchungen I [1934a] und Gentzen, Untersuchungen II [1934b]. – Zu Gentzens Person bietet eine umfangreiche Informationssammlung Menzler-Trott, Gentzens [2001]; eine gute Übersicht auch in den kürzeren Lexikonartikeln Schütte, Art. Gentzen [1964]; Szabo, Art. Gentzen [1972]; sowie in den Art. Gentzen in: Deutsche biographische Enzyklopädie (DBE), Bd. 3, München: Saur, S. 625, und in: Biographisch-literarisches Handwörterbuch der exakten Naturwissenschaften, Bd. 7,2, Berlin: Akademie 1958, S. 185.
- 2.
Vgl. Bernays, Hilberts Untersuchungen [1935], 211–212, 215–216. Bernays hat sich in seiner Darstellung mit äußerster Sorgfalt darum bemüht, einerseits die grundlegenden Intentionen des Hilbertschen Ansatzes der Beweistheorie zu wahren, andererseits aber die notwendigen Konsequenzen aus den Gödelschen Unvollständigkeitssätzen zu ziehen.
- 3.
Gentzen, Untersuchungen I [1934a] und Gentzen, Untersuchungen II [1934b]. – Zu Gentzens Promotion siehe Menzler-Trott, Gentzens [2001], 55–60.
- 4.
Die Ersetzung der logischen Axiome durch Regeln hatte Vorbilder, die in früheren Kapiteln schon besprochen wurden. Zu nennen sind hier die Studien zur gegenseitigen Ersetzbarkeit von aussagenlogischen Axiomen und Regeln in Bernays Habilitationsschrift Bernays, Habilschrift [1918]; dann Hilberts Manuskript von 1920/21, in dem er die Aussagenlogik für → mittels Regeln gestaltet, vgl. Abschn. 9.5.1; die Axiomatisierung der vollen Aussagenlogik in Hilberts Vorlesungen ab 1921, vgl. Abschn. 9.6; und schließlich Hilbert/Ackermann, Theoretische Logik [1928], worin die logischen Axiome schon große Ähnlichkeit mit den Regeln des natürlichen Schließens haben.
- 5.
Wie schon im Bezug auf Ackermanns Arbeit bemerkt, werden auch bei Gentzen keine festen formalen Alphabete angegeben, sondern – hier sogar expressis verbis – bloß Zeichenarten unterschieden. Diese Tatsache stützt die bei Ackermann geäußerte Vermutung, daß dieses Vorgehen zur damaligen Zeit in der Hilbert-Schule allgemein üblich gewesen ist.
- 6.
Bei Gentzen: „Zeichen für bestimmte Gegenstände“, „bestimmte Funktionen“, „bestimmte Prädikate“ und „bestimmte Aussagen“.
- 7.
Es ist interessant zu bemerken, daß Gentzens Herleitungsbegriff („Herleitung“ oder auch „Beweisfigur“) genau aus diesem Grund der Nähe zum wirklichen mathematischen Vorgehen i. A. keine Baumstruktur hat, denn eine einmal hergeleitete Formel kann mehrfach als Oberformel von Schlüssen auftreten. Die Baumstruktur läßt sich natürlich leicht herstellen, indem man die Herleitung der mehrfach als Oberformel auftretenden Formel vervielfältigt. Gentzen kann daher ohne Beschränkung der Allgemeinheit sagen, es seien im Folgenden nur „stammbaumförmige Herleitungen zu betrachten“; vgl. Gentzen, Untersuchungen I [1934a], 181.
- 8.
Vgl. dazu auch die Anmerkung in Fußnote 7 oben.
- 9.
Vgl. zu dieser Feststellung auch das Diktum Hilberts von 1931, das Tertium non datur habe eine Sonderstellung, da es nicht wie die anderen Schlußregeln und Axiome auf eine Definition hinauslaufe; außerdem Hilberts Lehre von der Definition von Grundbegriffen durch Axiome (erster Teil, Abschn. 3.3).
- 10.
Gentzen, Untersuchungen I [1934a], 190.
- 11.
Vgl. hierzu auch Gentzens entsprechenden Beweis in Gentzen, Untersuchungen II [1934b], 407–408.
- 12.
Vgl. Gentzen, Untersuchungen I [1934a], 193.
- 13.
Zu diesem Grundgedanken vgl. auch Gentzen, Untersuchungen I [1934a], 203.
- 14.
Gentzen, Untersuchungen II [1934b].
- 15.
Vgl. Hilbert/Ackermann, Theoretische Logik [1928], 65.
- 16.
Gentzen, Widerspruchsfreiheit [1936a].
- 17.
Gentzen, Collected Papers [1969], 201–213.
- 18.
Gentzen, Der erste [1974a].
- 19.
Vgl. für die Funktionen Nr. 13.12 und für die Prädikate Nr. 13.3 in Gentzen, Der erste [1974a], 101.
- 20.
Vgl. Gentzen, Widerspruchsfreiheit [1936a], 20–24.
- 21.
Gentzen, Untersuchungen I [1934a] und Gentzen, Untersuchungen II [1934b]; vgl. Abschn. 12.1
- 22.
Gentzen selbst bemerkt die Ähnlichkeit dieses Kalküls mit NK in einer Fußnote, ohne allerdings auf den Unterschied einzugehen, der in der Verwendung von Sequenzen besteht.
- 23.
Die Hinterformel der Endsequenz eines Beweises wird hier kurz „Endformel“ genannt. – Für den finiten Standpunkt, dem sich Gentzen verpflichtet fühlte, ist es wesentlich, daß solche Beweistransformationen an einem hypothetisch vorliegenden konkreten Beweis durchgeführt werden. Vgl. z. B. Gentzens Formulierung: „Es liege irgendeine zahlentheoretische Herleitung […] vor. […] Ich beginne mit einer Vorschrift zu einer Umformung der vorgelegten Herleitung.“ Gentzen, Widerspruchsfreiheit [1936a], 41.
- 24.
Zum Problem der unendlichen Verzweigungen der Reduktionsbäume vgl. auch Bernays' Einführung zu Gentzens 1935er Arbeit Gentzen, Der erste [1974a], 97.
- 25.
Gentzen hat diese Schwierigkeiten in Gentzen, Widerspruchsfreiheit [1936a], 37–41, bei der Diskussion des internen Konditionals ⊃ erläutert. Wenn man \(\mathfrak{A}\supset\mathfrak{B}\) finit so auffaßt, daß damit behauptet wird, es läge ein Beweis B dafür vor, daß aus einem Beweis von \(\mathfrak{A}\) ein Beweis von \(\mathfrak{B}\) erzeugt werden kann, so liegt die Hauptschwierigkeit darin, daß in diesem Beweis B selbst wieder Konditionale enthalten sein können. Diese können so also nicht konstruktiv gerechtfertigt werden.
- 26.
Gentzen, Der erste [1974a], 113.
- 27.
Eine „Verzweigungsfigur“ ergibt sich dadurch, daß beim Reduzieren von Sequenzen gewisse Wahlfreiheiten für Zahlparameter und für Konjunktionsglieder bestehen. Da die Reduziervorschrift für jede mögliche Wahl die weitere Reduktion festlegen muß, ergibt sich an diesen Stellen jeweils eine endliche bzw. unendliche Verzweigung.
- 28.
Gentzen, Der erste [1974a], 97.
- 29.
Das „fan theorem“ besagt in etwa, daß endlich verzweigende Bäume, deren Äste endlich sind, insgesamt endlich sind, d. h. nur endlich viele Knoten haben; m. a. W. gibt es für diese Bäume eine obere Schranke für die Länge ihrer Äste.
- 30.
Vgl. Gentzen, Der erste [1974a], 116.
- 31.
Eine Theorie heißt 1-inkonsistent, wenn sie für eine primitiv-rekursive Formel ϕ(x) sowohl ∃x ¬ϕ(x) impliziert als auch \(\phi(\mathfrak{n})\) für jedes Zahlzeichen \(\mathfrak{n}\). Ist eine Theorie nicht 1-inkonsistent, so heißt sie 1-konsistent. Die ω-Konsistenz wird genauso definiert, nur ohne die Beschränkung, daß ϕ(x) primitiv-rekursiv sein muss. Jede ω-konsistente Theorie ist 1-konsistent und jede 1-konsistente Theorie ist konsistent. Die beiden Umkehrungen gelten jedoch nicht.
- 32.
Zum Instrumentalismus siehe auch im ersten Teil Kap. 8.
- 33.
Jedenfalls hat Bernays 1974 nur die §§ 12–16 des ursprünglichen Beweises als Gentzen, Der erste [1974a] abdrucken lassen, die sich von der 1936 publizierten Fassung Gentzen, Widerspruchsfreiheit [1936a] unterscheiden. Gentzen selbst gibt in Fn. 20 von Gentzen, Widerspruchsfreiheit [1936a], 49, an, bei der Korrektur im Februar 1936 die Nummern 14.1 bis 16.1.1 anstelle der ursprünglichen Fassung eingefügt zu haben.
- 34.
Eine Sequenz in Endform ist eine „offenkundig richtige“ Sequenz: Sie enthält keine Variablen, keine Minimalterme und: die Hinterformel ist eine richtige Minimalformel oder die Hinterformel ist eine falsche Minimalformel und eine der Vorderformeln ist ebenfalls eine falsche Minimalformel.
- 35.
Dies ist also so zu verstehen, daß diejenigen Folgen von Sequenzen, die nach dem alten Herleitungsbegriff Herleitungen waren, auch nach dem neuen Herleitungsbegriff Herleitungen sind. Die Übergänge zwischen den einzelnen Sequenzen sind jedoch nun ggf. Anwendungen anderer Schlußregeln.
- 36.
Das ist jetzt hier im Beweis explizit gesichert, vgl. die Anmerkungen zur früheren Version von 1935.
- 37.
Gentzen hat diese Intuition u. A. mit dem Ausdruck eines „Kompliziertheitsmaßes“, das Vereinfachungen auf unterschiedlichen Ebenen unterschiedlich bewertet, beschrieben; vgl. Gentzen, Neue Fassung [1938b], 36.
- 38.
Die > -Relation zwischen Mantissen m′ und m′′ ist dabei definiert als die Standard > -Relation zwischen den rationalen Zahlen der Gestalt 0, m′ und 0, m′′.
- 39.
Vgl. Ackermann, Widerspruchsfreiheit [1940].
- 40.
Hilbert/Bernays, Grundlagen I [1934]; vgl. auch das Vorwort von Hilbert/Bernays, Grundlagen II [1939]; Kalmárs Beweis wurde als Supplement Va zur zweiten Auflage des ersten Bandes publiziert. – Zur systematischen Relevanz von Kalmárs eigenen Bemühungen im Bereich der Konsistenzbeweise siehe auch Boolos, On Kalmar's [1975].
- 41.
Gentzen, Neue Fassung [1938b].
- 42.
ε 0 ist der Grenzwert der Superexponentiationsfunktion, siehe Fußnote 49.
- 43.
Vgl. Gentzen, Widerspruchsfreiheit [1936a] und Gentzen, Neue Fassung [1938b].
- 44.
Gentzen, Beweisbarkeit [1943].
- 45.
Diese Funktion ω n wird rekursiv definiert durch: ω 0 = 1 und \(\omega _{{n+1}}=\omega^{{\omega _{n}}}\). Diese Definition läßt sich durch einfache Limesbildung auf beliebige Ordinalzahlen erweitern.
- 46.
Vgl. Gentzen, Beweisbarkeit [1943], 160. – Will man eine TI-Herleitung bis zu einer beliebigen Zahl α < ε 0, so wähle man \(\mathfrak{n}\) so groß, daß \(\omega_{\mathfrak{n}}>\alpha\). Zu \(\omega_{\mathfrak{n}}\) hat man dann nach dem gezeigten eine TI-Herleitung, deren Endsequenz \(\mathcal{E}(0)\rightarrow\mathcal{E}(\omega_{\mathfrak{n}})\) lautet. Dann ersetzt man überall in dieser Herleitung ℰ durch ℰ*, wobei ℰ*(ν) : ≡ ∀η(η ≤ ν ⊃ ℰ(η)). Nach gewissen Hinzufügungen an den nun etwas veränderten TI-Obersequenzen erhält man so eine Herleitung von \(\mathcal{E}^{\ast}(0)\rightarrow\mathcal{E}^{\ast}(\omega_{\mathfrak{n}})\). Dann fügt man eine einfache Herleitung von ℰ(0) → ℰ*(0) an und erhält aus beidem durch Schnitt \(\mathcal{E}(0)\rightarrow\mathcal{E}^{\ast}(\omega_{\mathfrak{n}})\). \(\mathcal{E}^{\ast}(\omega_{\mathfrak{n}})\) ist aber nichts anderes als eine Abkürzung für \(\forall\eta(\eta\leq\omega_{\mathfrak{n}}\supset\mathcal{E}(\eta))\), woraus man wegen \(\alpha<\omega_{\mathfrak{n}}\) leicht ℰ(α) gewinnt. Ein abschließender Schnitt liefert dann die gewünschte TI-Untersequenz ℰ(0) → ℰ(α).
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Tapp, C. (2013). Hilbertschule II: Gerhard Gentzen. In: An den Grenzen des Endlichen. Mathematik im Kontext. Springer Spektrum, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29654-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-29654-3_12
Published:
Publisher Name: Springer Spektrum, Berlin, Heidelberg
Print ISBN: 978-3-642-29653-6
Online ISBN: 978-3-642-29654-3
eBook Packages: Life Science and Basic Disciplines (German Language)