# 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|\mathrm{seg}(x)),$$ |

where $\mathrm{seg}\mathit{}\mathrm{(}x\mathrm{)}\mathrm{:=}\mathrm{\{}y\mathrm{\in}A\mathrm{\mid}y\mathit{}R\mathit{}x\mathrm{\}}$, 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 $\mathrm{seg}(a)=\mathrm{seg}(b)$ for $a\ne b$ in a well-founded set.

By converting $G$ into a formula^{} ($\phi (x,y,z)$ such that for all $x,y$, there is a unique $z$ such that $\phi (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 |