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

16
Of course, in practice this substitution is always possible, as
we have to use only extensional functions, but we must prove, for
any given instance that our function is extensional. Now, for the use
of extensional functions the use of the Leibnizian idea of identity
is, as a matter of fact, superfluous Hence, our definition of a function of a class seems to be useless.
2. I pass to the followiig difficulty of the Whitehead-Russellian theory of classes, which seems to be more essential. Let us
prove *20'7 for classes of classes Thus we must first write,121
iii the following manner:
(a/'f):îf t { 0! (01 {) } g (l)}
Le us now write explicitly -20'7. We have:
(a/l,): (W,):! " a -^ yî: ct:/!(i cî): =^(a^):!f ô =-,_ 0.!a:g(t!t).
It is obvious that to prove such a proposition, we should have:
a J):/!{g)!Q~}.e, g3!{mr }
Now, remark that tins proposition has the followxrig meaning:
a /':.f!{(.I0):!x e-.:!(0O!)}:, 3 {(a O): 0s!x-.E @ 0I^! ).
Thtu. we see that the axiom of reducibility must be assumed
fur variables of the type:
(M0): O!.,. ze:x o(01 0!.
Note that the sane difficulty subsists, if we note explicitly
the scope of the class-symbols. If we will not assume the axiomi
of reducibility for such functions as: C{(l0): O!x - =(_. kx (06)}.
such a primitive proposition being of course some-what artificial,
we should assume this axiom for variable functions of any type.
Now, in Principia we have no other functions but those of matrices
or individuals. Therefore a radical modification of the system of Whitehead and Russell seems absolutely necessary. even if we agree
with the axion of reducibility. We then meet the following difficulties:
A. Suppose we agree with such symbols as:
/!{^}s~c g{(éi)},