- Let $(J, <)$ be a well-ordered set.
- Denote by $[0, \alpha)$ the set $\{ j \in J : j < \alpha \}$ as suggestive notation. Similarly $[0, \alpha]$ is the set $\{ j \in J: j \leq \alpha \}$.
- Let $r: (\forall \alpha \in J, [0, \alpha) \rightarrow O) \rightarrow O$ be a recursion formula, which when given a function $f: [0, \alpha) \rightarrow O$ which is well defined on $J$ upto $\alpha$, produce a value $r(\alpha) \in O$that extends $f$ to be well defined at $\alpha$.
- We wish to find a function $f(j)$ such that for all $j \in J$, $f(j) = r([0, j))$. So this function $f$ is deterined by the recursion principle $r$. We construct such a function by transfinite induction.
- Let $J_0 \subseteq J$ be the set of $j \in J$ such that there exists a function $f_j: [0, j] \rightarrow O$ (see the closed interval!), which obeys the recursion formula upto $j$. That is, for all other $k \leq j$, we have that $f_j(k) = r(f_j|[0, k))$. Choose $k \leq j$ so that we check that $f_j(j) = r(f_j|[0, j))$.
- Claim: the set $J_0$ is inductive.
- Let $[0, j) \subseteq J_0$. Thus, for all $k < j$, there is a function $f_k: [0, k] \rightarrow O$ such that $f_k(l) = r(f_k|[0, l))$.
- We must show that $j \in J_0$. So we must construct a function $f_j: [0, j] \rightarrow O$ such that ... (reader: fill in the blanks).
- Handwavy: note that the set of functions $\{ f_k : k \in [0, j) \}$ all agree on their outputs since their outputs are determined by the recursion formula (Foraal: we can first prove that any function that satisfies the recursion scheme is uniquely defined).
- Thus, we can build the function $g_j: [0, j) \rightarrow O$ given by $g_j \equiv \cup_{k \in [0, j)} f_j$. That is, we literally take the "set union" of the functions as ordered pairs, as the functions are all compatible. This gives us a function defined upto $j$.
- The value of $f_j$ at $j$ must be $r(g_j)$. So we finally define $f_j \equiv g_j \cup \{ (j, r(g_j) \}$. This is a uniquely defined function as $r$ is a function: $r: [0, j) \rightarrow O$ thus produces a unique output for a unique input $g(j)$.
- We have a function $f_j$ that obeys the recursion schema: (1) at $j$, it is defined to obey the recursion schema; At $k < j$, it is written as union of prior $f_k$ which obey recursion schema by transfinite induction hypothesis.
- Thus, we have $j \in J_0$, witnessed by $f_j$.
- We have fulfilled the induction hypothesis. So $J_0 = J$, and we have a set of function $\{ f_j : j \in J \}$, all of which are compatible with each other and obey the recursion schema. We take their unions and define $f \equiv \cup_j f_j$ and we are done!