[proofplan] The naive definition — "set $f(\min X) = G(\varnothing)$, then extend" — is circular: it uses the very recursion principle we are trying to prove. The rigorous approach is to define an **attempt** to be a function $h: I \to Y$, with $I$ an initial segment of $X$, satisfying the recursion equation $h(x) = G(h|_{I_x})$ on its domain. Two [Principle of Transfinite Induction](/theorems/1463) arguments then do the work: first, any two attempts agree on the overlap of their domains, so attempts "glue"; second, every $x \in X$ lies in the domain of some attempt. The union of all attempts is the required function $f$, and uniqueness falls out of the agreement lemma applied to any two candidates. [/proofplan]

[step:Define attempts and state the goal] Given data $(X, <)$ a well-ordered set, $Y$ a set, and $G: \mathcal{P}(X \times Y) \to Y$ a function, recall $I_x := \{y \in X : y < x\}$. For $I \subseteq X$, call $I$ an *initial segment* (not necessarily proper) if $I = X$ or $I = I_x$ for some $x$, or more generally if $y \in I$ and $z < y$ imply $z \in I$. Define an **attempt** to be a pair $(I, h)$ where $I \subseteq X$ is an initial segment and \begin{align*} h: I \to Y \end{align*} satisfies $h(x) = G(h|_{I_x})$ for every $x \in I$. We abuse notation and refer to the attempt by $h$ alone when $I = \operatorname{dom}(h)$ is understood. The strategy is: (i) show any two attempts agree on the common part of their domains; (ii) show every $x \in X$ lies in the domain of some attempt; (iii) glue all attempts together into a single function $f: X \to Y$ and check it satisfies the recursion equation; (iv) verify uniqueness. [/step]

