Die Widerspruchsfreiheit der Stufenlogik. (Q2605697)

Man hat die Frage der Widerspruchsfreiheit der \textit{reinen} Stufenlogik zu unterscheiden von der Frage nach der Widerspruchsfreiheit der \textit{angewandten} Stufenlogik oder genauer der Formalismen, die entstehen, wenn man die Axiome und Regeln der Stufenlogik durch Hinzunahme von Axiomen, die einen bestimmten Gegenstandsbereich charakterisieren, erweitert. Die reine Stufenlogik muß widerspruchsfrei sein, wenn es einen Gegenstandsbereich gibt, so daß die Stufenlogik in Anwendung auf diesen Bereich widerspruchsfrei ist. Der Verf. beweist daher die Widerspruchsfreiheit der reinen Stufenlogik, indem er zeigt, daß die auf den einfachsten nicht-leeren Gegenstandsbereich, der aus einem einzigen Element besteht, angewendete Stufenlogik widerspruchsfrei ist (mit dem gleichen Grandgedanken haben \textit{Hilbert} und \textit{Ackermann} die Widerspruchsfreiheit des elementaren Prädikatenkalküls bewiesen). Durch Modifikation des Beweises läßt sich leicht die Widerspruchsfreiheit der Stufenlogik in Anwendung auf beliebige endliche, jedoch nicht auf alle (insbesondere unendliche) Gegenstandsbereiche beweisen. Unter der Stufenlogik versteht der Verf. (wie heute vielfach üblich) die Logik der \textit{Principia Mathematica} ohne verzweigte Typentheorie und ohne besondere Klassenzeichen; eine Variable \(\nu\)-ter Stufe \(\mathfrak a_\nu\) kann daher sowohl als Klassen- als auch als Prädikatenvariable \(\nu\)-ter Stufe interpretiert werden. Eine wesentliche Vereinfachung erfährt der Aufbau der Stufenlogik durch die Beschränkung auf einstellige Prädikate, die nach einer Bemerkung von \textit{Gödel} auch alle \textit{mehr}stelligen ersetzen können. Die von dem Verf. benutzte Formalisierung der Stufenlogik mag kurz so gekennzeichnet werden: Die aus der elementaren einstelligen Prädikatenlogik bekannten Axiome und Regeln werden für Ausdrücke beliebiger Stufe formuliert und durch das \textit{Gleichheitsaxiom} \[ [\forall \mathfrak x_\nu(\mathfrak a_{\nu+1} \mathfrak x_\nu \supset \subset \mathfrak b_{\nu+1} \mathfrak x_\nu)] \supset \mathfrak a_{\nu+1} = \mathfrak b_{\nu+1}, \] das \textit{Komprehensionsaxiom} \[ \exists \mathfrak x_{\nu+1} \forall \mathfrak y_\nu \left[ \mathfrak x_{\nu+1} \mathfrak y_\nu \supset \subset \text{ Subst } \mathfrak A \binom{\mathfrak a_\nu}{\mathfrak y_\nu}\right] \] (inhaltlich: Eine Aussageform \(\mathfrak A\), in der die Variable \(\mathfrak a_\nu\) vorkommt, bestimmt eine Menge \(\mathfrak x_{\nu+1}\), nämlich die Menge derjenigen \(\mathfrak a_\nu\), auf welche \(\mathfrak A\) zutrifft) und das \textit{Auswahlaxiom} ergänzt. -- Der Widerspruchsfreiheitsbeweis wird nun so geführt: Besteht der Gegenstandsbereich aus einem einzigen Element, so gibt es \(2^\nu\) Elemente (Mengen ) \(\nu\)-ter Stufe \(\gamma_\nu^{(1)}\), \(\gamma_\nu^{(2)}\), \dots, \(\gamma_\nu^{(2^\nu)}\), nämlich alle Mengen von Elementen \((\nu - 1)\)-ter Stufe. Einem Ausdruck \(\gamma_\nu^{(\sigma)} \gamma_{\nu-1}^{(\tau)}\) läßt sich dann, inhaltlich gesprochen, der Wert ``Wahr'' oder ``Falsch'' zuordnen, je nachdem \(\gamma_{\nu-1}^{(\tau)}\) der Menge \(\gamma_\nu^{(\sigma)}\) angehört oder nicht. Ersetzt man nun in den Formeln einer stufenlogischen Herleitung alle Variablen \(\nu\)-ter Stufe in gewisser Weise durch die \(\gamma\) \ \(\nu\)-ter Stufe, so entstehen aussagenlogische Verbindungen von \(\gamma\gamma\)-Ausdrücken, die sich elementar ausrechnen lassen. Es läßt sich zeigen, daß die Formeln einer Herleitung dabei stets den Wert ``Wahr'' ergeben, während eine Formel der Form \(\mathfrak A \;\& \;\sim \mathfrak A\) den Wert ``Falsch'' annehmen würde. Das von Verf. angewendete Verfahren ist in ähnlicher Form von \textit{Tarski} zum Beweis einer gewissen Nicht-Beweisbarkeit-Aussage in der Stufenlogik benutzt worden (\textit{A. Tarski}, Mh. Math. Phys. 40 (1933), 97-112 (F. d. M. \(59_{\text{I}}\), 53), insbes. S. 106-108).