Beweis der Widerspruchsfreiheit des Funktionenkalküls der mathematischen Logik. (Q2619878)

Verf. beschhäftigt sich mit dem in unserem Buch (\textit{D. Hilbert, W. Ackermann}, Grundzüge der theoretischen Logik, 1928 (F. d. M. 54, 55 (JFM 54.0055.*)), zitiert im folgenden als H. A.) aufgestellten engeren Funktionenkalkül und versucht, das dort für diesen Kalkül aufgestellte Axiomensystem wesentlich zu vereinfachen. Daß man entweder das All- oder das Seinszeichen, hier das Seinszeichen, sparen kann, ist bekannt (vgl. H. A., Seite 47 oben). Es kommt dann aber die durchgängige Symmetrie zwischen All- und Seinszeichen nicht zum Ausdruck. Verf. behauptet aber auch, daß die drei Einsetzungsregeln, die bei uns als Prinzipien auftreten, sich ableiten lassen. Zum Beweis soll der bekannte Gedanke von \textit{Hilbert}, statt der Variablen in der ganzen Beweisfigur von vornherein die Einsetzungen zu gebrauchen, dienen. Durch diese Methode werden aber die Einsetzungsregeln nicht überflüssig, sondern es wird nur die Art ihrer Anwendung modifiziert, indem die Einsetzungen zurückverlegt werden und nur direkt bei den Axiomen zur Anwendung kommen. Man kann dann die festen Axiome ganz fallen lassen und statt dessen nur Regeln zur Bildung von Axiomen, Axiomenschemata, nehmen (über die Axiomenschemata vgl. z. B. \textit{Hilbert-Bernays}, Grundlagen der Mathematik, 1. Bd. (1934; F. d. M. \(60_{\text{I}}\), S. 249). Bei dem in unserem Buch angegebenen endlichen System von Axiomen sind aber die Einsetzungsregeln keineswegs überflüssig. Das Mißverständnis des Verf. erklärt sich offenbar daraus, daß er in unseren Axiomen derartige Axiomenschemata sieht, weil ihm der in unserem Buch auftretende Unterschied von großen deutschen und großen lateinischen Buchstaben nicht aufgegangen ist (vgl. darüber H. A. S. 12 unten). Eine Formel \(A \vee A \rightarrow A\) z. B. baut sich aus den formalen Bestandteilen \(A, \vee, A, \rightarrow, A\) in dieser Reihenfolge auf, dagegen ist \(\mathfrak {A} \vee \mathfrak {A} \rightarrow \mathfrak {A}\) keine bestimmte Formel, sondern nur ein Formelschema, in das zwar \(A \vee A \rightarrow A\), aber auch z. B. \[ (A \& B) \vee (A \& B) \rightarrow (A \& B) \] hienipaßt. Unter unserem Axiom \(A \vee A \rightarrow A\) versteht nun der Verf. offenbar das Schema \(\mathfrak {A} \vee \mathfrak {A} \rightarrow \mathfrak {A}\). Nun liegt es natürlich in seinem Belieben, da lateinische Buchstaben zu gebrauchen, wo wir deutsche verwenden. Es hätten dann aber für die formalen Bausteine der Formeln, die wir eben mit lateinischen Buchstaben bezeichnen, nicht ebenfalls unterschiedslos lateinische Buchstaben verwendet werden dürfen. So enstehen nur Verwirrung und Unklarheiten. - Zu dem Widerspruchsfreitheitsbeweis für den engeren Funktionenkalkül, den der Verf. angibt, ist zu sagen, daß er viel zu umständlich ist, da sich für diesen Bereich die Widerspruchsfreiheit noch auf triviale Weise erkennen läßt (vgl. H. A. Seite 65).