Principia mathematica, by Alfred North Whitehead ... and Bertrand Russell.

*120. INDUCTIVE CARDINALS.

Summary of *120.
Inductive Cardinals are those that obey mathematical induction starting
from 0, i.e. in the language of Part II, Section E, they are the posterity of 0
with respect to the relation of v to v +, 1, or, in more popular language, they
are those that can be reached from 0 by successive additions of 1. In
former days, these were supposed to be all the cardinals, and mathematical
induction was treated as a kind of self-evident axiom. We now know that
only certain cardinals obey mathematical induction starting from 0. It is
these cardinals which are to be considered in this number. They embrace
0, 1, 2,... and generally all those cardinals which would be commonly called
finite, all those which can be expressed in the usual Arabic system of
numeration, and no others. The propositions to be proved concerning them
in this number are elementary and familiar; the interest lies entirely in the
definition and method of proof, not in the propositions themselves.
Put NC induct = a ta (+c 1)* 0} Df.
Since (+c 1)* has necessarily its domain and converse domainl ot the salle
type, it is important to be careful in noting the relations of type. Accordingly we also put
NtC induct = a a (+c l), 0e} Dfl
We begin by applying the propositions of *90. Thus we have,120-11.:. a e N,C induct: qb. D ~. ) (: +c 1): b0,: D. *a
*12012. F. 0 NCinduct
*120-121. F a e NCC induct. D. (a +4 1)c e NGC induct
*12013. F:. a e N,C induct:: e N,C induct. 4. Dt. + ( +) 1 ): )0,: D. Oa
*120'15. F: a e NC induct. i! a. D. sm"a e NC induct
*120-151.: a e NC induct.! a..a +c 1 NC induct
*120152. F a E NC. sm"a e NC induct - t'A. ). a e NC induct - t'A
We then proceed to deduce the elementary properties of ilndlctive
classes, putting
Cls induct = s'NC induct.
We have
*120-21. F: p e (Cs induct. _. Noc'p NC induct