Set Theory

Stages and Ranks

content/set-theory/spine/spine.tex

% Part: set-theory% Chapter: spine\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sth}{spine}{Stages and Ranks}\olimport{idea}\olimport{recursion}\olimport{stagesbasics}\olimport{foundation}\olimport{zf}\olimport{rank}\OLEndChapterHook\end{document}

content/set-theory/spine/idea.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{valpha}\olsection{Defining the Stages as the $V_\alpha$s}In \olref[sth][ordinals][]{chap}, we defined well-orderings and the(von Neumann) ordinals. In this chapter, we will use these tocharacterise the hierarchy of sets \emph{itself}. To do this, recallthat in \olref[sth][ordinals][opps]{sec}, we defined the idea ofsuccessor and limit ordinals. We use these ideas in followingdefinition:\begin{defn}\ollabel{defValphas}	\begin{align*}	V_\emptyset &\defis \emptyset\\	V_{\ordsucc{\alpha}} &\defis \Pow{V_\alpha} & & 	\text{for any ordinal }\alpha\\	V_{\alpha} &\defis \bigcup_{\gamma < \alpha} V_\gamma & & 	\text{when }\alpha\text{ is a limit ordinal}\end{align*}\end{defn}\noindentThis will be a definition by \emph{transfinite recursion} on theordinals. In this regard, we should compare this with recursivedefinitions of functions on the natural numbers.\footnote{Cf.\ thedefinitions of addition, multiplication, and exponentiation in\olref[sfr][infinite][dedekind]{sec}.} As when dealing with naturalnumbers, one defines a base case and successor cases; but when dealingwith ordinals, we also need to describe the behaviour of \emph{limit}cases. This definition of the $V_\alpha$s will be an important milestone. Wehave informally motivated our hierarchy of sets as forming sets by\emph{stages}. The $V_\alpha$s are, in effect, just those stages.Importantly, though, this is an \emph{internal} characterisation ofthe stages. Rather than suggesting a possible \emph{model} of thetheory, we will have defined the stages \emph{within} our set theory.\end{document}

