Transfinite induction

Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC. Let be a property defined for all ordinals . Suppose that whenever is true for all , then is also true. Then transfinite induction tells us that is true for all ordinals. Usually the proof is broken down into three cases: Zero case: Prove that is true. Successor case: Prove that for any successor ordinal , follows from (and, if necessary, for all ). Limit case: Prove that for any limit ordinal , follows from for all . All three cases are identical except for the type of ordinal considered. They do not formally need to be considered separately, but in practice the proofs are typically so different as to require separate presentations. Zero is sometimes considered a limit ordinal and then may sometimes be treated in proofs in the same case as limit ordinals. Transfinite recursion is similar to transfinite induction; however, instead of proving that something holds for all ordinal numbers, we construct a sequence of objects, one for each ordinal. As an example, a basis for a (possibly infinite-dimensional) vector space can be created by starting with the empty set and for each ordinal α > 0 choosing a vector that is not in the span of the vectors . This process stops when no vector can be chosen. More formally, we can state the Transfinite Recursion Theorem as follows: Transfinite Recursion Theorem (version 1). Given a class function G: V → V (where V is the class of all sets), there exists a unique transfinite sequence F: Ord → V (where Ord is the class of all ordinals) such that for all ordinals α, where denotes the restriction of Fs domain to ordinals < α. As in the case of induction, we may treat different types of ordinals separately: another formulation of transfinite recursion is the following: Transfinite Recursion Theorem (version 2)'''. Given a set g1, and class functions G2, G3, there exists a unique function F: Ord → V such that F(0) = g1, F(α + 1) = G2(F(α)), for all α ∈ Ord, for all limit λ ≠ 0.