The inconsistency of certain formal logics. (Q2611355)

Der Inhalt dieses kleinen Aufsatzes ist von größter Wichtigkeit für die Beurteilung der Versuche, eine Logik ohne Typentheorie aufzubauen. Die Verf. beweisen, daß derartige logische Systeme zu einem Widerspruch führen müssen, falls sie eine gewisse Freiheit in der Ausdrückbarkeit von Formeln als Werten von Funktionen gestatten. Genauer gesprochen handelt es sich in der Hauptsache um die Ausdrückbarkeit von zahlentheoretischen Funktionen, die die Gesamtheit der Formeln des Systems abzählen, und so eine \textit{Gödel}sche Repräsentation der Logik in sich selbst gestatten. Es zeigt sich nun, daß diejenigen typenlosen logischen Systeme, von denen bisher eine vollständige Formalisierung veröffentlicht worden ist, nämlich die kombinatorischen Systeme von \textit{Curry} (\textit{H. B. Curry}, Grundlagen der kombinatorischen Logik, Amer. Journ. of Math. 52 (1930), 509-536, 789-834; JFM 56.0048.*) und \textit{Rosser} (vgl. die beiden vorstehend besprochenen Arbeiten), sowie die Logik von \textit{Church} (\textit{A. Church}, A set of postulates for the foundation of logic. I, II, Ann. of Math. (2) 33 (1932), 346-366; (2) 34 (1933), 839-864; F. d. M. 58; 59\(_{\text{I}}\), 52 fortgesetzt in verschiedenen Arbeiten von \textit{Kleene} und \textit{Rosser}) gerade die verhängnisvolle Eigenschaft besitzen. Man wird nach dem Ergebnis dieser Arbeit weiteren Versuchen, eine typenlose Logik aufzubauen, sehr skeptisch gegenüberstehen. Die Paradoxien, die man freilich in den historischen Formen (z. B. der \textit{Russell}schen Form) vermeiden kann, scheinen sich in anderer Weise wieder einzuschleichen. Bemerkenswert ist, daß die von den Verf. aufgezeigten Widersprüche gerade mit der Ausdrückbarkeit gewisser zahlentheoretischer Funktionen zusammenhängen. Bildet doch die Möglichkeit, aus der typenlosen Logik die Zahlentheorie zu gewinnen, einen Hauptanreiz für den Aufbau eines solchen Systems. Beschränkt man andererseits das logische Operieren so, daß sich der Widerspruchsfreiheitsbeweis führen läßt, wie es \textit{Church} in seinem neusten System getan hat (\textit{A. Church}, A proof of freedom from contradiction, Proc. Acad. USA 21 (1935), 275-281; JFM 61.0055.*), so zeigt sich, daß sich die Zahlentheorie nicht mehr vollständig gewinnen läßt, sogar nicht einmal der vollständige Gebrauch der Quantifikatoren (``alle'' und ``es gibt''). Ein abschließendes Urteil über typenlose logische Systeme läßt sich natürlich insofern nicht fällen, als man die Gesamtheit aller möglichen Systeme nicht übersehen kann. Es scheint aber, daß sich eine Typentheorie in der einen oder der anderen Form doch nicht entbehren läßt.