In the type theoretic account of inductive types, we established the recursion-
induction principle which specifies the elements which can be obtained by a
finite process of recursion. A similar concept can be established in the
set theoretic approach by defining the least fixed point of .
A sequence of sets defined by a monotone can be defined, such that:
Clearly, we would like to consider this union of sets defined by
indefinitely (i.e.
.
To do this requires
a brief discourse in the concept of ordinal numbers. In laymans' terms,
ordinals
are an infinite set of numbers, whose beauty lies in the
fact that they continue forever. A slightly more detailed account of
ordinals is provided in
class notes 7
from fall 1993 for those who are
interested. The simple definition will suffice here.
Given the above knowledge, we can rewrite the indefinite union from above as
an ordinal.
Now because is monotone, it is true that
.
In fact, for any ordinal ,
.
Proof: The proof left as an exercise to the reader. Consider the fact
that since
, and
prove inductively.
Above, we claimed that we would like to apply indefinitely in order to
define the inductive type completely. Yet intuition tells us that eventually
must stop growing. Indeed, by our definition of
-rules
on the previous page,
, where
has cardinality
.
Therefore,
, which implies that this chain of sets cannot
grow indefinitely.
It then follows that for some
It is this which we define as the least fixed point of
.