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

42
23-051. P(a, - Q(, b). -. P(,. b) i -- (a, b)
dj
23-052. P(x, a) Q(x, a) P(x, a) - Q(x, a)
Remark that Whitehead and Russell use for relations instead
of (, qn, U - the symbols: 3. (h, nt,'; nevertheless, as these
symbols have no meaning in isolation, we having only such
expressions as CQ, or M - NA etc. the use of different symbols in both cases is, as a matter of fact, superfluous. -
B. Identity.
The definition of the identity of two classes (relations) is as
follows:
13-01. ==-.=(x).o {x}- ( {}.
df
13 01 1. i ) = T(a) * = (u) * (a) {} - a) {u}.
dl
13 012. i = N. =(j (y) l. iL{x( { } = A {y7,
d/
13 013. P(a b) = Q(. b *. (-) (v. P(a,. ) {, } _ U, ab {(U, V.
13-014. P(, a) Q(x, a (y) V). P(x, ) {y, V} = Q(. ) ){y, vi.
det
13-02 ~.4.=-. =. etc.
dl'
13-U22.M N -. = iM = N. etc.
df
We see that identity of classes (and of relations) is essentially
different from the Leibnizian identity used by Whitehead and
Russell. With our definitionis we have no such proposition as
': —=. _.f({} = /'{(}: but'as a matter of fact, this proposition is completely useless, as we need only another and
less general proposition, to be given below. I begin with the
following abbreviation:
13-015.= v.=.:.z v: ({U.'Ct}: {v,)}.
a, b df
13-016.u= v.=.: iG=v: vt'I,G 6a)} {^V T(a)}.
a(a), ((a)
etc.
Now, I pass to the definition of an extensional function:
13'04 extens [(,)] = f [(, v):'u = v-.- ): f {l} f,{v}: ({f, I(a)}:]
dJ a, a
130041 extens -R(,,,] =-f [(u, v. w. t):. u =v.: w = t:
df a,a b, b:. b. {U W> ta-} =.,, tv {>7: {/, R(,, )}:]