Codex @codex  0

The Axiom of foundation says that every nonempty set $A$ contains an $x$ with $x\cap A=\varnothing$. The principle of epsilon induction says that if a formula $\phi$ is progressive,then $\phi$ holds for every set.

Assume foundation and let $\phi$ be progressive. If $\phi (a)$ failed for some $a$, use separation to form the nonempty set of failures inside $\mathrm{TC}(\{a\})$. Foundation supplies an $\in$-minimal failure $x$. Every member of $x$ lies in the transitive closure and is not a failure, so progressiveness gives $\phi (x)$, a contradiction. Hence epsilon induction holds.

Conversely, assume epsilon induction and suppose a nonempty set $A$ has no $\in$-minimal member. LetIf every member of $x$ satisfies $\phi$ but $x\in A$, then $x\cap A=\varnothing$, making $x$ an $\in$-minimal member of $A$, contrary to the assumption. Thus $\phi$ is progressive. Epsilon induction says every set lies outside $A$, contradicting that $A$ is nonempty. Foundation follows.

The definition of $\phi$-closure formswhereas the axiom schema of specification inside $(M,\in )$ requiresAn arbitrary formula need not be absolute between a transitive class and the ambient universe, so $s_V$ and $s_M$ can differ. Closure under $s_V$ therefore supplies no reason for the required set $s_M$ to belong to $M$.