# 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

 $F(x)=G(x,F|\operatorname{seg}(x)),$

where $\operatorname{seg}(x):=\{y\in A\mid yRx\}$, the initial segment of $x$.

Remark. Since every well-ordered set is well-founded, the well-founded recursion theorem is a generalization 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 $\operatorname{seg}(a)=\operatorname{seg}(b)$ for $a\neq b$ in a well-founded set.

By converting $G$ into a formula ($\varphi(x,y,z)$ such that for all $x,y$, there is a unique $z$ such that $\varphi(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 WellfoundedRecursion 2013-03-22 17:54:52 2013-03-22 17:54:52 CWoo (3771) CWoo (3771) 8 CWoo (3771) Theorem msc 03E10 msc 03E45 TransfiniteRecursion