The theory of constructive types (principles of logic and mathematics). By Leon Chwistek.

53
We have the following proposition:
<A) (a7j.(~[(a)/ ~ {n }4 j z [(a?G { M} j). l 4{ [(a4 G{:z},x}
L
To see this, suppose we have: ~ G {z[(3P G {, z}], x}, i. e.
(7). (z[( ).f{, {lz}] z i(u ") G Ip, z}]) D 7f [(3 [ F) G { }L, 2}.
This proposition being true for every f, it is true for G.
Therefore we have:.(2 [ ) G {(", }] =- [j 1) G { 1z}]) D G { [( I3-) G {( 4}], x)
Here, the hypothesis being true by 1315, we have:
G {z 1(Ip) G {pf z}], x}, i e. the proposition (A).
Nuwi it is obvious that the function /f whose existence is proved
by (A), cannot be equivalent to G. Therefore we never shall have
'such a function, unless we assume the axiom of extension. As a system containing such an axiom in no longer one of pure logic, we
see that there is no system of pure logic to be based on the simplified theory of types.
I do not know whether an adequate definition of the hypothesis of Nominalisin is to be found in a system of Ontology using
no other primitive idea- than purely logical ones. At any rate the
Intax is a part of the hypothesis of Nominalism. Another constituent of this hypothesis would be the following axiom, which, as
is at once to be seen, is inconsistent with Proposition (A):
(x[~ av) fV {V: }] = [([ ïv) Gv (v, }]) D
L
(n x If {II, Ix = u x[G ~ {, x}])
This axiom enables us to prove that the class of functions of the
type W is similar to the class of classes x[(3v)fJv {v ], where;ux [L/{;,4)l is a function of the tyl)e W. The proof of this proposition is a trivial application of our axiom. We should then have
in any type the same cardinal numbers in spite of Cantor's theory.
INevertheless the axiom in question seems unfruitful, if used in a,system of Mathematics. To obtain a satisfactory one, we ought to
suppose that any type is similar to a class of inductive numbers.
We shall call this hypothesis the A x iom o f N o m i n a 1 i s m ). Note
1) Cf. Zasady czystej teorji typow. Przeglad;fil 1922 p. 28.