Using the Recusion Theorem (recursion on ordinals) we can give the official definition of the cumulative hierarchy first introduced informally in an earlier web page.
Definition.
We define , , and .
Alternatively and equivalently the single equation suffices in all cases, when is zero, a successor or a limit.
This is well-defined, by the Recursion Theorem.
Proposition.
For all sets there is some with .
Proof.
By -induction on . We have and if define a function mapping each to the least ordinal such that . Thus is a set by replacement, hence is an ordinal and it can be checked that .
Definition.
The rank of a set is the least ordinal such that .
This is well-defined by the proposition above. An alternative equivalent definition is obtained from .
The formal definition of the cumulative hierarchy and rank completes a major piece of work in the setting up of Zermelo-Fraenkel set theory: it shows that the axiom of ZF do capture in some sense the intuitive idea of the hierarchy of pure sets and the notion of sets constructed in stages that we talked about to justify the axioms, especially foundation. Of course, by Gödel's incompleteness theorem the ZF axioms cannot settle everything and we shall go on to look at further axioms that we can reasonably add to them. This is the subject of the next web page in this sequence.