content/set-theory/spine/recursion.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{recursion}\olsection{The Transfinite Recursion Theorem(s)}The first thing we must do, though, is confirm that\olref[valpha]{defValphas} is a successful definition. More generally,we need to prove that any attempt to offer a transfinite by(transfinite) recursion will succeed. That is the aim of this section.\emph{Warning: this is tricky material}. The overarching moral,though, is quite simple: Transfinite Induction plus Replacementguarantee the legitimacy of (several versions of) transfiniterecursion.\footnote{A reminder: all formulas and terms can have parameters (unless explicitly stated otherwise).}\begin{defn}	Let $\tau(x)$ be a term; let $f$ be a function; let $\alpha$ be an ordinal. We say that $f$ is an \emph{$\alpha$-approximation} for $\tau$ iff both $\dom{f} = \alpha$ and $(\forall \beta \in \alpha)f(\beta) = \tau(\funrestrictionto{f}{\beta})$.\end{defn}\begin{lem}[Bounded Recursion]\ollabel{transrecursionfun}For any term $\tau(x)$ and any ordinal $\alpha$, there is a unique $\alpha$-approximation for $\tau$.\end{lem}\begin{proof}We will show that, for any $\gamma \leq \alpha$, there is a unique$\gamma$-approximation. We first establish uniqueness. Let $g$ and $h$ (respectively) be $\gamma$- and $\delta$-approximations. A transfinite induction on their arguments shows that$g(\beta) = h(\beta)$ for any $\beta \in \dom{g} \cap \dom{h} =\gamma \cap \delta = \min(\gamma, \delta)$. So our approximations are unique (if they exist), and agree on all values.To establish existence, we now use a simple transfinite induction(\olref[ordinals][opps]{simpletransrecursion}) on ordinals$\delta \leq \alpha$. The empty function is trivially an $\emptyset$-approximation. If $g$ is a $\gamma$-approximation, then $g \cup\{\tuple{\gamma, \tau(g)}\}$ is a $\ordsucc{\gamma}$-approximation.If $\gamma$ is a limit ordinal and $g_\delta$ is a $\delta$-approximation for all $\delta < \gamma$, let $g = \bigcup_{\delta \in \gamma} g_\delta$. Thisis a function, since our various $g_\delta$s agree on all values. Andif $\delta \in \gamma$ then $g(\delta) = g_{\ordsucc{\delta}}(\delta) =\tau(\funrestrictionto{g_{\ordsucc{\delta}}}{\delta}) =\tau(\funrestrictionto{g}{\delta})$.This completes the proof by transfinite induction.\end{proof}If we allow ourselves to define a \emph{term} rather than a function,then we can remove the bound $\alpha$ from the previous result. Inthe statement and proof of the following result, when $\sigma$ is a term, welet $\funrestrictionto{\sigma}{\alpha} = \Setabs{\tuple{\beta,\sigma(\beta)}}{\beta \in \alpha}$.\begin{thm}[General Recursion]\ollabel{transrecursionschema}For any term $\tau(x)$, we can explicitly define a term$\sigma(x)$, such that$\sigma(\alpha) = \tau(\funrestrictionto{\sigma}{\alpha})$ for anyordinal~$\alpha$.\end{thm}\begin{proof}For each $\alpha$, by \olref{transrecursionfun} there is a unique $\alpha$-approximation, $f_\alpha$, for~$\tau$. Define $\sigma(\alpha)$ as $f_{\ordsucc{\alpha}}(\alpha)$. Now:	\begin{align*}		\sigma(\alpha) &= 		f_{\ordsucc{\alpha}}(\alpha) \\&= 		\tau(\funrestrictionto{f_{\ordsucc{\alpha}}}{\alpha}) \\&= 		\tau(\Setabs{\tuple{\beta, f_{\ordsucc{\alpha}}(\beta)}}{\beta \in \alpha}) \\&= 		\tau(\Setabs{\tuple{\beta, f_{\ordsucc{\beta}}(\beta)}}{\beta \in \alpha})\\&=		\tau(\funrestrictionto{\sigma}{\alpha})	\end{align*}noting that $f_{\ordsucc{\beta}}(\beta) = f_{\ordsucc{\alpha}}(\beta)$ for all $\beta < \alpha$, as in \olref{transrecursionfun}. \end{proof}\noindent Note that \olref{transrecursionschema} is a \emph{schema}. Crucially, we cannotexpect $\sigma$ to define a function, i.e., a certain kind of\emph{set}, since then $\dom{\sigma}$ would be the set of allordinals, contradicting the Burali-Forti Paradox(\olref[ordinals][basic]{buraliforti}).It still remains to show, though, that \olref{transrecursionschema}vindicates our definition of the $V_\alpha$s. This may not beimmediately obvious; but it will become apparent with a last, simple,version of transfinite recursion.\begin{thm}[Simple Recursion]\ollabel{simplerecursionschema} For any terms $\tau(x)$ and $\theta(x)$ and any set $A$, we canexplicitly define a term $\sigma(x)$ such that:\begin{align*}	\sigma(\emptyset) &= A\\	\sigma(\ordsucc{\alpha}) &= \tau(\sigma(\alpha)) &&		\text{for any ordinal }\alpha\\	\sigma(\alpha) &= \theta(\ran{\funrestrictionto{\sigma}{\alpha}})&&	\text{when }\alpha\text{ is a limit ordinal}\end{align*}\end{thm}\begin{proof}We start by defining a term, $\xi(x)$, as follows: %t $\xi(x) = A$ if $x$ is not a function whose domain is an ordinal;%otherwise let:\[	\xi(x) = 	\begin{cases}			A &\text{if $x$ is not a function whose}\\			&\hspace{1em}\text{domain is an ordinal; otherwise:}\\			\tau(x(\alpha)) & \text{if $\dom{x} = \ordsucc{\alpha}$}\\			\theta(\ran{x}) & \text{if $\dom{x}$ is a limit ordinal}	\end{cases}\]By \olref{transrecursionschema}, there is a term $\sigma(x)$ such that$\sigma(\alpha) = \xi(\funrestrictionto{\sigma}{\alpha})$ for everyordinal $\alpha$; moreover, $\funrestrictionto{\sigma}{\alpha}$ is afunction with domain $\alpha$. We show that $\sigma$ has the requiredproperties, by simple transfinite induction(\olref[ordinals][opps]{simpletransrecursion}). First, $\sigma(\emptyset) = \xi(\emptyset) = A$. Next, $\sigma(\ordsucc{\alpha}) = \xi(\funrestrictionto{\sigma}{\ordsucc{\alpha}}) = \tau(\funrestrictionto{\sigma}{\ordsucc{\alpha}}(\alpha)) = \tau(\sigma(\alpha))$.Last, $\sigma(\alpha) = \xi(\funrestrictionto{\sigma}{\alpha}) = \theta(\ran{\funrestrictionto{\sigma}{\alpha}})$, when $\alpha$ is a limit.\end{proof}\noindentNow, to vindicate \olref[valpha]{defValphas}, just take $A= \emptyset$ and $\tau(x) = \Pow{x}$ and $\theta(x) = \bigcup x$. At long last, this vindicates the definition of the $V_\alpha$s!{}\end{document}

