Grundlagen der Mathematik. I. (Q2616493)

Das vorliegende Werk stellt die erste zusammenhängende, von Grund an aufbauende Veröffentlichung über die \textit{Hilbert}sche Beweistheorie dar. Damit ist zum ersten Male eine genaue Unterlage für alle Diskussionen über diese Theorie gegeben; denn auf Grund der bisher vorliegenden Einzelveröffentlichungen von \textit{Hilbert, Bernays} und anderen Mitarbeitern sich ein Bild von dem gesamten Aufbau zu machen, war für den Fernerstehenden sicher nicht leicht, so daß Mißverändnisse vorgekommen sind. Hinzu kommt, daß sich der formale Aufbau der Theorie im einzelnen seit \textit{Hilbert}s erster Veröffentlichung über diesen Gegenstand (``Über die Grundlagen der Logik und der Arithmetik''; Verhandlungen des 3. internationalen Mathematikerkongresses in Heidelberg, 1904; F. d. M. 36, 84 (JFM 36.0084.*)) dauern verändert hat. Hier liegt nun die definitive Fassung vor. Das Werk ist in eine Reihe zu stellen mit den großen Veröffentlichungen von \textit{Frege, Peano} und \textit{Russel-Whitehead}; es enthält, wie diese, einen streng formalen Aufbau der Logik und der Mathematik, dessen Eigenart hier darin besteht, daß die Mathematik nicht auf die Logik zurückgeführt wird, sondern der Aufbau beider Disziplinen gleichzeitig erfolgt. Dazu kommt der ganz neue Gesichtspunkt \textit{Hilbert}s, den Aufbau nicht nur mittels plausibel erscheinender Denkgesetze zu begründen, sondern die Widerspruchsfreiheit des eingeführten Formalismus zu zeigen. Der vorliegende Band enthält die Grundlagen; ein zweiter Band, von wessentlich geringere Umfange, der in Kürze erscheinen soll, wird die Theorie bis zu ihrem heutigem Ergebnisstande weiterführen. \flushpar Was den Inhalt und die Gliederung der Darstellung im einzelnen anbetrifft, so beginnt der sustematische Aufbau erst mit dem 3. Kapitel. Die beiden ersten Kapitel dienen der Einführung in die Problemstellung. Der Begriff einer streng formalen Axiomatik wird eingeführt, und es wird dargelegt, daß zu ihrer Ergänzung ein Widerspruchsfreiheitsbeweis gehört, der in einfachem Fällen, wenn es sich nämlich um endliche Bereiche handelt, durch die Methode der Aufweisung sich oft leicht führen läßt, der aber auf Schwierigkeiten stößt, sobald unendliche Bereiche in Frage kommen. Der Versuch, die Widerspruchsfreiheit in diesem Falle ebenfals durch die Methode der Aufweisung, und zwar an einem zahlenteoretischen Modell, zu zeigen, führt sofort auf die Frage nach der Widerspruchsfreiheit der Arithmetik. Die Notwendigkeit, einen Widerspruchsfreiheitsbeweis für die Arithmetik unter Ausschluß von axiomatisch-existentialen Annahmen zu führen, legt den Gedanken nahe, zu versuchen, die ganze Arithmetik ohne derartige Annahmen zu begründen, um jeden Widerspruchsfreiheitsbeweis entbehrlich zu machen. Dieser Versuch wird im 2. Kapitel gemacht; es wird eine finite Zahlentheorie aufgebaut etwa im Sinne \textit{Brouwer}s, zugleich aber auch auf die wesentlich Einbuße an Systematik und Beweistechnik hingewiesen, die die Mathematik dadurch erfahren würde. Das führt zur klaren Umreißung der \textit{Hilbert}schen Problemstellung: Aufbau einer rein formalen Mathematik, in der auch die axiomatisch-existentialen Schlußweisen in voller Schärfe ihren Platz finden, dann aber einer übergeordneten Beweistheorie oder Metamathematik, die die Tragfähigkeit und Widerspruchsfreiheit der formalen Schlußweisen durch inhaltlich-finite Überlegungen untersucht. \flushpar Kapitel 3 bis 5 bringen dann den Aufbau der formalen Logik, des Aussagenkalküls und des Prädikatenkalküls der ersten Stufe mit Einbeziehung der Gleichheitsrelation. Der Aussagenkalkül wird nicht axiomatisch, sondern als Theorie der Wahrheitsfunktionen entwickelt. Dagegen wird beim Prädikatenkalkül die mengentheoretische Behandlung, die das Analogon zur Theorie der Wahrheitsfunktionen darstellen würde und sonst beim Aufbau der Logik häufig benutzt wird, in Wahrung der \textit{Hilbert}schen Grundeinstellung vermieden; vielmehr wird dieser Kalkül als deduktives System entwickelt, dessen Widerspruchsfreiheit hier noch in trivialer Weise zu erkennen ist, da noch keine Bedingungen hinzukommen, die eine Endlichkeit des zugrunde gelegten Individuenbereichs ausschließen. Es sei bemerkt, daß die Darstellung breiter ist als zum Gesamtaufbau des Buchs erforderlich wäre. Tatsächlich enthalten die drei Kapitel einen gedrängten Lehrgang der theoretischen Logik, den \textit{P. Bernays} noch durch zahlreiche interessante Einzelheiten -- ich weise nur hin auf die ``positive Logik'', die Unabhängigkeitsbeweise, die Behandlung der \(k\)-zahlig identischen Formeln, das ausführliche Eingehen auf das Entscheidungsproblem -- bereichert hat. Kap. 6 enthält die ersten Widerspruchsfreiheitsbeweise für unendlilche Bereiche. Bei diesen Beweisen wird nicht gleich auf die Widerspruchsfreiheit des gesamten Formalismus zugesteuert, sondern dieser Formalismus wird stufenweise aufgebaut, als widerspruchsfrei nachgewiesen und wieder erweitert, sobald sich zeigt, daß er noch nicht alle Schlußweisen auszudrücken gestattet. So wird hier für ein einfaches Axiomensystem der Arithmetik, das aber schon die \textit{Dedekind}sche Definition des unendlichen Bereiches enthält, die Widerspruchsfreiheit zunächst unter Ausschluß von gebundenen Variablen, dann Hinzuziehung von All- und Seinszeichen und schließlich des Axioms der vollständigen Induktion gezeigt. Beim Beweise der Widerspruchsfreiheit wird die aus früheren Veröffentlichungen bekannte Methode der Auflösung der Beweisfigur in Beweisfäden und anschließender Umformung jeder Formel in eine verifizierbare benutzt. Neu ist, daß auch die All- und Seinszeichen durch diese Methode mit erfaßt werden. Das war auf Grund neuerer Arbeiten von \textit{Preßburger} und \textit{Herbrand} möglich. Der Kalkül mit den All- und Seinszeichen wird direkt eingeführt und stützt sich nicht mehr auf das bekannte \textit{Hillbert}sche \(\varepsilon \)-Axiom, das in der früheren Form überhaupt verschwunden ist. Kapitel 7 bringt dann die rekursiven Definitionen, deren Einführung sich zwecks Aufbau der einfachsten zahlentheoretischen Funktionen als notwendig erweist. Der Widerspruchsfreiheitsbeweis gelingt aber, nach ähnlichen Methoden wie vorher, zunächst nur unter Ausschaltung der gebundenen Variablen, also bei wesentlicher Einschränkung des Formalismus. Ein das Induktionsaxiom ersetzendes Induktionsschema kann allerdings noch zugelassen werden. Im übrigen bringt dieses Kapitel, ganz unabhängig von dem Zweck des gesamten Werks, auch für den rein mathematisch Interessierten viel Wissenswertes. Es enthält eine ganze Theorie der Rekursionen, wobei sich der Begriff der ``primitiven Rekursion'' und der ``simultanen'' Rekursion als besonders fruchtbar erweist. Interessant ist auch, zu sehen, wie alle einfachen zahlentheoretischen Begriffe sich auf Rekursionen zurückführen lassen; z. B. wird die Rekursionsfunktion angegeben, die die Reihe der Primzahlen liefert. Im 8. Kapitel findet der Formalismus seinen vorläufigen Abschluß. Es wird nach dem Vorbild \textit{Russel}s eine Prädikatenfunktion eingeführt, die den Begriff ``derjenige, welcher'' auszudrücken gestattet und die an Stelle des früheren \textit{Hilbert}schen \(\varepsilon \) tritt. Es ergibt sich nun die überraschende Tatsache, daß nach Einführung dieser Funktion mit Ausnahme im wesentlichen der Addition und Multiplikation alle weiteren Rekursionsfunktionen entbehrlich werden, da sie sich durch explizite Definitionen ausdrücken lassen. Ferner wird gezeigt, daß bei Hinzunahme des ``derjenige, welcher'' zu einem an sich widerspruchsfreien Axiomensystem die Widerspruchsfreiheit erhalten bleibt. Danach ist es aber, um den ganzen Formalismus ohne Einschränkung als einwandfrei nachzuweisen, ausreichend, wenn die Widerspruchsfreiheit für ein System gezeigt wird, das aus dem im 6, Kapitel behandelten dadurch entsteht, daß die rekursive Definition der Addition und der Multiplikation hinzugenommen wird. Dieser Nachweis selbst findet in dem vorliegenden 1. Band nicht mehr seinen Platz, es wird dafür auf den kommenden 2. Band verwiesen.