Editing Transfinite induction (section)

==Transfinite recursion==
'''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 (vector space)|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 [[Linear span|span]] of the vectors <math>\{v_{\beta}\mid\beta<\alpha\}</math>. 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<ref>A class function is a rule (specifically, a logical formula) assigning each element in the lefthand class to an element in the righthand class. It is not a [[function (mathematics)|function]] because its domain and codomain are not sets.</ref> ''G'': ''V'' → ''V'' (where ''V'' is the [[Class (set theory)|class]] of all sets), there exists a unique [[transfinite sequence]] ''F'': Ord → ''V'' (where Ord is the class of all ordinals) such that
:<math>F(\alpha) = G(F \upharpoonright \alpha)</math> for all ordinals ''α'', where <math>\upharpoonright</math> denotes the restriction of ''F'''s domain to ordinals <{{Hair space}}''α''.

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 ''g''<sub>1</sub>, and class functions ''G''<sub>2</sub>, ''G''<sub>3</sub>, there exists a unique function ''F'': Ord → ''V'' such that
* ''F''(0) = ''g''<sub>1</sub>,
* ''F''(''α'' + 1) = ''G''<sub>2</sub>(''F''(''α'')), for all ''α'' ∈ Ord,
* <math>F(\lambda) = G_3(F \upharpoonright \lambda)</math>, for all limit ''λ'' ≠ 0.

Note that we require the domains of ''G''<sub>2</sub>, ''G''<sub>3</sub> to be broad enough to make the above properties meaningful.  The uniqueness of the sequence satisfying these properties can be proved using transfinite induction.

More generally, one can define objects by transfinite recursion on any [[well-founded relation]] ''R''. (''R'' need not even be a set; it can be a [[proper class]], provided it is a [[binary relation#set-like-relation|set-like relation]]; i.e. for any ''x'', the collection of all ''y'' such that ''yRx'' is a set.)