content/set-theory/spine/stagesbasics.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{Valphabasic}\olsection{Basic Properties of Stages}To bring out the foundational importance of the definition of the$V_\alpha$s, we will present a few basic results about them. We start with a definition:\footnote{There's no standard terminology for ``potent''; this is the name used by \citet{ButtonLT1}.}\begin{defn}	The set $A$ is \emph{potent} iff $\forall x((\exists y \in A)x \subseteq y \lif x \in A)$. \end{defn}\begin{lem}\ollabel{Valphabasicprops}For each ordinal $\alpha$:\begin{enumerate}	\item\ollabel{Valphatrans} Each $V_\alpha$ is transitive.	\item\ollabel{Valphapotent} Each $V_\alpha$ is potent.	\item\ollabel{Valphacum} If $\gamma \in \alpha$, then $V_\gamma	\in V_\alpha$ (and hence also $V_\gamma \subseteq V_\alpha$ by	\olref{Valphatrans})\end{enumerate}\end{lem}\begin{proof}We prove this by a (simultaneous) transfinite induction.  Forinduction, suppose that \olref{Valphatrans}--\olref{Valphacum} holdsfor each ordinal $\beta < \alpha$. The case of $\alpha = \emptyset$ is trivial. Suppose $\alpha = \ordsucc{\beta}$. To show \olref{Valphacum}, if$\gamma \in \alpha$ then $V_\gamma \subseteq V_\beta$ by hypothesis,so $V_\gamma \in \Pow{V_\beta} = V_\alpha$. To show\olref{Valphapotent}, suppose $A \subseteq B \in V_\alpha$ i.e., $A\subseteq B \subseteq V_\beta$; then $A \subseteq V_\beta$ so $A \inV_\alpha$. To show \olref{Valphatrans}, note that if $x \in A \inV_\alpha$ we have $A \subseteq V_\beta$, so $x \in V_\beta$, so $x\subseteq V_\beta$ as $V_\beta$ is transitive by hypothesis, and so $x\in V_\alpha$. Suppose $\alpha$ is  a limit ordinal. To show \olref{Valphacum}, if$\gamma \in \alpha$ then $\gamma \in \ordsucc{\gamma} \in \alpha$, sothat $V_\gamma \in V_{\ordsucc{\gamma}}$ by assumption, hence$V_\gamma \in \bigcup_{\beta \in \alpha} V_\beta = V_\alpha$. To show\olref{Valphatrans} and \olref{Valphapotent}, just observe that aunion of transitive (respectively, potent) sets is transitive(respectively, potent). \end{proof}\begin{lem}\ollabel{Valphanotref}For each ordinal $\alpha$, $V_\alpha \notin V_\alpha$.\end{lem}\begin{proof}By transfinite induction. Evidently $V_\emptyset \notin V_\emptyset$. If $V_{\ordsucc{\alpha}} \in V_{\ordsucc{\alpha}} = \Pow{V_\alpha}$,then $V_{\ordsucc{\alpha}} \subseteq V_\alpha$; and since $V_\alpha\in V_{\ordsucc{\alpha}}$ by \olref{Valphabasicprops}, we have$V_\alpha \in V_\alpha$. Conversely: if $V_\alpha \notin V_\alpha$then $V_{\ordsucc{\alpha}} \notin V_{\ordsucc{\alpha}}$If $\alpha$ is a limit and $V_\alpha \in V_\alpha = \bigcup_{\beta \in\alpha}V_\beta$, then $V_\alpha \in V_\beta$ for some $\beta \in\alpha$; but then also $V_\beta \in V_\alpha$ so that $V_\beta \inV_\beta$ by \olref{Valphabasicprops} (twice). Conversely, if $V_\beta\notin V_\beta$ for all $\beta \in \alpha$, then $V_\alpha \notinV_\alpha$.\end{proof}\begin{cor}For any ordinals $\alpha, \beta$: $\alpha \in \beta$ iff $V_\alpha \in V_\beta$\end{cor}\begin{proof}\Olref{Valphabasicprops} gives one direction. Conversely, suppose $V_\alpha \in V_\beta$. Then $\alpha \neq \beta$ by \olref{Valphanotref}; and $\beta \notin \alpha$, for otherwise we would have $V_\beta \in V_\alpha$ and hence $V_\beta \in V_\beta$ by \olref{Valphabasicprops} (twice), contradicting \olref{Valphanotref}. So $\alpha \in \beta$ by Trichotomy.\end{proof}\noindentAll of this allows us to think of each $V_\alpha$ as the $\alpha$thstage of the hierarchy. Here is why.Certainly our $V_\alpha$s can be thought of as being formed in an\emph{iterative} process, for our use of ordinals tracks the notion ofiteration. Moreover, if one stage is formed before the other, i.e.,$V_\beta \in V_\alpha$, i.e., $\beta \in \alpha$, then our process offormation is \emph{cumulative}, since $V_\beta \subseteq V_\alpha$.Finally, we are indeed forming \emph{all} possible collections of setsthat were available at any earlier stage, since any successor stage$V_{\ordsucc{\alpha}}$ is the power-set of its predecessor $V_\alpha$.In short: with $\ZFminus$, we are \emph{almost} done, in articulatingour vision of the cumulative-iterative hierarchy of sets. (Though, ofcourse, we still need to justify Replacement.)\end{document}

content/set-theory/spine/foundation.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{foundation}\olsection{Foundation}We are only \emph{almost} done---and not \emph{quite} finished---because nothing in$\ZFminus$ guarantees that \emph{every} set is in some $V_\alpha$,i.e., that every set is formed at some stage. Now, there is a fairly straightforward (mathematical) sense in whichwe don't \emph{care} whether there are sets outside the hierarchy. (Ifthere are any there, we can simply ignore them.) But we have motivatedour \emph{concept} of set with the thought that every set is formed atsome stage (see \stageshier{} in \olref[z][story]{sec}). Sowe will want to preclude the possibility of sets which fall outside ofthe hierarchy. Accordingly, we must add a new axiom, which ensuresthat every set occurs somewhere in the hierarchy. Since the $V_\alpha$s are our stages, we might simply consider addingthe following as an axiom:\begin{defish}\emph{Regularity.} $\forall A \exists \alpha\, A \subseteq V_\alpha$\end{defish}This would be a perfectly reasonable approach. However, for reasonsthat will be explained in the next section, we will instead adopt analternative axiom:\begin{axiom}[Foundation]$(\forall A \neq \emptyset)(\exists B \in A)A \cap B = \emptyset$.\end{axiom}With some effort, we can show (in $\ZFminus$) that Foundation entails Regularity:\begin{defn}For each set $A$, let:\begin{align*}	\text{cl}_0(A) &= A,\\	\text{cl}_{n+1}(A) &= \bigcup \text{cl}_n(A),\\	\text{trcl}(A) &= \bigcup_{n < \omega} \text{cl}_{n}(A).\end{align*}We call $\text{trcl}(A)$ the \emph{transitive closure} of $A$.\end{defn}\noindentThe name ``transitive closure'' is apt:\begin{prop}\ollabel{subsetoftrcl}$A \subseteq \trcl{A}$ and $\trcl{A}$ is a transitive set. \end{prop}\begin{proof}Evidently $A = \text{cl}_0(A) \subseteq \text{trcl}(A)$. And if $x\in b \in \trcl{A}$,  then $b \in \text{cl}_n(A)$ for some $n$, so $x\in \text{cl}_{n+1}(A) \subseteq \text{trcl}(A)$. \end{proof}\begin{lem}\ollabel{lem:TransitiveWellFounded}If $A$ is a transitive set, then there is some $\alpha$ such that $A\subseteq V_\alpha$.\end{lem}\begin{proof}Recalling the definition of ``$\supstrict(X)$'' from\olref[ordinals][opps]{defsupstrict}, define two sets:\begin{align*}	D  &= \Setabs{x \in A}{\forall \delta\ x \nsubseteq V_\delta}\\	\alpha &= \supstrict\Setabs{\delta}{(\exists x \in A)	(x \subseteq V_\delta \land (\forall \gamma \in \delta)x \nsubseteq V_\gamma)}\end{align*}Suppose $D = \emptyset$. So if $x \in A$, then there is some $\delta$ such that $x \subseteq V_\delta$ and, by the well-ordering of the ordinals, $(\forall \gamma \in \delta)x \nsubseteq V_\gamma$; hence $\delta \in \alpha$ and so $x \in V_\alpha$ by\olref[spine][Valphabasic]{Valphabasicprops}. Hence $A \subseteqV_{\alpha}$, as required. So it suffices to show that $D = \emptyset$. For reductio, supposeotherwise. By Foundation, there is some $B \in D \subseteq A$ such that $D \cap B= \emptyset$. If $x \in B$ then $x \in A$, since $A$ is transitive,and since $x \notin D$, it follows that $\exists \delta\ x \subseteqV_\delta$. So now let\[	\beta = \supstrict\Setabs{\delta}{(\exists x \in b)(x \subseteq V_\delta \land (\forall \gamma < \delta)x \nsubseteq V_\gamma)}.\]As before, $B \subseteq V_\beta$, contradicting the claim that $B \inD$.	\end{proof}\begin{thm}\ollabel{zfentailsregularity}Regularity holds.\end{thm}\begin{proof}Fix $A$; now $A \subseteq \trcl{A}$ by \olref{subsetoftrcl}, which is transitive. So there is some $\alpha$ such that $A \subseteq \trcl{A} \subseteq V_\alpha$ by \olref{lem:TransitiveWellFounded}\end{proof}These results show that $\ZFminus$ proves the conditional$\emph{Foundation}\Rightarrow\emph{Regularity}$. In\olref[spine][rank]{zfminusregularityfoundation}, we will show that$\ZFminus$ proves $\emph{Regularity}\Rightarrow\emph{Foundation}$. Assuch, Foundation and Regularity are \emph{equivalent} (modulo$\ZFminus$). But this means that, given $\ZFminus$, we can justifyFoundation by noting that it is equivalent to Regularity. And we canjustify Regularity immediately on the basis of \stageshier{}. \end{document}

content/set-theory/spine/zf.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{zf}\olsection{$\Z$ and $\ZF$: A Milestone}With Foundation, we reach another important milestone. We haveconsidered theories $\Zminus$ and $\ZFminus$, which we said werecertain theories ``minus'' a certain something. That certain somethingis Foundation. So:\begin{defn}The theory $\Z$ adds Foundation to $\Zminus$. So its axioms areExtensionality, Union, Pairs, Powersets, Infinity, Foundation, and allinstances of the Separation scheme.The theory $\ZF$ adds Foundation to $\ZFminus$. Otherwise put, $\ZF$adds all instances of Replacement to~$\Z$.\end{defn}Still, one question might have occurred to you. If Regularity isequivalent over $\ZFminus$ to Foundation, and Regularity'sjustification is clear, why bother to go around the houses, and takeFoundation as our basic axiom, rather than Regularity? Setting aside historical reasons (to do with who formulated what andwhen), the basic reason is that Foundation can be presented withoutemploying the definition of the~$V_\alpha$s. That definition reliedupon all of the work of \olref[recursion]{sec}: weneeded to prove Transfinite Recursion, to show that it was justified.But our proof of Transfinite Recursion employed \emph{Replacement}.So, whilst Foundation and Regularity are equivalent modulo $\ZFminus$,they are not equivalent modulo $\Zminus$. Indeed, the matter is more drastic than this simple remark suggests.Though it goes well beyond this book's remit, it turns out that both$\Zminus$ and $\Z$ are too weak to define the $V_\alpha$s. So, if youare working only in $\Z$, then Regularity (as we have formulated it)does not even make \emph{sense}. This is why our official axiom isFoundation, rather than Regularity. From now on, we will work in $\ZF$ (unless otherwise stated), withoutany further comment. \end{document}

content/set-theory/spine/rank.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{spine}{rank}\olsection{Rank}Now that we have defined the stages as the $V_\alpha$'s, and we knowthat every set is a subset of some stage, we can define the\emph{rank} of a set. Intuitively, the rank of $A$ is the first momentat which $A$ is formed. More precisely:\begin{defn}\ollabel{defnsetrank}For each set $A$, $\setrank{A}$ is the least ordinal $\alpha$ such that $A\subseteq V_\alpha$.\end{defn}\begin{prop}\ollabel{ranksexist}	$\setrank{A}$ exists, for any $A$.\end{prop}\begin{proof}	Left as an exercise.\end{proof}\begin{prob}	Prove \olref[sth][spine][rank]{ranksexist}.	\end{prob}\noindent The well-ordering of ranks allows us to prove some important results:\begin{prop}\ollabel{valphalowerrank}For any ordinal $\alpha$, $V_\alpha = \Setabs{x}{\setrank{x} \in \alpha}$.\end{prop}\begin{proof}If $\setrank{x} \in \alpha$ then $x \subseteq V_{\setrank{x}} \inV_\alpha$, so $x \in V_\alpha$ as $V_\alpha$ is potent (invoking\olref[Valphabasic]{Valphabasicprops} multiple times). Conversely, if $x \in V_\alpha$ then $x \subseteq V_\alpha$, so $\setrank{x} \leq \alpha$; now a simple transfinite induction shows that $x \notin V_\alpha$. \end{proof}\begin{prob}	Complete the simple transfinite induction mentioned in \olref[sth][spine][rank]{valphalowerrank}.\end{prob}\begin{prop}\ollabel{rankmemberslower}If $B \in A$, then $\setrank{B} \in \setrank{A}$.\end{prop}\begin{proof}$A \subseteq V_{\setrank{A}} = \Setabs{x}{\setrank{x} \in\setrank{A}}$ by \olref{valphalowerrank}.\end{proof}\noindentUsing this fact, we can establish a result which allows us to provethings about \emph{all sets} by a form of induction:\begin{thm}[$\in$-Induction Scheme] For any formula $\phi$:\[	\forall A((\forall x \in A)\phi(x) \lif \phi(A)) \lif \forall A \phi(A).\]\end{thm}\begin{proof}We will prove the contrapositive. So, suppose $\lnot \forall A\phi(A)$. By Transfinite Induction(\olref[ordinals][basic]{ordinductionschema}), thereis some non-$\phi$ of least possible rank; i.e.\ some $A$such that $\lnot \phi(A)$ and $\forall x(\setrank{x} \in \setrank{A}\lif \phi(x))$. Now if $x \in A$ then $\setrank{x} \in\setrank{A}$, by \olref{rankmemberslower}, so that $\phi(x)$; i.e.\ $(\forall x \inA)\phi(x) \land \lnot \phi(A)$.\end{proof}\noindent Here is an informal way to gloss this powerfulresult. Say that $\phi$ is \emph{hereditary} iff whenever every!!{element} of a set is $\phi$, the set itself is $\phi$. Then$\in$-Induction tells you the following: if $\phi$ is hereditary,every set is $\phi$.To wrap up the discussion of ranks (for now), we'll prove a fewclaims which we have foreshadowed a few times. \begin{prop}\ollabel{ranksupstrict}$\setrank{A} = \supstrict_{x \in A}\setrank{x}$.\end{prop}\begin{proof}Let $\alpha = \supstrict_{x \in A}\setrank{x}$. By\olref{rankmemberslower}, $\alpha \leq \setrank{A}$. But if $x \in A$then $\setrank{x} \in \alpha$, so that $x \in V_\alpha$ by \olref{valphalowerrank}, and hence $A\subseteq V_\alpha$, i.e., $\setrank{A} \leq \alpha$. Hence$\setrank{A} = \alpha$.\end{proof}\begin{cor}\ollabel{ordsetrankalpha}For any ordinal $\alpha$, $\setrank{\alpha} = \alpha$.\end{cor}\begin{proof}Suppose for transfinite induction that $\setrank{\beta} = \beta$ forall $\beta \in \alpha$. Now $\setrank{\alpha} = \supstrict_{\beta \in\alpha}\setrank{\beta} = \supstrict_{\beta \in \alpha}\beta = \alpha$by \olref{ranksupstrict}.%	First note that $\setrank{\alpha} \neq \beta$ for any $\beta \in%	\alpha$. For otherwise we would have $\beta = \setrank{\beta} \in%	\setrank{\alpha} = \beta$ by \olref{rankmemberslower}, i.e.,%	$\beta \in \beta$, a contradiction. %%	Now note that $\alpha \subseteq V_\alpha$. For $\alpha =%	\Setabs{\beta}{\beta \in \alpha}$ by%	\olref[sfr][ordinals][basic]{ordissetofsmallerord}. And if%	$\beta \in \alpha$ then $\beta \subseteq V_{\setrank{\beta}} =%	V_\beta \in V_\alpha$, hence $\beta \in V_\alpha$, by%	\olref[sfr][spine][Valphabasic]{Valphabasicprops} twice. \end{proof}Finally, here is a quick proof of the result promised at the end of\olref[foundation]{sec}, that $\ZFminus$ proves the conditional$\emph{Regularity} \Rightarrow \emph{Foundation}$. (Note that thenotion of ``rank'' and \olref{rankmemberslower} are available for usein this proof since---as mentioned at the start of this section---theycan be presented using $\ZFminus + \text{Regularity}$.)\begin{prop}[working in $\ZFminus + \text{Regularity}$]\ollabel{zfminusregularityfoundation} Foundation holds.\end{prop}\begin{proof}Fix $A \neq \emptyset$, and some $B \in A$ of least possible rank. If$c \in B$ then $\setrank{c} \in \setrank{B}$ by\olref{rankmemberslower}, so that $c \notin A$ by choice of $B$.\end{proof}\end{document}