§ Transfinite recursion: Proof
- Let (J,<) be a well-ordered set.
- Denote by [0,α) the set {j∈J:j<α} as suggestive notation. Similarly [0,α] is the set {j∈J:j≤α}.
- Let r:(∀α∈J,[0,α)→O)→O be a recursion formula, which when given a function f:[0,α)→O which is well defined on J upto α, produce a value r(α)∈Othat extends f to be well defined at α.
- We wish to find a function f(j) such that for all j∈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 J0⊆J be the set of j∈J such that there exists a function fj:[0,j]→O (see the closed interval!), which obeys the recursion formula upto j. That is, for all other k≤j, we have that fj(k)=r(fj∣[0,k)). Choose k≤j so that we check that fj(j)=r(fj∣[0,j)).
- Claim: the set J0 is inductive.
- Let [0,j)⊆J0. Thus, for all k<j, there is a function fk:[0,k]→O such that fk(l)=r(fk∣[0,l)).
- We must show that j∈J0. So we must construct a function fj:[0,j]→O such that ... (reader: fill in the blanks).
- Handwavy: note that the set of functions {fk:k∈[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 gj:[0,j)→O given by gj≡∪k∈[0,j)fj. 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 fj at j must be r(gj). So we finally define fj≡gj∪{(j,r(gj)}. This is a uniquely defined function as r is a function: r:[0,j)→O thus produces a unique output for a unique input g(j).
- We have a function fj 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 fk which obey recursion schema by transfinite induction hypothesis.
- Thus, we have j∈J0, witnessed by fj.
- We have fulfilled the induction hypothesis. So J0=J, and we have a set of function {fj:j∈J}, all of which are compatible with each other and obey the recursion schema. We take their unions and define f≡∪jfj and we are done!