[proofplan] We prove uniqueness first by [well-founded induction](/theorems/4797) on the class relation $R$. For existence, we construct for each $a \in A$ a local solution on the set of all predecessors of $a$ generated by finitely many backward $R$-steps; set-likeness makes this closure a set, so ordinary set construction applies inside it. We then show by well-founded induction that any two local solutions agree wherever their domains overlap, allowing the local values to patch into a single class function on $A$. [/proofplan]

[step:Prove that any two recursive class functions agree on all elements of $A$]Let \begin{align*} F_0:A &\to V,\\ F_1:A &\to V \end{align*} be class functions satisfying \begin{align*} F_i(a)=G(a,F_i|_{P_a}) \end{align*} for every $a \in A$ and each $i \in \{0,1\}$. Define the disagreement class \begin{align*} D:=\{a \in A : F_0(a) \ne F_1(a)\}. \end{align*} Suppose, for contradiction, that $D$ is nonempty. Since $R$ is well-founded on $A$, there exists $a_0 \in D$ such that no element of $D$ is an $R$-predecessor of $a_0$. Thus for every $b \in P_{a_0}$ we have $F_0(b)=F_1(b)$, and hence \begin{align*} F_0|_{P_{a_0}} = F_1|_{P_{a_0}}. \end{align*} Both restrictions are set functions $P_{a_0}\to V$ because $P_{a_0}$ is a set and $F_0,F_1$ are class functions into $V$. Therefore \begin{align*} F_0(a_0) &=G(a_0,F_0|_{P_{a_0}})\\ &=G(a_0,F_1|_{P_{a_0}})\\ &=F_1(a_0), \end{align*} contradicting $a_0 \in D$. Hence $D=\varnothing$, so $F_0=F_1$.[/step]

[guided]The uniqueness argument is the standard minimal-counterexample argument for a well-founded relation. Assume there are two solutions \begin{align*} F_0:A &\to V,\\ F_1:A &\to V \end{align*} satisfying the same recursion rule. We want to prove that they agree everywhere, so we isolate the possible failures by defining \begin{align*} D:=\{a \in A : F_0(a) \ne F_1(a)\}. \end{align*} If $D$ were nonempty, well-foundedness of $R$ would give an $R$-minimal disagreement $a_0 \in D$: no predecessor of $a_0$ lies in $D$. This means that for every $b \in A$ with $bRa_0$, the two functions agree at $b$. Since \begin{align*} P_{a_0}:=\{b \in A : bRa_0\}, \end{align*} we obtain \begin{align*} F_0|_{P_{a_0}} = F_1|_{P_{a_0}}. \end{align*} The set-like hypothesis is used here: $P_{a_0}$ is a set, so each restriction $F_i|_{P_{a_0}}$ is a legitimate set function from $P_{a_0}$ to $V$, hence a valid input to $G$. Applying the recursive identity for both $F_0$ and $F_1$ gives \begin{align*} F_0(a_0) &=G(a_0,F_0|_{P_{a_0}})\\ &=G(a_0,F_1|_{P_{a_0}})\\ &=F_1(a_0). \end{align*} This contradicts the choice of $a_0$ as a point of disagreement. Therefore no disagreement exists, and the recursive class function is unique.[/guided]

[step:Build a set of all finite predecessors of a fixed element]Fix $a \in A$. Let $\mathbb{N}:=\{1,2,3,\dots\}$ denote the set of positive integers. Define subsets $S_n(a)$ of $A$ by recursion on $n \in \mathbb{N}$, with $S_1(a):=\{a\}$ and \begin{align*} S_{n+1}(a):=S_n(a)\cup \bigcup_{x\in S_n(a)}P_x. \end{align*} Because $S_1(a)$ is a set and each $P_x$ is a set, induction on $n$ shows that every $S_n(a)$ is a set. Define \begin{align*} S(a):=\bigcup_{n=1}^{\infty}S_n(a). \end{align*} The sequence $n\mapsto S_n(a)$ is a set-indexed family by ordinary recursion on $\mathbb{N}$, and its range is a set by Replacement. Therefore $S(a)$ is a set by the Union axiom. Moreover, $a\in S(a)$, and $S(a)$ is closed under predecessors: if $x\in S(a)$ and $yRx$, then $y\in S(a)$. Indeed, if $x\in S(a)$, then $x\in S_n(a)$ for some $n\in\mathbb{N}$; since $yRx$, we have $y\in P_x\subset S_{n+1}(a)\subset S(a)$.[/step]

