[proofplan] We prove the $\in$-induction schema by contradiction, reducing it to the Axiom of Foundation. The Axiom of Foundation states that every nonempty **set** has an $\in$-minimal element; however, the naive reduction — apply Foundation to $\{x : \neg p(x)\}$ — fails because this class may not be a set. The remedy is to localise the argument: using the [Transitive Closure](/theorems/1493), we form the transitive set $u := TC(\{x_0\})$ containing a hypothetical counter-example $x_0$, then apply Foundation to the set $S := \{y \in u : \neg p(y)\}$, which is a set by Separation. An $\in$-minimal element $y_0$ of $S$ has all its $\in$-predecessors inside $u$ (by transitivity) and satisfying $p$ (by minimality). The inductive hypothesis then forces $p(y_0)$, contradicting $y_0 \in S$. [/proofplan] [step:Fix parameters and assume the induction hypothesis] Fix parameters $t_1, \ldots, t_n$ and assume the **induction hypothesis**: \begin{align*} (\forall x)\bigl[(\forall y)(y \in x \Rightarrow p(y)) \Rightarrow p(x)\bigr]. \tag{$\mathrm{IH}$} \end{align*} Our goal is to prove $(\forall x)\,p(x)$. Suppose for contradiction that this fails: there exists some $x_0$ with \begin{align*} \neg p(x_0). \end{align*} [guided] The structure of the induction schema is: if the local implication "$p$ holds on all $\in$-predecessors of $x$ $\Rightarrow p(x)$" holds **uniformly** for all $x$, then $p$ holds everywhere. In the standard natural-number induction, we prove $(\forall n) p(n)$ by verifying $p(0)$ (the empty-predecessor case) and the inductive step $p(n) \Rightarrow p(n+1)$. Here, instead of the successor structure, we use the membership relation — there is no distinguished "base case" because $\emptyset$ has no $\in$-predecessors, making the local implication vacuous at $\emptyset$ and forcing $p(\emptyset)$ directly. The proof proceeds by contradiction. Assume the induction hypothesis (IH) and suppose there is some witness $x_0$ with $\neg p(x_0)$. We will descend through the $\in$-predecessors of $x_0$ using Foundation to find a **minimal** counterexample, then derive a contradiction at that minimal point. [/guided] [/step] [step:Localise to the transitive closure of $\{x_0\}$] Why not simply apply Foundation to $\{x : \neg p(x)\}$? Because this is a **class**, not in general a set — Foundation applies only to sets. We therefore localise by restricting to a transitive set containing $x_0$. By the [Transitive Closure Theorem](/theorems/1493), there exists a transitive set \begin{align*} u := TC(\{x_0\}) \end{align*} containing $\{x_0\}$; in particular $x_0 \in u$ (since $\{x_0\} \subseteq u$ and transitivity of $u$ together give $\{x_0\} \in u$ is not immediate, but we have $x_0 \in \{x_0\} \subseteq u$, hence $x_0 \in u$). [guided] The key technical difficulty is that the collection \begin{align*} C := \{x : \neg p(x)\} \end{align*} is a **proper class** in general — Russell-type considerations prevent it from being a set. The Axiom of Foundation states that every **nonempty set** has an $\in$-minimal element; it does not apply directly to classes like $C$. To work around this, we cut down to a set. Choose any counterexample $x_0 \in C$ and form the transitive closure $u := TC(\{x_0\})$. Recall (from Theorem 1493) that $TC(\{x_0\})$ is the smallest transitive set containing $\{x_0\}$. Transitivity of $u$ means: if $y \in u$, then $y \subseteq u$. This will be crucial in the next step. Since $x_0 \in \{x_0\} \subseteq u$ (the latter holds because $TC$ adds the elements of $\{x_0\}$ by construction — the iterated-union construction of $TC$ makes the elements of $\{x_0\}$ part of the union), we have $x_0 \in u$. Indeed, the concrete construction of $TC(\{x_0\})$ in Theorem 1493 begins $f(0) = \{x_0\}$, and $\bigcup f(0) = x_0 \in f(1)$, hence $x_0 \in TC(\{x_0\})$. [/guided] [/step] [step:Apply Foundation to the set of counterexamples in $u$] Define \begin{align*} S := \{y \in u : \neg p(y)\}. \end{align*} By the [Axiom Schema of Separation](/theorems/???) applied to the set $u$ and the formula $\neg p(y)$ (with parameters $t_1, \ldots, t_n$), $S$ is a set. Moreover $S \ne \varnothing$ because $x_0 \in u$ and $\neg p(x_0)$, so $x_0 \in S$. By the [Axiom of Foundation](/theorems/???), applied to the nonempty set $S$, there exists an $\in$-minimal element $y_0 \in S$, i.e., \begin{align*} y_0 \in S \quad \text{and} \quad y_0 \cap S = \varnothing. \end{align*} [/step] [step:Show that every $\in$-predecessor of $y_0$ satisfies $p$] Let $z \in y_0$. We show $p(z)$. **$z \in u$:** Since $y_0 \in S \subseteq u$, and $u$ is transitive, $y_0 \subseteq u$. Thus $z \in y_0 \subseteq u$, so $z \in u$. **$\neg(\neg p(z))$:** Since $y_0 \cap S = \varnothing$ (by $\in$-minimality of $y_0$), we cannot have $z \in y_0 \cap S$. But $z \in y_0$, so $z \notin S$. Since $z \in u$, the definition of $S$ gives \begin{align*} z \notin S \iff \neg(z \in u \wedge \neg p(z)) \iff z \notin u \vee p(z). \end{align*} Since $z \in u$, we conclude $p(z)$. Therefore $(\forall z)(z \in y_0 \Rightarrow p(z))$. [guided] We now extract the critical fact from $\in$-minimality. An $\in$-minimal element $y_0$ of $S$ is one for which no member of $y_0$ is itself in $S$ — this is exactly the statement $y_0 \cap S = \varnothing$. Take any $z \in y_0$. We want to show $p(z)$ holds. Two pieces must be combined: **Piece 1 — $z \in u$ (transitivity of $u$).** Since $y_0 \in S \subseteq u$, and $u$ is transitive (any element of $u$ is a subset of $u$), we get $y_0 \subseteq u$, hence every element $z \in y_0$ lies in $u$. **Piece 2 — $z \notin S$ (minimality of $y_0$).** Since $z \in y_0$ and $y_0 \cap S = \varnothing$, $z \notin S$. **Combining:** $S$ was defined as $\{y \in u : \neg p(y)\}$. Being in $u$ but not in $S$ means **not** satisfying the defining property of $S$, i.e., $\neg \neg p(z)$, which is $p(z)$ (by the law of excluded middle, valid in classical first-order logic). This is the heart of the argument: transitivity of $u$ ensures $\in$-predecessors stay in $u$, and $\in$-minimality of $y_0$ ensures they escape $S$. Together, they pin down $p$-validity on all predecessors of $y_0$. [/guided] [/step] [step:Apply the induction hypothesis to conclude $p(y_0)$, contradicting $y_0 \in S$] By Step 4, $(\forall z)(z \in y_0 \Rightarrow p(z))$ holds. Instantiating the induction hypothesis (IH) at $x := y_0$: \begin{align*} \bigl[(\forall z)(z \in y_0 \Rightarrow p(z))\bigr] \Rightarrow p(y_0). \end{align*} The antecedent holds, so $p(y_0)$. But $y_0 \in S = \{y \in u : \neg p(y)\}$, so $\neg p(y_0)$. This is a contradiction. The contradiction was derived from the assumption $\neg (\forall x)\,p(x)$. We therefore conclude $(\forall x)\,p(x)$. Since $t_1, \ldots, t_n$ were arbitrary parameters, this completes the proof of the induction schema. $\square$ [guided] Let us assemble the logical structure: - **Assumed** (IH): "For every $x$, if $p$ holds on all $\in$-predecessors of $x$, then $p(x)$ holds." - **Assumed for contradiction:** there exists $x_0$ with $\neg p(x_0)$. - **Derived** via Foundation on $S = \{y \in u : \neg p(y)\}$: a minimal counterexample $y_0 \in S$. - **Derived** (Step 4): every $z \in y_0$ satisfies $p(z)$. - **Applied (IH) at $y_0$:** since all $\in$-predecessors of $y_0$ satisfy $p$, we get $p(y_0)$. - **But** $y_0 \in S$ means $\neg p(y_0)$. **Contradiction.** The contradiction arose solely from the assumption that some $x_0$ has $\neg p(x_0)$. Therefore no such $x_0$ exists, i.e., $(\forall x)\, p(x)$ holds. Discharging the assumption (IH) and the parameter-quantifiers yields the full schema: \begin{align*} (\forall t_1)\cdots(\forall t_n)\Bigl(\bigl[(\forall x)\bigl((\forall y)(y \in x \Rightarrow p(y))\Rightarrow p(x)\bigr)\bigr] \Rightarrow (\forall x)\,p(x)\Bigr). \end{align*} **Where each axiom entered.** Foundation gave us the minimal element $y_0$ of $S$. Separation gave us $S$ as a set from the transitive set $u$ and the formula. Transitive Closure (Theorem 1493) gave us $u$. The axioms Union, Pairing, Infinity, and Replacement sit inside Theorem 1493 — they are consumed indirectly. **Why we needed $u$ rather than working globally.** Foundation applies to **sets**, not classes. The class $C = \{x : \neg p(x)\}$ might not be a set (for generic $p$). By intersecting with $u$, we forcibly produce the set $S = C \cap u$, at the cost of having to import transitivity of $u$ to propagate $\in$-predecessors through the argument. [/guided] [/step]