13I (source code)

= 13I
{scope}
{title2=Logic and Set Theory}

The <Axiom of foundation> states that every nonempty set $A$ has a member $a$ with $a\cap A=\varnothing$. The principle of <epsilon induction> states that a formula $\phi$ satisfying $\forall x[(\forall y\in x\;\phi(y))\Rightarrow\phi(x)]$ holds for every set $x$.

Assume <Axiom of foundation> and suppose a progressive formula has a counterexample $a$. In the <transitive closure> of $\{a\}$, use <axiom schema of separation> to collect the counterexamples into a nonempty set $B$. Foundation supplies $b\in B$ having no member in $B$. Since the closure is transitive, every member of $b$ satisfies $\phi$, contradicting progressiveness. Conversely, if a nonempty set $A$ had no foundation-minimal member, every $x\in A$ would have a member $y\in x\cap A$. The formula $x\notin A$ is then progressive: if every member of $x$ lies outside $A$, $x$ cannot belong to $A$. <Epsilon induction> would make $A$ empty, a contradiction. This proves equivalence in the presence of the other <Zermelo–Fraenkel set theory>.

To obtain the <cumulative hierarchy>, perform <epsilon induction> on the assertion that $x$ belongs to some $V_\alpha$. If this holds for each member $y$, <Axiom schema of replacement> collects their least such ordinals into a set. Choose an ordinal $\beta$ above them all. Then $x\subseteq V_\beta$ and $x\in V_{\beta+1}$. Thus every set occurs in the hierarchy. Use the <rank of a set> convention $\operatorname{rk}(x)=\sup_{y\in x}(\operatorname{rk}(y)+1)$, equivalently the least $\alpha$ with $x\subseteq V_\alpha$.