[guided]To construct the value of the recursive function near a fixed element $a$, we first gather every element whose value can influence $F(a)$ through finitely many recursive calls. Define \begin{align*} S_1(a):=\{a\} \end{align*} and then recursively set \begin{align*} S_{n+1}(a):=S_n(a)\cup \bigcup_{x\in S_n(a)}P_x. \end{align*} Thus $S_2(a)$ contains $a$ and its immediate predecessors, $S_3(a)$ also contains predecessors of those predecessors, and so on. We verify that each $S_n(a)$ is a set. The initial set $S_1(a)=\{a\}$ is a set. If $S_n(a)$ is a set, then for each $x\in S_n(a)$ the predecessor class $P_x$ is a set by set-likeness of $R$. Therefore the union \begin{align*} \bigcup_{x\in S_n(a)}P_x \end{align*} is a set, and hence $S_{n+1}(a)$ is a set. By induction, all $S_n(a)$ are sets. Now define \begin{align*} S(a):=\bigcup_{n=1}^{\infty}S_n(a). \end{align*} This is a countable union of sets, so it is a set. The important structural property of $S(a)$ is predecessor-closure. Suppose $x\in S(a)$ and $yRx$. Choose $n\in\mathbb{N}$ with $x\in S_n(a)$. Since $yRx$, we have $y\in P_x$, and by the definition of $S_{n+1}(a)$ this implies \begin{align*} y\in P_x\subset S_{n+1}(a)\subset S(a). \end{align*} Thus every predecessor needed to compute a value inside $S(a)$ also lies inside $S(a)$.[/guided]

[step:Construct the unique local recursive function on each predecessor closure]For the fixed $a\in A$, let $R_a$ denote the restriction of $R$ to $S(a)$: \begin{align*} R_a:=R\cap (S(a)\times S(a)). \end{align*} Since $R$ is well-founded on $A$, the relation $R_a$ is well-founded on the set $S(a)$. Define the local recursion operator $G_a$ as the class function which assigns to each pair $(x,h)$, where $x\in S(a)$ and $h:P_x\to V$ is a set function, the value \begin{align*} G_a(x,h):=G(x,h). \end{align*} This operator is legitimate because predecessor-closure gives $P_x\subset S(a)$ for every $x\in S(a)$, and set-likeness gives that $P_x$ is a set. Applying the ordinary well-founded recursion theorem for set relations to the set $S(a)$, the well-founded relation $R_a$, and the operator $G_a$, there exists a unique set function \begin{align*} f_a:S(a)\to V \end{align*} such that, for every $x\in S(a)$, \begin{align*} f_a(x)=G_a(x,f_a|_{P_x})=G(x,f_a|_{P_x}). \end{align*} The theorem applies because $S(a)$ is a set, $R_a$ is well-founded on $S(a)$, and each predecessor set for $R_a$ is exactly $P_x$ since $S(a)$ is predecessor-closed.[/step]