[step:Prove the Agreement Lemma — any two attempts coincide on the overlap of their domains][claim:Agreement of attempts] If $(I, h)$ and $(I', h')$ are attempts, then $h(x) = h'(x)$ for every $x \in I \cap I'$. [/claim] [proof] Let $S := \{x \in X : x \in I \cap I' \text{ implies } h(x) = h'(x)\}$. We show $S = X$ by applying the [Principle of Transfinite Induction](/theorems/1463) to $(X, <)$ and $S$. Fix $x \in X$ and suppose $\{y \in X : y < x\} \subseteq S$, i.e. $h(y) = h'(y)$ for every $y < x$ that lies in $I \cap I'$. We show $x \in S$. If $x \notin I \cap I'$, the implication defining membership in $S$ is vacuously true, so $x \in S$. If $x \in I \cap I'$, then since $I$ and $I'$ are initial segments, $I_x \subseteq I$ and $I_x \subseteq I'$, so $I_x \subseteq I \cap I'$. The inductive hypothesis gives $h(y) = h'(y)$ for all $y \in I_x$, so the restrictions agree: \begin{align*} h|_{I_x} = h'|_{I_x}. \end{align*} Both $h$ and $h'$ are attempts, so they satisfy the recursion equation at $x$: \begin{align*} h(x) = G(h|_{I_x}) = G(h'|_{I_x}) = h'(x). \end{align*} Hence $x \in S$. By the [Principle of Transfinite Induction](/theorems/1463), $S = X$, proving the claim. [/proof][/step]

[guided]We want to show any two attempts $h$ and $h'$ agree wherever both are defined. The natural tool is the [Principle of Transfinite Induction](/theorems/1463): define \begin{align*} S := \{x \in X : x \in I \cap I' \Rightarrow h(x) = h'(x)\} \end{align*} and show $S = X$. To apply transfinite induction, we must verify: for every $x \in X$, if every $y < x$ lies in $S$, then $x \in S$. Fix such an $x$ and assume the inductive hypothesis holds. **Case $x \notin I \cap I'$.** The implication "$x \in I \cap I' \Rightarrow \ldots$" is vacuously true, so $x \in S$. **Case $x \in I \cap I'$.** We must show $h(x) = h'(x)$. Because $I$ and $I'$ are initial segments, they are downward-closed: $x \in I$ forces every $y < x$ to lie in $I$, and similarly for $I'$. Therefore $I_x \subseteq I \cap I'$. For every $y \in I_x$, the inductive hypothesis (applied to that $y$, which is strictly below $x$) gives $y \in S$, and since $y \in I \cap I'$ the implication yields $h(y) = h'(y)$. Thus $h|_{I_x} = h'|_{I_x}$. Now both $h$ and $h'$ are *attempts*, meaning they satisfy the recursion equation at every point of their domain. In particular, at $x \in I \cap I'$ both $h$ and $h'$ obey \begin{align*} h(x) = G(h|_{I_x}), \qquad h'(x) = G(h'|_{I_x}). \end{align*} Since $h|_{I_x} = h'|_{I_x}$ and $G$ is a function, $G(h|_{I_x}) = G(h'|_{I_x})$, so $h(x) = h'(x)$ and $x \in S$. This completes the inductive step. The [Principle of Transfinite Induction](/theorems/1463) now concludes $S = X$, which is exactly the claimed agreement statement.[/guided]

[step:Prove the Existence Lemma — every $x \in X$ lies in the domain of some attempt][claim:Existence of attempts covering $X$] For every $x \in X$, there is an attempt $(I, h)$ with $x \in I$. [/claim] [proof] Let \begin{align*} T := \{x \in X : x \in I \text{ for some attempt } (I, h)\}. \end{align*} We show $T = X$ by transfinite induction. Fix $x \in X$ and suppose every $y < x$ belongs to $T$; that is, for each $y < x$ there is an attempt $(I_y, h_y)$ with $y \in I_y$. We construct an attempt whose domain contains $x$. Define \begin{align*} h': I_x &\to Y \\ y &\mapsto h_y(y). \end{align*} We verify that $h'$ is well-defined: if $y \in I_x$ with $y < x$, then two choices of attempt at $y$, say $(I_y, h_y)$ and $(I_{y'}, h_{y'})$ (for the same $y$), satisfy $y \in I_y \cap I_{y'}$, so by the Agreement Lemma $h_y(y) = h_{y'}(y)$. Hence $h'(y)$ does not depend on which attempt we chose. Next, we check $h'$ is itself an attempt on the initial segment $I_x$. Given $z \in I_x$, the attempt $(I_z, h_z)$ at $z$ satisfies $h_z(z) = G(h_z|_{I_z})$. For any $w \in I_z$, we have $w < z < x$, so $w \in I_x$. The attempt $(I_w, h_w)$ at $w$ satisfies $w \in I_w$, and both $h_z$ and $h_w$ are attempts with $w \in I_z \cap I_w$, so by the Agreement Lemma $h_z(w) = h_w(w) = h'(w)$. Hence $h_z|_{I_z} = h'|_{I_z}$, and \begin{align*} h'(z) = h_z(z) = G(h_z|_{I_z}) = G(h'|_{I_z}). \end{align*} Thus $h'$ satisfies the recursion equation on $I_x$, so $(I_x, h')$ is an attempt. Finally, extend $h'$ to $I := I_x \cup \{x\}$ by setting $h(x) := G(h'|_{I_x}) = G(h')$, with $h|_{I_x} := h'$. Then $I$ is an initial segment (as $I_x$ is one and we have added the immediate successor $x$), and $h$ satisfies the recursion at every point of $I$: on $I_x$ by the previous paragraph, and at $x$ by construction since $h|_{I_x} = h'$. Hence $(I, h)$ is an attempt containing $x$, so $x \in T$. By the [Principle of Transfinite Induction](/theorems/1463), $T = X$. [/proof][/step]

[guided]We want to show that every $x \in X$ is covered by some attempt. Define \begin{align*} T := \{x \in X : \text{some attempt has } x \text{ in its domain}\} \end{align*} and apply the [Principle of Transfinite Induction](/theorems/1463). Fix $x \in X$ and assume every $y < x$ lies in $T$. We must build an attempt containing $x$. For each $y < x$, choose (using the inductive hypothesis) an attempt $(I_y, h_y)$ with $y \in I_y$. The idea is to glue these attempts together, then extend one step further to include $x$. **Step A: glue attempts on $I_x$.** Define $h': I_x \to Y$ by $h'(y) := h_y(y)$. *Is $h'$ well-defined?* A priori, two different choices of attempt at the same point $y$ might disagree. But the **Agreement Lemma** of the previous step guarantees that any two attempts agree on the intersection of their domains. If we chose two attempts $(I_y, h_y)$ and $(I_{y'}, h_{y'})$ both containing $y$, they agree at $y$, so the value $h'(y)$ is unambiguous. *Is $h'$ an attempt?* We must check $h'(z) = G(h'|_{I_z})$ for every $z \in I_x$. Fix such $z$. The attempt $(I_z, h_z)$ satisfies $h_z(z) = G(h_z|_{I_z})$ by the attempt property. To replace $h_z|_{I_z}$ with $h'|_{I_z}$, we use the Agreement Lemma again: for each $w \in I_z$ the attempts $h_z$ and $h_w$ both contain $w$, so $h_z(w) = h_w(w) = h'(w)$. Hence $h_z|_{I_z} = h'|_{I_z}$, and \begin{align*} h'(z) = h_z(z) = G(h_z|_{I_z}) = G(h'|_{I_z}). \end{align*} So $(I_x, h')$ is an attempt. **Step B: extend by one step to cover $x$.** Let $I := I_x \cup \{x\}$ and define \begin{align*} h: I \to Y, \qquad h(y) := \begin{cases} h'(y) & y \in I_x \\ G(h') & y = x \end{cases} \end{align*} Note $G(h')$ is shorthand for $G(h'|_{I_x}) = G(h')$ since $\operatorname{dom}(h') = I_x$. *Is $I$ an initial segment?* $I_x$ is an initial segment, and adding $x$ — the supremum-like successor defining $I_x$ — keeps this property: if $w < z$ and $z \in I$, either $z \in I_x$ (so $w \in I_x \subseteq I$) or $z = x$ (so $w < x$, giving $w \in I_x \subseteq I$). *Is $h$ an attempt?* For $z \in I_x$, $h(z) = h'(z) = G(h'|_{I_z}) = G(h|_{I_z})$ since $h$ and $h'$ agree on $I_x \supseteq I_z$. For $z = x$, $h(x) = G(h') = G(h|_{I_x})$ by definition. Hence $h$ satisfies the recursion equation on all of $I$. Thus $(I, h)$ is an attempt containing $x$, so $x \in T$, completing the inductive step. Transfinite induction yields $T = X$.[/guided]

[step:Define $f$ as the union of all attempts and check it satisfies the recursion] By the Existence Lemma, for every $x \in X$ there is an attempt $(I, h)$ with $x \in I$. Define \begin{align*} f: X &\to Y \\ x &\mapsto h(x) \text{ for any attempt } (I, h) \text{ with } x \in I. \end{align*} By the Agreement Lemma, $f(x)$ does not depend on the choice of attempt, so $f$ is well-defined. To verify the recursion equation, fix $x \in X$. Choose an attempt $(I, h)$ with $x \in I$; by downward closure of $I$, we also have $I_x \subseteq I$, so $h$ is defined on $I_x$. For every $y \in I_x$, $y \in I$, hence $f(y) = h(y)$, so $f|_{I_x} = h|_{I_x}$. Since $h$ is an attempt, \begin{align*} f(x) = h(x) = G(h|_{I_x}) = G(f|_{I_x}). \end{align*} This holds for every $x \in X$. [/step]

[step:Prove uniqueness by applying the Agreement Lemma to two candidates]Suppose $f, \tilde{f}: X \to Y$ both satisfy $f(x) = G(f|_{I_x})$ and $\tilde{f}(x) = G(\tilde{f}|_{I_x})$ for all $x \in X$. Then $(X, f)$ and $(X, \tilde{f})$ are both attempts in the sense of Step 1 (the domain $X$ is an initial segment of itself). By the Agreement Lemma applied to these two attempts, $f(x) = \tilde{f}(x)$ for every $x \in X \cap X = X$. Hence $f = \tilde{f}$. Combining existence (Steps 3–4) with uniqueness, there is a unique function $f: X \to Y$ satisfying the recursion equation, completing the proof.[/step]

[guided]We establish uniqueness by reducing it to the Agreement Lemma already proved. Suppose $f$ and $\tilde{f}$ are any two functions $X \to Y$ satisfying the recursion equation \begin{align*} f(x) = G(f|_{I_x}), \qquad \tilde{f}(x) = G(\tilde{f}|_{I_x}) \qquad \text{for all } x \in X. \end{align*} The whole of $X$ is an initial segment of itself: every element $y < x$ of any $x \in X$ still lies in $X$. Hence $(X, f)$ and $(X, \tilde{f})$ are both attempts by the definition in Step 1. The **Agreement Lemma** applied to these two attempts gives $f(x) = \tilde{f}(x)$ on the overlap of their domains, which is $X \cap X = X$. Therefore $f = \tilde{f}$ pointwise, completing the uniqueness proof. Combined with the existence proof in the previous steps, this establishes the existence of a **unique** function $f: X \to Y$ satisfying the recursion equation, which is the content of the theorem. **Why is the attempt-based approach necessary?** The naive "define $f(\min X) = G(\varnothing)$, then proceed upward" seems intuitive but is circular: what does "proceed upward" mean when $X$ has no successor structure (e.g. $X$ contains limit points like $\omega$)? At a limit point $\lambda$, there is no immediate predecessor to extend from, and the naive approach cannot specify $f(\lambda)$ without already having $f$ defined on all of $I_\lambda$ — which is exactly what we are trying to build. The attempt formalism sidesteps this by asserting the *existence* of partial solutions and showing they are compatible and exhaustive; the recursion is then a consequence of gluing rather than iterated construction.[/guided]