Definition eines (relativ vollständigen) formalen Systems konstruktiver Arithmetik

Zusammenfassung Gödels Resultate (1931) [5] — die Unvollständigkeit formaler Systeme, die eine Arithmetik enthalten, und die Unableitbarkeit einer Aussage, die die Widerspruchsfreiheit des betreffenden formalen Systems in arithmetischer Verschlüsselung ausdrückt — reizen wegen der konstruktiven Art ihres Beweises zu der Aufgabe, die konstruktive Mathematik mit der klassischen Mathematik in einen Wettbewerb treten zu lassen, bei dem es darum geht, welche Art des Mathematisierens unter dem unparteiischen Gesichtspunkt der finiten Metamathematik Hilberts [9] zu einem formalistisch feinmaschigeren Netz von Postulaten führt. Gödels Umdeutung einer Arithmetik mit berechenbaren Funktionalen (1958) [7] schafft einen neuen Zugang zu Widerspruchsfreiheitsbeweisen; dort wird in dem früher von Gentzen (1936) [4] behandelten Fall der reinen Zahlentheorie mit primitiv rekursiven Funktionen endlichen Typs über natürlichen Zahlen gearbeitet, dafür aber ohne transfinite Ordinalzahlen und ohne logische Partikeln — von der vollständigen Induktion reicht eine direkte (beim Schritt von n auf n + 1 nicht auf eine Implikation reflektierende) Schlußweise aus, die von Φ(n) = Φ(n + 1) zu Φ(1) = Φ(m) übergeht.