Untersuchungen über den Aussagenkalkül von A. Hey\-ting. (Q2593902)

Es sei \[ \begin{alignedat}{2} &M_1 &&= \{1.\;CpCqp,\quad 2.\;CCpCqrCCpqCpr\},\\ &M_{11}&&=\{1.\;CpCqp,\quad 2.\;CCpCpqCpq,\quad CCpqCCqrCpr\},\\ &M_{12}&&=\{1.\;CpCqp,\quad 2.\;CCpqCCpCqrCpr\},\\ &M_2 &&=\{1.\;CKpqp,\quad 2.\;CKpqq,\quad 3.\;CCpqCCprCpKqr\},\\ &M_3 &&= \{1.\;Cp\,Apq,\quad 2.\;Cp\,Aqp,\quad 3.\;CCprCCqrCApqr\},\\ &M_4 &&= \{1.\;CEpqCpq,\quad 2.\;CEpqCqp,\quad 3.\;CCpqCCqpEpq\},\\ &M_5 && =\{1.\;CCpNqCqNp,\quad 2.\;CNpCpq\},\\ &M_{51}&&=\{1.\;CCpqCCpNqNp,\quad 2.\;CNpCpq\},\\ &M_{52}&& =\{COp\}. \end{alignedat} \] Vorausgesetzt ist außerdem der übliche, durch Einsetzung und Abtrennung bestimmte Folgerungsbegriff. \(M = M_1 + M_2 +M_3 +M_4+M_5\) ist ein dem Verf. vom Ref. seiner Zeit mitgeteiltes unabhängiges Axiomensystem in \(C\), \(K\), \(A\), \(E\), \(N\) für die Satzmenge \textit{heyt} des Heyting-Kalküls, wobei zu \(M_5\) die nachträgliche Mitteilung des Verf. in der nachstehend besprochenen Arbeit heranzuziehen ist. In \(M\) kann \(M_1\) durch \(M_{11}\) bzw. (p. 52 dieser Arbeit) durch \(M_{12}\), \(M_5\) durch \(M_{51}\) bzw. für \(Np =_{\text{Df}}CpO\), \(O =_{\text{Df}}NCpp\) durch \(M_{52}\) ersetzt werden (\S~5 dieser Arbeit). \(M_4\) ist in der bekannten Art durch \(Epq=_{\text{Df}}KCpqCqp\) eliminierbar. \(M_0 = M - \{CNpCpq\}\) ist ein Axiomensystem in \(C\), \(K\), \(A\), \(E\), \(N\) für die Satz\-menge \textit{mink} des \textit{Kolmogoroff-Johansson}schen Minimal-Kalküls (Compositio math., Groningen, 4 (1936), 119-136; F. d. M. \(62_{\text{II}}\), 1045). \(M_{00} =M_1+\{CCpqCCpNqNp\}\) ist ein Axiomensystem in \(C\) und \(N\) für die auf \(C\) und \(N\) beschränkte Satzmenge \(\text{\textit{mink}}_0\) dieses Kalküls. Das Haupttheorem dieser Arbeit ist das \textit{Homogoneitätstheorem für heyt} (p. 98, Satz 6 und Amn. 3): Ist \(H\) ein Heyting-Satz, der einen der aussageerzeugenden Funktoren \(K\), \(A\), \(E\), \(N\) nicht enthält, so ist \(H\) ableitbar aus der Teilmenge von \(M\), in der nur die in \(H\) enthaltenen Funktoren vorkommen. -- In \S~12 wird ein entsprechen\-des Theorem für die mit \(\text{\textit{mink}}_0\) zusammenfallende Satzmenge des (Zusatz des Ref.: mit dem Johansson-Kalkül in \(C\) und \(N\) identischen) Kolmogoroff-Kalküls bewiesen: Jeder \(N\)-freie \(\text{\textit{mink}}_0\)-Satz ist aus \(M_1\) ableitbar. -- Hieraus und aus dem Beweis für das erste Theorem ergibt sich das nicht explizit formulierte, dem ersten genau ent\-sprechende \textit{Homogeneitätstheorem für mink}. Auf dem Wege zum Beweis des Haupttheorems ergeben sich als wesentliche Resultate: (1) eine neue Lösung des Entscheidungsproblems für den Heyting-Kalkül (\S~9), (2) das inzwischen auch von \textit{J. C. C. McKinsey} (vgl. die Besprechung auf S. 1105) auf eine ganz andere Art bewiesene Theorem von der wechselseitigen Un\-definierbarkeit von \(C\), \(K\), \(A\), \(N\) (\S~10). -- Endlich ergibt sich aus dem Haupttheorem noch das Theorem von der Identität der Satzmenge der positiven Bernays-Logik, mit der Folgerungsmenge aus \(M - M_5\), also mit der Satzmenge des positiven (\(N\)-freien) Heyting-Kalküls: eine höchst aufschlußreiche Koinzidenz, wenn man bedenkt, daß die positive Bernays-Logik dazu bestimmt ist, aus der Menge der \(N\)-freien Sätze des klassischen Aussagenkalküls die den Regeln des hypothetischen Schließens ent\-sprechende Teilmenge auszusondern. Vgl. \textit{Hilbert-Bernays}, Grundlagen der Mathe\-matik I (1934), 68f. und jetzt auch II (1939; F. d. M. 65, 21 (JFM 65.0021.*)), 422-450, wo auf die vorliegende Arbeit wiederholt Bezug genommen ist. Die entscheidende Komponente des Theorems von der Identität der Satzmenge des (auf die \(C\)-Sätze der positiven Bernays-Logik beschränkten) positiv identischen Bernays-Kalküls mit der Folge\-rungsmenge von \(M_1\) ist mit \S~3, Satz 1 bewiesen.