10. Hilbertschule I: Wilhelm Ackermann

Ackermann, Begründung (Publ.) [1925].

Zu den folgenden Ausführungen vgl. auch Tapp/Lück, Transfinite [2004a]; Zach, Hilbert's Finitism [2001].

Zur Person Ackermanns vgl. Hermes, Ackermann [1962]; Hermes, In memoriam [1967]; zu seinem Verhältnis zu Hilbert auch Reid, Hilbert [1970], 173. – In Ackermann, Briefwechsel [1983] veröffentlichte sein Sohn Richard Ackermann einige Briefe, die zwischen seinem Vater und den Logikern Bernays, Scholz, Lorenzen und Schmidt gewechselt worden waren.

Siehe Ackermann, Hilbertscher Aufbau Theoretische Logik [1928]. Erläuterungen zum Zusammenhang mit Hilberts Werk: Bernays, Hilberts Untersuchungen [1935], 205–206.

Hilbert/Ackermann, Theoretische Logik [1928].

So z. B. Ewald/Sieg, Lectures [2013], 28–29.

Vgl. Zach, Hilbert's Finitism [2001], 73.

Hilbert, Tertium non datur [1931a].

Vgl. hierzu auch im ersten Teil Abschn. 5.​4

So wird bspw. in Hilberts Vorlesung vom WS 1917/18 der Kalkül eingeführt unter der Überschrift „Bezeichnungen“; vgl. Hilbert, Wintersemester 17/18 [1918*], 115. – Die Sichtweise scheint die folgende zu sein: Es gibt eine große Menge von Formeln, die als Axiome zulässig wären, d. h., die in einem Beweis benutzt werden können. Dann möge ein konkreter Beweis vorliegen und nur die darin verwendeten Axiome zählen zur in den beweistheoretischen Erwägungen betrachteten Theorie. Auch wenn das letztlich vielleicht keinen Unterschied zum modernen Standpunkt ergibt, könnte die Rede von der (unendlichen) Menge aller Axiome mit Blick auf die Bemühungen um einen finiten Standpunkt absichtlich vermieden worden sein.

Nimmt man die Definition wörtlich, so wären beispielsweise „+ + f(3)“ und „00“ Funktionale. Vgl. Ackermann, Begründung (Publ.) [1925], 2.

Man beachte, daß Ackermann hier möglicherweise bewußt nicht die induktive Formulierung der Termdefinition gewählt hat, um auch hier die Frage der Induktion auf der metamathematischen Ebene zu umgehen. Die folgende Definition der Formeln hat jedoch das induktive Gepräge „sind …Formeln, so auch …“.

Hilbert, Die logischen Grundlagen [1923]; vgl. auch Abschn. 9.​6.​2

Eigentlich ist es nicht ganz korrekt, die neuen Zeichen als Grundzeichen zu bezeichnen, da die in diesen Ausdrücken auftretenden Zeichen auch wirklich in einem enthaltenden Term auftreten (z. B. tritt in einem Term t(ε a. A(a)) die Aussagevariable A auf). Dies wäre bei einer ganz exakten formalen Rekonstruktion etwa im Zusammenhang der Definition der freien Variablen zu beachten.

So etwa Gentzen, Widerspruchsfreiheit [1936a], 9; Hermes, Ackermann [1962]; Reid, Hilbert [1970], 189.

Vgl. Hilbert/Bernays, Grundlagen II [1939], VI.

Vgl. die Schilderung der axiomatischen Methode als eines schrittweisen Tieferlegens der Fundamente einer Wissenschaft in Hilbert, Axiomatisches Denken [1918], 407, sowie Hilberts Vorgehen, Widerspruchsfreiheitsbeweise bei einfachen Systemen anzusetzen und auf umfassendere Systeme auszuweiten (Kap. 9).

