A formalization of recursive arithmetic. (Q2579576)

Verf. gibt eine neue Formalisierung der rekursiven Arithmetik. Diese Theorie ist in Hilbert-Bernays ``Grundlagen der Mathematik'', Bd. 1 (1934; JFM 60.0017.*) auf den elementaren logischen Kalkül mit freien Variablen gegründet mit Hinzufügung der Gleichheitsbeziehung, der Nachfolgerfunktion \(n +1\), der primitivrekursiven Definitionen und des Induktionsschemas. Die Formalisierung des Verf. unterscheidet sich von der von Hilbert-Bernays besonders darin, daß sie nicht auf einen anderen logischen Kalkül gegründet ist, sondern ein selbstständiges logisches System darstellt. Nach einer Erklärung der primitiven Begriffe, der Axiome und der Schlußregeln beweist Verf. einige grundlegende Sätze seines Systems und entwickelt die Eigenschaften der elementaren arithmetischen Funktionen. Danach zeigt er, daß der klassische Aussagenkalkül in seinem System enthalten ist, und daß die von Hilbert-Bernays gegebene Formalisierung mit der des Verf. gleichwertig ist. Diese soll für gewisse metamathematische Untersuchungen besonders geeignet sein.