A set of axioms for the theory of deduction. (Q2619868)

Verf. gibt hier für den Aussagenkalkül und den Prädikatenkalkül eine Axiomatisierung, bei der, im Unterschied von der Behandlung in den ``Principia Mathematica'', die Formalisierung in strengster Weise durchgeführt und auch bei der Ableitung der logischen Formeln nicht mehr auf ihre inhaltliche Bedeutung Bezug genommen wird. Die Axiome an und für sich sind dieselben wie in den ``Principia''. Beim Aussagenkalkül fehlt nur das von \textit{P. Bernays} (1926; F. d. M. 52, 49 (JFM 52.0049.*)) als überflüssig nachgewiesene Axiom. Beim Prädikatenkalkül tritt bei der strengen Formalisierung eine gewisse Schwierigkeit dur die Typentheorie auf, da die Axiome der ``Principia'' immer nur für einen bestimmten Typ gelten und also eine Formel, die für irgendeinen Typ abgeleitet ist, für einen anderen Typ immer wieder von neuem bewiesen werden muß. Diese Schwierigkeit wird durch Einführung von zwei verschiedenen Variablengattungen überwunden. Während eine ``intra-typical variable'' auf einen bestimmten Typ beschränkt bleibt, erstreckt sich der Bereich einer ``inter-typical variable'' auf mehr als einen Typ. Eine freie Variable der ersten Art kann immer durch eine gebundene Variable ersetzt werden, nicht aber eine Variable der zweiten Art, denn ihr Einsetzungsbereich kann nicht immer als eine Klasse angesehen werden. Durch die Einführung der ``inter-typical variable'' wird das Reduzibilitätsaxiom der ``Principia'' trotz Beibehaltung der Typenlehre entbehrlich (vgl. auch die ähnliche Zwecke verfolgende Arbeit des Verf. in Ann. of Math. (2) 36 (1935), 670-678; F. d. M. \(61_{\text{I}}\), 54).