Ackermann erwähnt dazu, daß in den Rekursionsaxiomen (ϕ ⁱ 1) und (ϕ ⁱ 2) auch in der ε-Sprache ℒ ₁ ⁰ nur ℒ ₀ ⁰ -Funktionale \(\mathfrak{a}\) und \(\mathfrak{b}\) zugelassen sind. Die aus ε-Terme enthaltenden Funktionalen rekursiv definierbaren Funktionen lassen sich auch so erhalten, daß zunächst die Rekursionsgleichung mit einer Funktionsvariable angesetzt wird und für diese anschließend mittels [Subst] der gewünschte ε-Term eingesetzt wird.

Es ist wichtig zu sehen, daß hier ein ganz anderer „Richtigkeits“-Begriff im Spiel ist, als 1917/18 in Hilberts Umfeld üblich. Sowohl Hilberts Vorlesung im Wintersemester 1917/18, als auch Bernays' Göttinger Habilitationsschrift vom Frühjahr 1918 verwenden „Richtigkeit“ nahezu synonym mit „Beweisbarkeit“, also genau nicht für die semantische Seite (wie Ackermann), sondern für die syntaktische. Ackermanns Begriff von „Richtigkeit“ hat wesentlich mehr Ähnlichkeit mit Hilberts Begriff der „Einsetzungsrichtigkeit“ in der Kneser-Mitschrift der Vorlesung WS 1921/22, vgl. Abschn. 9.​6.​1.​1.

Strenggenommen ist das Produkt dieser Umformung kein Beweis mehr, sondern höchstens ein beweisähnliches Gebilde, das strukturell isomorph zum ursprünglichen Beweis ist; vgl. auch den ursprünglichen Fehler in Hilbert, Wintersemester 21/22 (Bernays) [1922a*]. Beispielsweise sind nach der „Herausschaffung“ der Variablen, also ihrer Ersetzung durch Zahlzeichen, die Spitzen eines Beweisbaumes nicht mehr unbedingt Axiome. Stand z. B. das Axiom (13.) a = a an einer Spitze des Beweisbaumes, so steht dort nach der Umformung \(\mathfrak{z}=\mathfrak{z}\) für ein Zahlzeichen \(\mathfrak{z}\) und diese Gleichung ist kein Axiom. Außerdem hat Ackermann keine Strukturschlüsse und das kann dazu führen, daß eine Instanz des Substitutionsschemas nach der Transformation trivialisiert ist (z. B. \(\frac{a=a}{\mathfrak{z}=\mathfrak{z}}\) zu \(\frac{\mathfrak{z}=\mathfrak{z}}{\mathfrak{z}=\mathfrak{z}}\)), solche trivialen Schlüsse aber strenggenommen nicht in Ackermanns Formalismus vorkommen. Bei den transformierten Bäumen handelt es sich i. A. also nicht um Beweise im Sinne des Kalküls.

Zu einer ausführlicheren Diskussion der Frage, inwiefern in Hilberts und Ackermanns Arbeiten „transfinite Schlußweisen“ auf der Metaebene vermieden werden sollen oder können, vgl. auch Tapp/Lück, Transfinite [2004a].

Strenggenommen muß man in den folgenden Überlegungen immer von Gleichungen und Ungleichungen reden. Da beide Fälle jedoch hier genau symmetrisch sind, wird im Folgenden kurzerhand nur von Gleichungen gesprochen.

Der Ausdruck „Funktionszeichen“ klingt doppeldeutig: Es könnte damit ein Überbegriff für Namen für individuelle Funktionen und die Funktionsvariablen gemeint sein, oder nur die Namen für individuelle Funktionen. Der Ausdruck „Funktionszeichen“ wird in dieser Arbeit durchgängig in der letztgenannten Weise gebraucht, d. h. synonym mit den umständlichen Ausdrücken „Individuenkonstante für Funktionen“, „Namen für individuelle Funktionen“ o. ä., und damit ganz analog zum Ausdruck „Zahlzeichen“.

Stillschweigend wird hier immer „reduzieren“ nicht bloß als „ersetzen“ verstanden, sondern als „so ersetzen, daß Rekursionsaxiome richtig werden“.

