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

52
We see that the o'c-order Leibnizian identity of two classes implies their identity (equivalence).
I shall use the following abbreviations:
13)0012 ==u[.:u= V:u{x}: {u, V}.]
dj:1300121 W=R[.ao"'{R}.z{, }.i
d/
13.0013 (R-= P) =(T):T{Z}3Dr{P}.z{7, W)}.
L * *
The definition of the Axiom of Intension, i e. Intax, is as
follows:
13002 Intax =.(:[r{}fly{x}.] - x.l' {x.}y{x}.] )
df - L
L
We have now the proposition:
13-4 -. Intax D (E?T, v).-(u = ):-. vl-uV: -v {U, V}:.
Dem. [13002 V.10-24
Thus it is obvious that the Intax is not consistent with the Axiom.
of Extension. Now, it is possible to prove, as we shall see below,
that Intax implies Infinax (i. e. the Axiom of Infinity).
On the contrary there seeins to be no real simplification of
Arithmetic, if we assume the axiom of extension -The problem
of the Leibnizian identity of two equivalent classes or relations can
be eliminated by simply dealing with extensional classes or relations,
as we have seen in Part I. The axioin of extension would be needed only in the simplified theory of types, to avoid the proof of`
the existence of classes, which can never be explieilly given. This
proof is as follows:
In the simplified theory of types we have the complete Leibnizian identity, which is to be defined as follows:
(= - y)= (.{.x,}D {</}.
L dF
Now let us assume the following definition, using a, fP as variable
class-letters:
G =ax[(jf).(z[() {,}]-a). J'{a,}.]
dt L
t) The possibility of such a proof was suggested to me by Mr Greniewski