Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I. (Q571218)

Diese bedeutungsvolle Arbeit leitet Tatsachen her, die für axiomatisierte mathematische Systeme und speziell für den metamathematischen Standpunkt grundlegend sind. Ausgangspunkt ist im wesentlichen das formale System, das man erhält, indem man die \textit{Peano}schen Axiome mit der Logik der ``Principia Mathematica'' überbaut (natürtürliche Zahlen als Individuen) und eventuell eine rekursiv definierbare Klasse von Axiomen hinzufügt, vorausgesetzt, daß dabei eine gewisse Widerspruchsfreiheitsbedingung erfüllt bleibt. In diesen noch etwas erweiterbaren Bereich fallen nicht bloß die ``Principia Mathematica'' (einschließlich des Auswahlaxioms für alle Typen) und die \textit{Peano}sche Arithmetik samt einem bestimmten Schema der rekursiven Definition, sondern z. B. auch die von \textit{Ackermann} und \textit{von Neumann} herrührenden Axiomensysteme der Analysis und die axiomatisierte Mengenlehre nach \textit{Zermelo-Fraenkel} oder nach \textit{von Neumann}. Das Hauptergebnis ist, daß es in jedem solchen System unentscheidbare Sätze gibt, und zwar sogar unentscheidbare arithmetische Sätze, wobei ``arithmetisch'' die Beschränkung auf Addition und Multiplikation natürlicher Zahlen sowie die logischen Konstanten ``oder'', ``nicht'', ``alle'', ``identisch'' (die beiden letzteren auf natürliche Zahlen bezogen) ausdrückt. Ebenso gibt es unentscheidbare Probleme des ``engeren Funktionenkalküls'' (im Sinne der theoretischen Logik von \textit{Hilbert-Ackermann}). Ersetzt man die vorausgesetzte engere Widerspruchsfreiheit durch Widerspruchsfreiheit schlechthin, so tritt an die Stelle eines unentscheidbaren Satzes eine Eigenschaft, für die weder ein Gegenbeispiel angebbar noch die durchgängige Erfülltheit beweisbar ist. Der Beweis beruht in der Hauptsache auf einer Numerierung der Formelzeichen des formalen Systems, wodurch eine Formel in eine endliche Folge natürlicher Zahlen, eine Beweisfigur in eine endliche Folge solcher Folgen übergeht. Damit werden die metamathematischen Begriffe bzw. Sätze zu Begriffen bzw. Sätzen über Folgen natürlicher Zahlen und daher in den Symbolen des formalen Systems ausdrückbar; das gilt z. B. auch für den Satz: ``\(v\) ist eine beweisbare Formel''. Von hier aus gelingt die Herstellung eines unentscheidbaren Satzes auf eine Art, die der \textit{Richard}schen Antinomie analog ist. Der auf solche Art erhaltene Satz, der seine eigene Unbeweisbarkeit behauptet (und daher metamathematisch richtig ist, nicht aber im System), hat aber in diesem Fall nichts Zirkelhaftes an sich. Aus dem Hauptergebnis folgt weiter die Unmöglichkeit, die \textit{Widerspruchsfreiheit} eines solchen formalen Systems (metamathematisch) zu beweisen mit Hilfe von Schlußweisen, die in dem System formalisiert sind (um so mehr mit den, wie üblich, weiter eingeschränkten Schlußweisen). Wenn es also nach \textit{Hilbert} finite Widerspruchsfreiheitsbeweise geben sollte, so müßten sie in dem betreffenden System sich nicht darstellen lassen.