well-founded recursion

Theorem 1.

Let G be a binary (class) function on V, the class of all sets. Let A be a well-founded set (with R the well-founded relation). Then there is a unique function F such that


where seg(x):={yAyRx}, the initial segment of x.

Remark. Since every well-ordered set is well-founded, the well-founded recursion theorem is a generalizationPlanetmathPlanetmath of the transfinite recursion theorem. Notice that the G here is a function in two arguments, and that it is necessary to specify the element x in the first argument (in contrast with the G in the transfinite recursion theorem), since it is possible that seg(a)=seg(b) for ab in a well-founded set.

By converting G into a formulaMathworldPlanetmathPlanetmath (φ(x,y,z) such that for all x,y, there is a unique z such that φ(x,y,z)), then the above theorem can be proved in ZF (with the aid of the well-founded induction). The proof is similar to the proof of the transfinite recursion theorem.

Title well-founded recursion
Canonical name WellfoundedRecursion
Date of creation 2013-03-22 17:54:52
Last modified on 2013-03-22 17:54:52
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 8
Author CWoo (3771)
Entry type Theorem
Classification msc 03E10
Classification msc 03E45
Related topic TransfiniteRecursion