[guided]Now that $S(a)$ is a set and contains all predecessors of its elements, the recursion can be performed by the ordinary well-founded recursion theorem for set relations. Let \begin{align*} R_a:=R\cap (S(a)\times S(a)) \end{align*} be the restricted relation. Since every nonempty subset of $S(a)$ is also a nonempty subclass of $A$, the well-foundedness of $R$ implies that $R_a$ is well-founded on the set $S(a)$. We define a local operator $G_a$ by reusing the given class function $G$ on the set domain $S(a)$. Precisely, $G_a$ assigns to each pair $(x,h)$, where $x\in S(a)$ and $h:P_x\to V$ is a set function, the value \begin{align*} G_a(x,h):=G(x,h). \end{align*} This definition has the correct input type. If $x\in S(a)$ and $yRx$, predecessor-closure gives $y\in S(a)$, so the predecessor set of $x$ inside the restricted relation $R_a$ is the same set $P_x$. Set-likeness of $R$ gives that $P_x$ is a set, so a restriction to $P_x$ is a set function and is an admissible second argument for $G$. The ordinary well-founded recursion theorem for set relations now applies to the set $S(a)$, the well-founded relation $R_a$, and the operator $G_a$. It yields a unique set function \begin{align*} f_a:S(a)\to V \end{align*} such that, for every $x\in S(a)$, \begin{align*} f_a(x)=G_a(x,f_a|_{P_x}). \end{align*} Substituting the definition of $G_a$ gives the local recursion formula \begin{align*} f_a(x)=G(x,f_a|_{P_x}) \end{align*} for every $x\in S(a)$. This avoids any partial-construction circularity: the existence and coherence of all predecessor assignments are supplied by the set-level recursion theorem, and uniqueness is part of that same theorem.[/guided]

[step:Show that local recursive functions agree on overlaps]Let $a,c\in A$. We prove that \begin{align*} f_a(x)=f_c(x) \end{align*} for every $x\in S(a)\cap S(c)$. Let \begin{align*} E:=\{x\in S(a)\cap S(c): f_a(x)\ne f_c(x)\}. \end{align*} If $E$ were nonempty, well-foundedness of $R$ would give an $R$-minimal element $x_0\in E$. For every $y\in P_{x_0}$, predecessor-closure of both $S(a)$ and $S(c)$ gives $y\in S(a)\cap S(c)$, and minimality gives $f_a(y)=f_c(y)$. Hence \begin{align*} f_a|_{P_{x_0}}=f_c|_{P_{x_0}}. \end{align*} Using the local recursion for $f_a$ and $f_c$ at $x_0$, \begin{align*} f_a(x_0) &=G(x_0,f_a|_{P_{x_0}})\\ &=G(x_0,f_c|_{P_{x_0}})\\ &=f_c(x_0), \end{align*} contradicting $x_0\in E$. Therefore $E=\varnothing$.[/step]

[guided]The local functions must be compatible before they can be patched. Fix $a,c\in A$. We compare \begin{align*} f_a:S(a)\to V \end{align*} and \begin{align*} f_c:S(c)\to V \end{align*} on the overlap $S(a)\cap S(c)$. Define the possible disagreement set \begin{align*} E:=\{x\in S(a)\cap S(c): f_a(x)\ne f_c(x)\}. \end{align*} If $E$ is nonempty, well-foundedness of $R$ gives an $R$-minimal element $x_0\in E$. Now take any $y\in P_{x_0}$. Since $x_0\in S(a)$ and $S(a)$ is predecessor-closed, $y\in S(a)$. Since $x_0\in S(c)$ and $S(c)$ is predecessor-closed, $y\in S(c)$. Hence $y\in S(a)\cap S(c)$. Minimality of $x_0$ in $E$ then implies \begin{align*} f_a(y)=f_c(y). \end{align*} Therefore the two predecessor restrictions agree: \begin{align*} f_a|_{P_{x_0}}=f_c|_{P_{x_0}}. \end{align*} Both local functions satisfy the same recursion rule at $x_0$, so \begin{align*} f_a(x_0) &=G(x_0,f_a|_{P_{x_0}})\\ &=G(x_0,f_c|_{P_{x_0}})\\ &=f_c(x_0). \end{align*} This contradicts $x_0\in E$. Therefore there is no disagreement on the overlap, and the local recursive functions are compatible.[/guided]

