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

80
119-45 -. ((a+ -) - a')eNC. (z-a')N.
(( + -t) -- ~') -=(o +-( )).
The proof of these propositions is to be got by a direct applicatiun of the method of Principia and of lemmas 101'10011002.
VIII. Indnctiive niuiiberSe
The Theory of iductive numbers, as based on the pure theory
of Types, is quite complete and seems very simple. Moreover, it can
be exposed in a quite popular way, without any serious difficulty.
I begin with the definition of an hereditary class.
12.0001 J(g, )=. eg. ( e) gD (a — 1) eg: {a l}
df
We have now following proposition
120-101 H(u'[. (g, ) D o'e*, g], )
Dem g 5'5 H(g z)3:H(gT) 3G' g. G'selg.
[(120 001)] D H(u'[. H(a, ) D a' g.]. r) (1)
- 221 ) - - f(g, ): -f(g, ) a'E. {/i }.
[(120'001)] H( '['. H(g, ) D3 'e g.], r) (2)
(1). (2)0 g _j - Prop.
Note that H(g,,z) is ambiguous in respect to the type of g.
I proceed now to the definition of inductive numbers. The class of
inductive numbers ought to be the logical product of all hereditary
classes, i. e. all classes g sùch that M(g, 0). Now, we cannot speak
about,all hereditary classes', these classes not having the same
type. Therefore we cannot speak simply of inductive numbers, as
we have different orders of them.
Let us now lay down the definition:
120 002 H = - [[ Ca). NC. Tl NC.]
Our definition of the -order inductive numbers will be:
120-01 NC(O) induct = [(): H(g, 0) 3 re1g: el g, >}.]
This definition is a pattern for definitions of inductive numbers in any order, We shall here use the definition.