Zur Widerspruchsfreiheit der Zahlentheorie. (Q2585745)

Nach dem Vorgang von \textit{Gentzen} (Math. Ann., Berlin, 112 (1936), 493-565; F.~d.~M. 62\(_{\text{I}}\), 44) gibt Verf. einen neuen Widerspruchsfreiheitsbeweis für die Zahlentheorie. Der Kalkül verwendet freie und gebundene Zahlvariable, den Term 0, die Funktionszeichen \(\delta\), \('\), \(+\), \(\cdot\), die logischen Konstanten \(=\), \(-\), \(\to\) und das Hilbertsche \(\varepsilon\)-Symbol. Simultan werden die Begriffe \textit{Term} (speziell \(\varepsilon\)-Term: \(\varepsilon_x\) \(\mathfrak{A}(x)\)) und \textit{Formel} eingeführt. Beweisbar sind alle Formeln (ohne freie Variablen), die aus 20 (darunter vier kritischen, das \(\varepsilon\)-Symbol enthaltenden) Axiomen mit Hilfe des Schlußschemas erhalten werden können. Die Beweisidee entstammt früheren Untersuchungen des Verf. (dargestellt z. B. in \textit{Hilbert-Bernays}, Grundlagen der Mathematik II (1939); F.~d.~M. 65, 21). Eine \textit{Gesamtersetzung} (G. E.) ersetzt in einem Beweis alle \(\varepsilon\)-Terme durch ihre Grundtypen (die aus ihnen durch Ersetzung aller maximalen echten Termbestandteile durch verschiedene freie Variablen entstehen) und ordnet diesen rekursive Funktionen mit entsprechender Argumentzahl (argumentfreien ein Zahlzeichen \(0' \cdots ')\) zu. Eine G. E. führt unter Beibehaltung des Beweischarakters alle das \(\varepsilon\)-Symbol enthaltenden Formeln in \(\varepsilon\)-freie über, die sich in finiter Weise als falsch oder richtig erweisen. Gelingt es, ausgehend von einer normierten G. E. durch sukzessive Verbesserungen (festgelegter Art) eine solche G. E. zu finden, die alle im Beweis vorkommenden kritischen Axiome in richtige Formeln überführt, so ist die Endformel richtig, also von \(0 \neq 0\) verschieden. Mit Hilfe von transfiniter Induktion wird bewiesen, daß das Verbesserungsverfahren in endlich vielen Schritten zum Ziele führt. In der zweiten Hälfte der Arbeit gibt Verf. -- und dies ist ein Fortschritt gegenüber Gentzen -- eine explizite Schranke für die Anzahl der soeben genannten Verbesserungen der G. E. bei vorgegebenem Beweis. Diese hängt ab von der Zahl der Grundtypen, dem maximalen Grad der Terme (Grad eines Terms \(=\) Anzahl der Funktionszeichen, mit deren Hilfe er aus \(\varepsilon\)-Termen und aus dem Term 0 aufgebaut ist) und der Anzahl der \(\varepsilon\)-Terme im Beweis. Die Abhängigkeitsfunktion ist insofern rekursiv, als sich der Wert für ein vorgegebenes Argumentsystem in endlich vielen Schritten berechnen läßt. Es handelt sich dabei (wegen der Gödelschen Ergebnisse) nicht um gewöhnliche Rekursionen, sondern urn solche höherer Stufe. Unter einer zahlentheoretischen rekursiven Funktion \(n\)-ter Stufe versteht Verf. dabei eine Funktion, deren Berechnung für ein gegebenes Argument \(a\) sich auf ihre Berechnung für endlich viele Argumente \(a_i\) reduziert, so daß \(a_i \underset{n} {<} a\), wobei \(\underset{n} {<}\) eine (von \(n\) abhängige) Ordnung der Menge der natürlichen Zahlen nach einem Ordnungstyp der zweiten Zahlklasse darstellt (\(\underset{0} {<}\) ist die gewöhnliche Ordnung).