On the consistency of Quine's new foundations for mathematical logic. (Q2590258)

Der neueste -- noch nicht an einem Widerspruch gescheiterte -Versuch auf dem Wege zur Konstruktion einer ``typenfreien'' Logik stammt von \textit{W. V. Quine} (Amer. math. Monthly 44 (1937), 70-80; F. d. M. \(63_{\text{I}}\), 23). Verf. gibt in der vorliegenden Arbeit zunächst den Aufbau von drei Kalkülen \(Q\), \(Q_1\), \(Q_2\). Allen drei Kalkülen gemeinsam ist, daß bei der Konstruktion der sinnvollen Ausdrücke nur zwei Symbole verwendet werden: 0 und 1. Der Kalkül \(Q_1\) ist im wesentlichen der Quinesche. Der Kalkül \(Q_2\) ist ein durch ``Kennzeichnungen'' erweiterter Kalkül \(Q_1\). Die Einführung des ``\(\iota\)'' geschieht axiomatisch. Sie ist dadurch besonders beachtenswert, daß die Regeln, die den Gebrauch des ``\(\iota\)'' beherrschen, äußerst handlich formuliert sind. Der Rossersche Beweis für die ``Eliminierbarkeit der \(\iota\)-Symbole'' ist im Grundgedanken dem Hilbert-Bernaysschen (\textit{Hilbert-Bernays}, Grundlagen der Mathematik I. Berlin (1934) F. d. M. \(60_{\text{I}}\), 17), \S\,8) verwandt, ohne natürlich eine mechanische Übertragung zu sein. Der Kalkül \(Q\) wird aus \(Q_2\) erhalten durch Hinzufügung zweier Schlußregeln, von denen eine zuerst in einer früheren Arbeit des Verf. (J. symbolic Logic 2 (1937), 129-137; F. d. M. \(63_{\text{II}}\), 824) angegeben worden ist. Sämtliche Kalküle \(Q\), \(Q_1\), \(Q_2\) sind nicht rein typenfrei. Denn eine wesentliche Rolle spielt in ihnen der Begriff des ``geschichteten'' Ausdrucks. Die Einschränkungen, die dadurch hervorgerufen werden, sind jedoch wesentlich geringer als die entsprechenden in der vereinfachten Stufenlogik. Zumal die Beschränkung auf ``geschichtete'' Ausdrücke nur bei der Formulierung der Axiomengruppe, die der Gruppe der ``Reduzierbarkeitsaxiome'' der Stufenlogik entspricht, effektiv verwendet wird. Nach Vollendung des Kalkülaufbaus führt Verf. (für den Kalkül \(Q_2\)) die Theorie so weit, daß er 41 Theoreme ableitet, unter denen die wesentlichsten bei dem Aufbau der Arithmetik benötigten Sätze vorkommen. In einem Schlußabschnitt unterwirft Verf. dann den Kalkül \(Q\) -- und damit erst recht \(Q_2\) und \(Q_1\) -- einer kritischen Betrachtung hinsichtlich der Frage der Widerspruchsfreiheit. Er erörtert die üblichen Wege zur Konstruktion eines Widerspruchs, zeigt, daß diese Wege für den Kalkül \(Q\) nicht gangbar sind, und untersucht, woran es liegt, daß für \(Q\) in diesen Fällen kein Widerspruch konstruierbar ist. Ein Widerspruchsfreiheitsbeweis wird auf diese Weise natürlich nicht erhalten -- aber für die Stufenlogik (mit Unendlichkeitsaxiom) gibt es z. Z. ja auch noch keinen. Immerhin geht so viel aus Rossers Untersuchungen hervor, daß die Konstruktion eines Widerspruchs -- falls ein solcher konstruierbar ist -- erst gelingt, wenn die Theorie der ``ungeschichteten'' Relationen weiter ausgebaut ist, mindestens so weit, daß man imstande ist ``ungeschichtete'' Relationen durch Induktion zu definieren.