transfinite recursion

Transfinite recursion, roughly speaking, is a statement about the ability to define a function recursively using transfinite induction. In its most general and intuitive form, it says

Theorem 1.

Let $G$ be a (class) function on $V$, the class of all sets. Then there exists a unique (class) function $F$ on $\mathrm{On}$, the class of ordinals, such that

$$F(\alpha )=G(F|\alpha )$$

where $F\mathrm{|}\alpha$ is the function whose domain is and whose values coincide with $F$ on every $\beta \mathrm{\in }\mathrm{seg}\mathit{}\mathrm{(}\alpha \mathrm{)}$. In other words, $F\mathrm{|}\alpha$ is the restriction of $F$ to $\alpha$.

Notice that the theorem above is not provable in ZF set theory, as $G$ and $F$ are both classes, not sets. In order to prove this statement, one way of getting around this difficulty is to convert both $G$ and $F$ into formulas, and modify the statement, as follows:

Let $\phi (x,y)$ be a formula such that

$$\forall x\exists y\forall z(\phi (x,z)\leftrightarrow z=y).$$

Think of $G=\{(x,y)\mid \phi (x,y)\}$. Then there is a unique formula $\psi (\alpha ,z)$ (think of $F$ as $\{(\alpha ,z)\mid \psi (\alpha ,z)\}$) such that the following two sentences are derivable using ZF axioms:

1. $\forall x\exists y\forall z(\mathrm{𝐎𝐧}(x)\wedge (\psi (x,z)\leftrightarrow z=y)),$ where $\mathrm{𝐎𝐧}(x)$ means “$x$ is an ordinal”,

2. $\forall x\forall y(\mathrm{𝐎𝐧}(x)\wedge (\psi (x,y)\leftrightarrow \exists f(A\wedge B\wedge C\wedge D)))$, where

   • $A$ is the formula “$f$ is a function”,

   • $B$ is the formula “$\mathrm{dom}(f)=x$”,

   • $C$ is the formula $\forall z(z\in x\wedge \phi (f|z,f(z)))$, and

   • $D$ is the formula $\phi (f,y)$.

A stronger form of the transfinite recursion theorem says:

Theorem 2.

Let $\phi \mathit{}\mathrm{(}x\mathrm{,}y\mathrm{)}$ be any formula (in the language of set theory). Then the following is a theorem: assume that $\phi$ satisfies property that, for every $x$, there is a unique $y$ such that $\phi \mathit{}\mathrm{(}x\mathrm{,}y\mathrm{)}$. If $A$ be a well-ordered set (well-ordered by $\mathrm{\le }$), then there is a unique function $f$ defined on $A$ such that

$$\phi (f|\mathrm{seg}(s),f(s))$$

for every $s\mathrm{\in }A$. Here, , the initial segment of $s$ in $A$.

The above theorem is actually a collection of theorems, or known as a theorem schema, where each theorem corresponds to a formula. The other difference between this and the previous theorem is that this theorem is provable in ZF, because the domain of the function $f$ is now a set.