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

81
120-001 NI C induct = NC()) induct
df
It is obvious that the - order inductive numbers do not necessarily belong to all hereditary classes of another order. Now, it
is useful to speak about No C induct- order inductive numbers.
We shall see below that the inductive numbers of this order have
all fundametal group-properties of the natural numbers. Therefore
we shall call these numbers simply inductive numbers, and
we shall use the following definition:
1 20013 NC induct = NC(NoC induct) induct
dJ
It is easy to prove that all,inductive nnmbers" are 0i-order
inductive numbers. We have the following proposition:
120-1011 ]-,e~NC induct 3 teloCinduct
Dem 1- 24-2324 3
H-. Hp. H(g, 0). Cg, i}. D H((gU1(No Cinduct n, A)), 0)
[Hp] 3 Te,(g U1 (N Cinduct lAo))
[24-23-24] D e1g
D [- Prop.
The following propositions concerning NoCinduct can be proved by the same method for NCinduct.
120'1 1- ae1ioCinduct (g): H(g,O) e ag. C{g 0}.
To prove this proposition we use 120-001 and we show in
an easy manner that NG induct is an extensional class.
120'11 i 1. H(g,O). {g, }. o elNCinduct. Oas g
120-12 1- H(g, )) oeg
120'121 i-. H(g, 0) 3D oe1g. D. H(g, 0) (- 1)e,g.
120-122 - H(g,0) 1 elg [120-12-121. 110-641.]
120-123 1- H(g,0)3 2e g [120-122-121.110-643.]
Note that, if any natural number, e. g. 1918: is defined in
our system, we can prove the proposition 1918 e JNVoCinduct, using
1918 times the method of the proof of 110-122.
120-124 i- (a+1) + 0 [1 10 4.101 1. 10-632.1
120-14 1- oCinduct C ( VCUti A ") ]120121'121.]
120-02 Cls () induct=- [(:a) a. NC(0) induct. xel a.]
d4
120-021 ClsO induct= Cls (0) induct
df
120-023 J(h) = (X) (T): extens (x). xe'h. 3D (-x Uat t) 'Ih.
df