Beispielsweise tritt in „2 ⋅ 3“ nur ein Funktionszeichen auf. Rechnet man diesen Term gemäß der Rekursionsgleichungen für  ⋅  aus, so erhält man „2 + 2 + 2“, also einen Term, in dem trotz einiger Schritte des Ausrechnens nun mehr Funktionszeichen auftreten. – Die Anzahl der Funktionszeichen, die durch einen Rekursionsschritt entstehen, ist bei ℒ ₀ ⁰ allerdings noch ausschließlich durch die Definitionsklauseln der Funktionen bestimmt. Bei höheren Theorien werden später Fälle auftreten, wo diese Anzahl auch durch die Argumente der Funktion mitbestimmt sein kann.

So Zach, Hilbert's Finitism [2001], 77. Das System der zweitstufigen primitiv-rekursiven Arithmetik ohne Induktion (2 PRA ⁻) besteht neben der Logik und den Gleichheitsaxiomen aus Axiomen für die Nachfolger- (+1) und die Vorgängerfunktion (δ) und aus definierenden Gleichungen für erst- und zweitstufige primitiv-rekursive Funktionen, es enthält jedoch keine Induktionsregel. Zu Ackermanns eigenen Angaben vgl. oben Abschn. 10.2.

Man betrachte z. B. die Funktion ϕ(x, f), die rekursiv definiert ist durch: mit einer freien Funktionsvariable f. Ein Term ϕ(2, f) wird dann im ersten Schritt ausgerechnet zu ϕ(1, f) + f(3), im zweiten Schritt zu ϕ(0, f) + f(2) + f(3) und im dritten schließlich zu f(0) + f(2) + f(3). Das Problem ist, daß nun beliebige Substitutionen für den Parameter f gestattet sind, die etwa auch das Zeichen ϕ enthalten können. Für f(x) könnte also ϕ ⋅ ϕ(x, ψ) mit einer individuellen Funktion ψ eingesetzt werden. Dann wäre das Rekursionsergebnis bis hierher schon ϕ ⋅ ϕ(0, ψ) + ϕ ⋅ ϕ(2, ψ) + ϕ ⋅ ϕ(3, ψ), es würde also viel mehr Vorkommnisse von ϕ enthalten und noch dazu mit einem höheren Argument als der ursprüngliche Term ϕ(2,λ y. (ϕ ⋅ ϕ(y, ψ))). Dennoch ist die Komplexität des Gesamtausdrucks durch das Ausrechnen kleiner geworden, denn nun tritt in dem Funktionsargument von ϕ nicht mehr der Term auf, der selbst wieder ϕ enthielt. Dieser Anschauung von einer Komplexitätsverringerung trotz Erhöhung von Zeichenanzahl und maximalem Argumentwert trägt die besprochene Indexordnung Rechnung.

Ackermann, Begründung (Publ.) [1925], 16–18.

Zach schlägt in Zach, Hilbert's Finitism [2001] eine Korrektur der Ackermannschen Definition von „Unterordnung“ vor. Sie besteht darin, daß Unterordnung von ξ unter ϕ durch eine gebundene Variable b nicht nur dann vorliegt, wenn diese Variable durch ϕ gebunden wird, sondern auch dann, wenn ϕ im Bindungsbereich (scope) von b auftritt. Die Notwendigkeit dieser Korrektur ist aus zwei Gründen nicht nachvollziehbar. Erstens illustriert Zach die korrigierte Definition durch das Beispielfunktional \(\mathfrak{t}^{\prime}(\dots\phi_b(\dots\xi(\dots b\dots)\dots)\dots)\) (S. 21), obwohl in diesem Beispiel genau wie bei Ackermann das b von ϕ gebunden wird. Zweitens bleibt unklar, was diese Korrektur bewirken soll. Zach hält sie für nötig an der Stelle im Reduktionsbeweis, wo bei einem Funktional \(\mathfrak{t}\) der innerste konstante Teilterm die Form \(\mathfrak{s}=\phi_b(\mathfrak{z},\mathfrak{c}(b))\) hat, und zwar um in diesem Fall auf die Unterordnung aller Funktionszeichen(auftreten) in \(\mathfrak{c}(b)\) unter dieses ϕ _b zu schließen (S. 22). Dies tut aber auch Ackermanns eigene Definition: Denn gäbe es in \(\mathfrak{s}\) Variablen, die (wie in Zachs Fn. 35 angedeutet) durch weiter außen als ϕ _b in \(\mathfrak{t}\) stehende Funktionszeichenauftreten gebunden würden, so wäre \(\mathfrak{s}\) ja gar kein innerster konstanter Teilterm von \(\mathfrak{t}\) gewesen. Summa summarum ist nicht nachvollziehbar, warum diese Korrektur des Ackermannschen Unterordnungsbegriffs nötig ist. Sie verändert u. U. deutlich die Zahl der als untergeordnet geltenden Funktionszeichen, was möglicherweise im weiteren Verlauf des Beweises für Komplikationen sorgen könnte. (Die vorstehenden Überlegungen gehen davon aus, daß das „See note 4.“ in Fn. 35 bei Zach eigentlich „See note 34.“ heißen müßte und Fn. 34 und 35 sich auf dieses Problem beziehen.)

