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

Now let us take O!z for ~Jz. It is easy to prove the proposition:
((3): 0!x =. 0o d I. 0z 06z,
whe!ice we get immediately by (1):
(10[): x0!= s Qx'.(!z=60!z)~ i.e.
~!x.' x.. 0!,: z. 0V - 0!z.
Then, assuming the convention of Whitehead and Russell we
have proved that all equivalent matrices must be identical; which
is a paralogism. So we cannot assume Whitehead and Russell's
convention. As and I see no means of making any other useful
convention, i have tried to note explicitly the scope of,z(.z)("
i. e. I have assumed the following definition:
[z(ez)].f (tpz()}. =: (3h0): x.- x:/{!-.z}. Df
With such a definition of a function of class we avoid all
ambiguity, but it soon appears that we get no simplification of
the calculus of functions. This becomes clear if we remark that,
e. -[z(Çz)l.f{z(Vpz)} and [z(pz)]. f{z(ez)} are two different
functions. It is to be noted that, if we do not assume that any two
equivalelit matrices must be identical, we have the proposition:
[z (z)] [z(z,)]. c z )4 +: ([z).
where the symbol t is given by the definition (13'02)
5x - y.. (x=-y). Df
The most important consequence of our notiiin the scope of
the class-symbols is as follows:
We can prove:
[z()z}\: Lz(OZ)]. %(8vr) - - 2 (0-):J: z.. - O (P: 20.15)9
but we cannot prove:.. 3 z. 3 ~': g{\(^z)].z /' [z() 1} ~ z) g{; (~).1 /'[ ([( )1.}.
Therefore, given any function of the form:
we cannot take for a any class sueli, that'
x a. 5 x~pg