[proofplan] We transfer the proofs of $\in$-induction and $\in$-recursion to an arbitrary well-founded, local relation-class $R$. The two hypotheses play precisely these roles: **well-foundedness** replaces the Axiom of Foundation in the base case of induction (every non-empty class has an $R$-minimal element), and **locality** — the condition that for every set $x$ the class $\{y : y \mathrel{R} x\}$ of $R$-predecessors is a set — replaces transitivity and Replacement in the construction of the set-sized closure $TC_R(\{x\})$ under $R$-predecessors. Once these substitutions are made, the proofs from the $\in$ case carry over verbatim. [/proofplan] [step:Define the $R$-closure of a set and verify it is a set] For a set $x$, define the **$R$-closure** $TC_R(\{x\})$ to be the smallest class $C$ such that $x \in C$ and, for every $z \in C$, every $R$-predecessor of $z$ also lies in $C$. [claim:$R$-closure is a set] If $R$ is local, then $TC_R(\{x\})$ is a set for every set $x$. [/claim] [proof] Define inductively \begin{align*} C_0 &:= \{x\}, \\ C_{n+1} &:= C_n \cup \bigcup_{z \in C_n} \{y : y \mathrel{R} z\}, \quad n \in \mathbb{N}. \end{align*} By locality, $\{y : y \mathrel{R} z\}$ is a set for each $z$. Replacement applied to $C_n$ and the function-class $z \mapsto \{y : y \mathrel{R} z\}$ yields a set, and Union produces $C_{n+1}$. By induction, each $C_n$ is a set. Replacement on $\mathbb{N}$ with $n \mapsto C_n$, followed by Union, yields the set \begin{align*} TC_R(\{x\}) = \bigcup_{n \in \mathbb{N}} C_n. \end{align*} By construction this class contains $x$ and is closed under $R$-predecessors, and any class with these properties contains every $C_n$ and hence $TC_R(\{x\})$. $\square$ [/proof] [/step] [step:Prove $R$-induction using well-foundedness] [claim:$R$-Induction] Let $\varphi$ be a class formula. If $(\forall z \mathrel{R} y\, \varphi(z)) \implies \varphi(y)$ holds for every set $y$, then $\varphi(y)$ holds for every set $y$. [/claim] [proof] Suppose for contradiction that the hypothesis of the implication holds for every $y$ but there exists $x_0$ with $\neg \varphi(x_0)$. **Restrict to a set.** By the previous step, $TC_R(\{x_0\})$ is a set. Define \begin{align*} A := \{z \in TC_R(\{x_0\}) : \neg \varphi(z)\}. \end{align*} $A$ is a set (by Separation) and is non-empty because $x_0 \in A$. **Apply well-foundedness.** Since $R$ is well-founded, every non-empty set has an $R$-minimal element: there exists $y \in A$ such that no $z \in A$ satisfies $z \mathrel{R} y$. By definition of $A$, this means: for every $z \mathrel{R} y$ with $z \in TC_R(\{x_0\})$, $\varphi(z)$ holds. **Every $R$-predecessor of $y$ lies in $TC_R(\{x_0\})$.** Since $y \in TC_R(\{x_0\})$ and $TC_R(\{x_0\})$ is closed under $R$-predecessors, every $z$ with $z \mathrel{R} y$ satisfies $z \in TC_R(\{x_0\})$. Combining with the previous point, $\varphi(z)$ holds for every $z \mathrel{R} y$. **Contradiction.** By the inductive hypothesis, $(\forall z \mathrel{R} y\, \varphi(z)) \implies \varphi(y)$, so $\varphi(y)$ holds. But $y \in A$ means $\neg \varphi(y)$, contradiction. $\square$ [/proof] [guided] Why does well-foundedness suffice to replace Foundation? The Axiom of Foundation says exactly that the $\in$-relation is well-founded on every non-empty set: every non-empty set $A$ contains an element $y$ with no $z \in A$ satisfying $z \in y$. Our hypothesis says the same for $R$. So the inductive argument proceeds identically, **provided** the $R$-minimal element argument can be applied to a set. This is where locality enters: we need to cut the universe down to a set before we can apply well-foundedness. Why do we restrict to $TC_R(\{x_0\})$ rather than to some other set? Because two properties are needed for the argument: 1. $TC_R(\{x_0\})$ contains the counterexample $x_0$ (so $A$ is non-empty). 2. $TC_R(\{x_0\})$ is closed under $R$-predecessors (so the $R$-minimal $y \in A$ has all its $R$-predecessors inside $TC_R(\{x_0\})$, where we know $\varphi$ holds). The $R$-closure is the minimal class with these two properties, and locality is exactly what makes it a set. Without locality, $TC_R(\{x_0\})$ could be a proper class and the application of well-foundedness (which requires a set) would fail. [/guided] [/step] [step:Prove $R$-recursion by the same attempt construction] [claim:$R$-Recursion] Let $G$ be a function-class defined on all sets. Then there exists a unique function-class $F$ such that \begin{align*} F(x) = G(F|_{R,\, x}) \quad \text{for all sets } x, \end{align*} where $F|_{R,\, x} := \{(y, F(y)) : y \mathrel{R} x\}$. [/claim] [proof] The proof parallels the $\in$-Recursion Theorem verbatim, with three substitutions: **Substitution 1: $F|_{R,\, x}$ is a set.** For fixed $x$, the collection $\{y : y \mathrel{R} x\}$ is a set by locality. Replacement applied to this set and the function-class $y \mapsto (y, F(y))$ yields the set $F|_{R,\, x}$. Hence $G(F|_{R,\, x})$ is well-defined. **Substitution 2: attempts have $R$-closed domains.** Call $f$ an **$R$-attempt** if $\operatorname{dom} f$ is a set closed under $R$-predecessors (meaning: $y \in \operatorname{dom} f$ and $z \mathrel{R} y$ imply $z \in \operatorname{dom} f$) and $f(y) = G(f|_{R,\, y})$ for every $y \in \operatorname{dom} f$. The role previously played by transitive domains is now played by $R$-closed domains. **Substitution 3: arguments use $R$-induction and $TC_R$ in place of $\in$-induction and $TC$.** *Agreement of attempts.* If $f$ and $f'$ are $R$-attempts, then $f(y) = f'(y)$ for every $y \in \operatorname{dom} f \cap \operatorname{dom} f'$. By $R$-induction (previous claim): fix $y$ and assume $f(z) = f'(z)$ for every $z \mathrel{R} y$ with $z \in \operatorname{dom} f \cap \operatorname{dom} f'$. If $y \in \operatorname{dom} f \cap \operatorname{dom} f'$, then by $R$-closure every $z \mathrel{R} y$ lies in both domains, so the inductive hypothesis gives $f|_{R,\, y} = f'|_{R,\, y}$, and hence \begin{align*} f(y) = G(f|_{R,\, y}) = G(f'|_{R,\, y}) = f'(y). \end{align*} *Existence of attempts.* By $R$-induction: fix $x$ and assume for each $y \mathrel{R} x$ there is an $R$-attempt $f_y$ with $y \in \operatorname{dom} f_y$. For each $y \mathrel{R} x$, let $g_y := f_y|_{TC_R(\{y\})}$. The set $TC_R(\{y\})$ is $R$-closed and a set by the first step, so $g_y$ is an $R$-attempt. By agreement, the union \begin{align*} f := \bigcup_{y \mathrel{R} x} g_y \end{align*} is a well-defined function with $R$-closed domain $TC_R(\{y : y \mathrel{R} x\})$. The extension \begin{align*} f' := f \cup \{(x, G(f|_{R,\, x}))\} \end{align*} has domain $\operatorname{dom} f \cup \{x\}$, which is $R$-closed (the $R$-predecessors of $x$ are exactly the indices $y$, which lie in $\operatorname{dom} f$), and satisfies the recursion equation everywhere, including at $x$ itself. Hence $f'$ is an $R$-attempt with $x \in \operatorname{dom} f'$. *Definition of $F$ and uniqueness.* Define $F(x)$ to be the common value $f(x)$ over all $R$-attempts $f$ with $x \in \operatorname{dom} f$; this is well-defined by agreement and total by existence. Uniqueness of $F$ follows by $R$-induction: if $F_1$ and $F_2$ both satisfy the recursion, then $F_1(y) = F_2(y)$ for every $y \mathrel{R} x$ implies $F_1|_{R,\, x} = F_2|_{R,\, x}$, hence $F_1(x) = F_2(x)$. $\square$ [/proof] [/step] [step:Conclude that $R$-induction and $R$-recursion hold] Combining the two claims, we have shown that both $R$-induction and $R$-recursion are valid whenever $R$ is a well-founded and local relation-class. The hypotheses are used as follows: **locality** ensures that $R$-predecessor classes and $R$-closures are sets (making Replacement and Separation applicable), and **well-foundedness** ensures that every non-empty set has an $R$-minimal element (driving the base case of induction). This completes the proof. $\square$ [/step]