Vgl. Zach, Hilbert's Finitism [2001], 79.

Mit „den ϕ-Rang \(\mathfrak{n}\) haben“ ist natürlich dasselbe gemeint wie mit „vom Rang \(\mathfrak{n}\) bzgl. ϕ sein“.

Diese Definition hat Zach, Hilbert's Finitism [2001] genauso.

Vgl. Ackermann, Begründung (Publ.) [1925], 15.

Auch hier ist darauf hinzuweisen, daß Ackermanns Fassung dieses Gedankens von der heute gängigen Weise abweicht. Er betrachtet hier keine ganze Folge von Rängen bezüglich aller rekursiven Funktionen, sondern er stellt sich den gegebenen Beweis vor, zählt die darin gegebenen n rekursiven Funktionen mit 1, …, n ab und kann dann mit einem n-Tupel auskommen. (Eigentlich macht er es sogar noch sparsamer, nämlich so, daß Nullen (also Ränge von gar nicht in \(\mathfrak{t}\) auftretenden Funktionszeichen) erst beim Vergleich zweier Rangkombinationen eingefügt werden, und nicht schon in der Definition der Rangkombinationen vorkommen. Auf diese Sparsamkeit wird hier zugunsten der Übersichtlichkeit verzichtet.)

Die Konzentration auf das Finden der richtigen Ersetzungen für die einen ε-Terme scheint gelegentlich dazu zu führen, daß keine Ersetzungen für ε-Terme, deren kritische Axiome nicht vorkommen, angegeben werden.

Bernays, Hilberts Untersuchungen [1935].

Vgl. Hilbert/Bernays, Grundlagen II [1939], VI.

von Neumann, Zur Hilbertschen [1927]. – Über Leben und Werk von Neumanns (1903–1957) informieren Legendi/Szentivanyi, von Neumann [1983], und besonders Ádám, von Neumann [1983].

Vgl. Ackermann, Begründung (Publ.) [1925], 10.

Vgl. Ackermann, Begründung (Publ.) [1925], 21.

Vgl. Ackermann, Begründung (Publ.) [1925], 16–17,19–20.

Vgl. von Neumann, Zur Hilbertschen [1927], 43.

Ackermann hat die Notwendigkeit, die Substitutionsregel einzuschränken, anscheinend selbst als erster bemerkt. Dies zeigt eine entsprechende Anmerkung, die er seiner Arbeit noch während der Drucklegung zugefügt hat; vgl. Ackermann, Begründung (Publ.) [1925], 9.

Bernays, Hilberts Untersuchungen [1935], 210.

Vgl. hierzu Moser, The Epsilon [2000], 14; Zach, Hilbert's Finitism [2001], 31; Hilbert, Grundlagen Mathematik [1928], 19; Hilbert, Probleme Grundlegung [1929], 6.

Vgl. Zach, Hilbert's Finitism [2001].