The consistency of arithmetics (Q5923139)

Bisher lagen mit finiten Mitteln geführte Widerspruchsfreiheitsbeweise nur für solche Teilgebiete der Zahlentheorie vor, die das Axiom der vollständigen Induktion nicht umfassen. Die Widerspruchsfreiheit der vollständigen Zahlentheorie konnte zwar, nach einem zuerst von \textit{Gödel} ausgesprochenen Gedanken, aus der Widerspruchsfreiheit der intuitionistischen Arithmetik hergeleitet werden; jedoch konnte diese Lösung vom finiten Standpunkt aus nicht als befriedigend angesehen werden, da von diesem Standpunkt gegen die intuitionistische Verwendung des Implikationszeichens Bedenken erhoben werden müssen. Der Verf. beweist nun zum erstenmal die Widerspruchsfreiheit der Schlußweisen der vollständigen reinen Zahlentheorie mit finiten Mitteln. Die reine Zahlentheorie ist dabei (in der Darstellungsweise von \textit{Hilbert} und \textit{Bernays} ausgesprochen) als durch einen Kalkül gegeben gedacht, der den elementaren Prädikatenkalkül einschließlich der Identitätsaxiome, die formalisierten \textit{Peano}-Axiome und rekursive Definitionen umfaßt. Ein solcher Formalismus kann sich allerdings den praktischen Bedürfnissen der Forschung gegenüber einmal als zu eng erweisen und ist außerdem nach bekannten metamathematischen Sätzen notwendig unvollständig. Es ist daher wichtig, daß der Widerspruchsfreiheitsbeweis des Verf. so angelegt ist, daß er auch bei Erweiterungen des Formalismus anwendbar bleibt. Nach einem Satz von \textit{Gödel} ist der Widerspruchsfreiheitsbeweis für die reine Zahlentheorie nur möglich, wenn eine Schlußweise verwendet wird, die in dem Formalismus der reinen Zahlentheorie nicht dargestellt werden kann. Als eine solche Schlußweise verwendet der Verf. in seinem Beweis einen transfiniten Induktionsschluß im Bereich der Ordinalzahlen bis zur ersten \textit{Cantor}schen \(\varepsilon\)-Zahl. Nach einer Bemerkung von \textit{Bernays} kann diese transfinite Induktion in einem Widerspruchsfreiheitsbeweis der reinen Zahlentheorie nicht durch eine schwächere Schlußweise ersetzt werden. Der Verf. schickt seinem Widerspruchsfreiheitsbeweis Abschnitte über Sinn und Möglichkeit von Widerspruchsfreiheitsbeweisen, über die Formalisierung der reinen Zahlentheorie und über bedenkliche und unbedenkliche Schlußweisen in der reinen Zahlentheorie voraus, in denen er eine ausführliche Darstellung des \textit{Hilbert}schen Programms gibt. Von diesen Ausführungen ist vor allem die in dem dritten Abschnitt gegebene Charakterisierung der finiten Schlußweisen wichtig, da bei den bisherigen eingehenderen Kennzeichnungen des finiten Standpunktes gewöhnlich die ``finitkombinatorischen'' Schlußweisen in den Vordergrund gestellt wurden, die bekanntlich für den Beweis der Widerspruchsfreiheit der Zahlentheorie nicht ausreichen. Der Widerspruchsfreiheitsbeweis wird nun so geführt, daß für die beweisbaren Formehl der Zahlentheorie ein Begriff der inhaltlichen Richtigkeit dadurch eingeführt wird, daß für die Herleitungen dieser Formeln ein Reduktionsverfahren definiert wird. Durch dieses Reduktionsverfahren wird die Frage der inhaltlichen Richtigkeit einer Herleitung, und damit der Endformel dieser Herleitung, auf die Frage nach der Richtigkeit einfacherer Herleitungen, und zwar (dies ist für das angewendete Verfahren kennzeichnend) im allgemeinen nach der Richtigkeit von Herleitungen aus einer abzählbar unendlichen Mannigfaltigkeit einfacherer Herleitungen, zurückverlegt. Um nun zu zeigen, daß dieses Reduktionsverfahren stets nach endlich vielen Schritten auf die einfachsten Herleitungen führt, die nur aus einer Formel bestehen, von deren Richtigkeit man sich durch elementares Ausrechnen überzeugen kann, ordnet der Verf. den Herleitungen endliche Dezimalbrüche zu, die eine wohlgeordnete Menge vom Ordnungstypus der ersten \(\varepsilon\)-Zahl bilden. Die Endlichkeit des Reduktionsverfahrens wird dann mit Hilfe des transfiniten Induktionsschlusses im Bereich dieser Dezimalbrüche erschlossen. Der transfinite Induktionsschluß wird finit-konstruktiv interpretiert.