On the axiom of reducibility. (Q2610748)

Die Typentheorie von \textit{Whitehead} und \textit{Russel} besteht bekanntlich aus zwei Teilen, der einfachen Typentheorie, die die Aussagefunktionen nach der Art ihrer Argumente in eine Hierarchie von Typen einordnet, und der verzweigten Typentheorie, die außerdem bei den Aussagefunktionen eine weitere Unterscheidung je nach Art ihrer Definition vornimmt. Die verzweigte Typentheorie machte die Einführung des Axioms der Reduzibilität erforderlich. In der Vorrede zur zweiten Auflage der Principia mathematica (1925; F.~d.~M. 51, 46) führte \textit{Russel} ein abgeschwächtes Extensionalitätsprinzip ein, indem er formal äquivalente Aussagefunktionen, die außerdem dieselbe Stufe im Sinne der verzweigten Typentheorie besitzen, identifizierte. Von \textit{Ramsey} wurde vorgeschlagen, die verzweigte Typentheorie und damit das Axiom der Reduzierbarkeit fallen zu lassen. Verf. zeigt zur Unterstützung der \textit{Ramsey}schen Überlegungen, daß gerade das Axiom der Reduzierbarkeit und das genannte \textit{Russel}sche Extensionalitätsprinzip die Gültigkeit des \textit{Ramsey}schen Systems garantieren. Man braucht ja nur festzusetzen, daß jeder Ausdruck, der im System der Principia mathematica eine nichtprädikative Aussagenfunktion \(\varphi\) bezeichnet, im neuen System die prädikative Funktion bedeuten soll, die gemäß dem Axiom der Reduzierbarkeit mit \(\varphi\) formal äquivalent und die nach dem obigen Extensionalitätsprinzip eindeutig bestimmt ist. Es ergibt sich also, daß entweder die Einführung des Axioms der Reduzierbarkeit überhaupt nicht berechtigt oder daß dieses Axiom samt der verzweigten Typentheorie entbehrlich ist.