The universal quantifier in combinatory logic. (Q5893219)

Verf. beweist in dieser Arbeit einige weitere Sätze über die sogenannten Kombinatoren, die er in zwei früheren Arbeiten behandelt hat (1930; JFM 56.0048.*). Diese Sätze werden benutzt zu einem formalen Beweis des intuitiv als richtig erkannten Prinzips: Wenn ein Ausdruck, der gewisse Variablen enthält, für alle Werte dieser Variablen eine wahre Aussage darstellt, und wenn man einen neuen Ausdruck bildet durch Einsetzung andrer Ausdrücke, die wieder Variablen enthalten, oder wenn man die Variablen transformiert, so ist der neue Ausdruck wahr für beliebige Werte der neuen Variablen. Er stellt zuerst eine rekurrierende Definition des Quantifikators \(\prod_n\) auf mittels der Kombinatoren \(I\) und \(B\) und beweist, daß \(\prod_n\) tatsächlich die Bedeutung eines Präfixes mit n Allzeichen hat. Später definiert er, ebenfalls rekurrierend, den ``formalisierenden'' Kombinator \(\varPhi_n\), mit dessen Hilfe er die Beziehung der Implikation für Funktionen mehrerer Variablen auf die gewöhnliche einfache Implikation zurückführen kann. Bei der genaueren Untersuchung über die Eigenschaften der Implikation sieht er sich genötigt, einige Axiome einzuführen, wie z. B. ein Axiom, dessen Interpretation \[ (f)\left[(x)f(x)\rightarrow (g,x)f(g(x))\right] \] ist. Zum Schlüsse wird das Substitutionsprinzip bewiesen.