= Solution
The membership induction principle is the schema
$$
\boxed{\bigl[\forall x\bigl((\forall y\in x\ \varphi(y))\Rightarrow\varphi(x)\bigr)\bigr]\Longrightarrow\forall x\ \varphi(x),}
$$
allowing fixed parameters in $\varphi$.
Suppose the progressiveness hypothesis holds but $\neg\varphi(a)$. The <transitive set> $T=\operatorname{TC}(\{a\})$ contains $a$. <Separation> gives the nonempty set $B=\{x\in T:\neg\varphi(x)\}$. By <Foundation> choose $b\in B$ with $b\cap B=\varnothing$. Every $y\in b$ belongs to $T$ because it is a <transitive set> and cannot belong to $B$, so every such $y$ satisfies $\varphi$. Progressiveness now gives $\varphi(b)$, a contradiction. Thus the principle holds. The <transitive closure> is needed to turn a possibly proper class of counterexamples into a set to which <Foundation> applies.
Back to article page
