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

69
This relation enables us to have the following definition of:a homogeneous cardinal number of the class x having the type
DaC. -
103-01 N-' = co[ co smr x]
dg
We see that Nc' is the class of all reducible classes of the
type DaC, which are similar to x.
We shall use the abbreviation:
101001 Q DC
101o002 A' - (A Q)
cf
The numbers 0, 1, 2 are defined as follows:
101-01 0 = Nc' A':101-02 1 =Nc (t'aa U A')
101-03 2 = Nce ((LCa Ua ' - a) Ua A')
101 003 A"=(A n lQ 1)
The class of cardinals other than /" being denoted by NC,
we have the following definition:
103-02 NC= a [( x): a =Nxc: '. {, NLCCQ}.]
df' Q
We now have the following propositions concerning the use
of Red, w).
101'1001 -: C ow: extens[Q(, ] }.i) Red (w).3 Red(x)
Dem |- 22 44 _ 1- Hp: w' C ^: D ' (C o: Red (w),
o a
[1 0 33jl] 3D - Prop.
101 1002 gI- Red (x, ) 3 Red (( Ua, ))
Dem. 1- 22 43- 68 621 3 -: ' C (x Ua,, ): extens [Q(a)] {'}.
a a:(' a) C X.: (' nra w) c o'. ' =((n' ) Ua,(' ( -, 0j)): (1)
I- 35431-65'412 D 1-: X' C (xULo w) extens [R,jx'}.Pe1 -Cls:
aFP= ':. {P, C}.
a.D.(p (nw (a )) 1 -. Cls (PP ( fla. ))ç 1 -*Cls': (a(P: (X na ))Cx:
(a(P7(X' (n w) C w:. P= ((r('n a))Ua(P(x' a w ))) (2)
a a a a a