[step:Patch the compatible local functions into the required class function]Define a class relation $\Gamma$ on $A\times V$ by declaring that $(x,v)\in\Gamma$ if and only if there exists $a\in A$ such that $x\in S(a)$ and $f_a(x)=v$. The constructions $a\mapsto S(a)$ and $a\mapsto f_a$ are uniform: $S(a)$ is defined by the displayed recursion on $\mathbb{N}$ from the parameter $a$, and $f_a$ is the unique set function on $S(a)$ satisfying the displayed local recursion. Hence this condition is a class formula with parameters $R$, $G$, $A$, and $V$. For each $x\in A$, there is at least one $v\in V$ with $(x,v)\in\Gamma$, because $x\in S(x)$ and $f_x(x)\in V$. There is at most one such $v$: if $(x,v_0),(x,v_1)\in\Gamma$, choose $a,c\in A$ with $x\in S(a)\cap S(c)$, $v_0=f_a(x)$, and $v_1=f_c(x)$; the previous step gives $f_a(x)=f_c(x)$, so $v_0=v_1$. Therefore $\Gamma$ is the graph of a class function \begin{align*} F:A\to V. \end{align*} Equivalently, whenever $x\in S(a)$, the value of this class function is \begin{align*} F(x)=f_a(x). \end{align*} Fix $x\in A$. Since $P_x\subset S(x)$, the definition of $F$ and compatibility of the local functions give \begin{align*} F|_{P_x}=f_x|_{P_x}. \end{align*} Using the local recursion for $f_x$ at $x$, \begin{align*} F(x) &=f_x(x)\\ &=G(x,f_x|_{P_x})\\ &=G(x,F|_{P_x}). \end{align*} Thus $F$ satisfies the recursion equation for every $x\in A$. The uniqueness proved in the first step shows that this $F$ is the unique class function $A\to V$ satisfying the stated rule.[/step]

[guided]We now define the global function by its graph, which is the point at which class-level uniformity matters. Let $\Gamma$ be the class relation on $A\times V$ defined by \begin{align*} (x,v)\in\Gamma \end{align*} if and only if there exists $a\in A$ such that $x\in S(a)$ and $f_a(x)=v$. This is a class definition because the construction of $S(a)$ is given uniformly from $a$ by recursion on $\mathbb{N}$, and $f_a$ is identified uniformly as the unique set function on $S(a)$ satisfying the local recursion. For every $x\in A$, existence of a value follows from $x\in S(x)$: the local function $f_x:S(x)\to V$ gives $(x,f_x(x))\in\Gamma$. To prove uniqueness of the value, suppose $(x,v_0),(x,v_1)\in\Gamma$. Then there are $a,c\in A$ such that $x\in S(a)\cap S(c)$, $v_0=f_a(x)$, and $v_1=f_c(x)$. The compatibility result on overlaps gives \begin{align*} f_a(x)=f_c(x), \end{align*} so $v_0=v_1$. Thus $\Gamma$ is single-valued and total on $A$, hence it is the graph of a class function \begin{align*} F:A\to V. \end{align*} When $x\in S(a)$, this function satisfies $F(x)=f_a(x)$ by definition of $\Gamma$. It remains to verify the recursive identity. Fix $x\in A$. Since $S(x)$ is predecessor-closed, every $y\in P_x$ lies in $S(x)$. On $P_x$, the global function $F$ agrees with the local function $f_x$, so \begin{align*} F|_{P_x}=f_x|_{P_x}. \end{align*} The local recursion for $f_x$ at the point $x$ gives \begin{align*} f_x(x)=G(x,f_x|_{P_x}). \end{align*} Using the definition of $F(x)$ and the equality of restrictions, we obtain \begin{align*} F(x) &=f_x(x)\\ &=G(x,f_x|_{P_x})\\ &=G(x,F|_{P_x}). \end{align*} Thus $F$ satisfies the required recursion equation at every $x\in A$. Finally, the uniqueness step already proved that no two class functions can satisfy this recursion rule. Hence the patched function $F$ is the unique class function $A\to V$ with \begin{align*} F(a)=G(a,F|_{P_a}) \end{align*} for all $a\in A$.[/guided]