Well-Founded Recursion

Theorem

Let $A$ be a class.

Let $\RR$ be a relation that is strictly well-founded on $A$.

Let every $\RR$-initial segment of any element $x$ of $A$ be a small class.

Let $G$ be a (class) mapping from $A^A$ to $A$.

Let $K$ be a class of mappings $f$ that satisfy:

$(1): \quad$ The domain of $f$ is some subset $y \subseteq A$ such that $y$ is transitive with respect to $\RR$.

$(2): \quad \forall x \in y: \map f x = \map G {f \restriction \RR^{-1} x}$

where $f \restriction R^{-1} x$ denotes the restriction of $f$ to the $\RR$-initial segment of $x$.

Let $F = \bigcup K$, the union of $K$.

Then:

$F$ is a mapping with domain $A$

$\forall x \in A: \map F x = \map G {F \restriction \RR^{-1} x}$

$F$ is unique, in the sense that if another mapping $A$ has the above two properties, then $A = F$.

Proof

This theorem requires a proof. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Sources

• 1971: Gaisi Takeuti and Wilson M. Zaring: Introduction to Axiomatic Set Theory: $\S 9.7$