Set Theory

Steps towards Z

content/set-theory/z/z.tex

% Part: set-theory% Chapter: z\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sth}{z}{Steps towards $\Z$}\olimport{story}\olimport{separation}\olimport{union}\olimport{pairs}\olimport{powerset}\olimport{infinity-again}\olimport{milestone}\olimport{nat}\olimport{arbintersections}\OLEndChapterHook\end{document}

content/set-theory/z/story.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{story}\olsection{The Story in More Detail}	In \olref[story][approach]{sec}, we quoted Schoenfield'sdescription of the process of set-formation. We now want to write downa few more principles, to make this story a bit more precise. Herethey are:\begin{enumerate}\item[] \stageshier. Every set is formed at some stage.\item[] \stagesord. Stages are ordered: some come \emph{before}others.\footnote{We will actually assume---tacitly---that the stagesare \emph{well-ordered}. What this amounts to is explained in\olref[ordinals][]{chap}. This is a substantial assumption. In fact,using a very clever technique due to \citet{Scott1974}, thisassumption can be \emph{avoided} and then \emph{derived}. (This willalso explain why we should think that there is an initial stage.) We cannot go into that here; for more, see \citet{ButtonLT1}.} \item[] \stagesacc. For any stage $S$, and for any sets which wereformed \emph{before} stage~$S$: a set is formed at stage~$S$ whosemembers are exactly those sets. Nothing else is formed at stage~$S$.\end{enumerate}These are informal principles, but we will be able to use them tovindicate several of the axioms of Zermelo's set theory. (We should offer a word of caution. Although we will be presenting somecompletely standard axioms, with completely standard names, theitalicized principles we have just presented have no particular namesin the literature. We simply monikers which we hope are helpful.)\end{document}

content/set-theory/z/separation.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{sep}\olsection{Separation}We start with a principle to replace Na\"{i}ve Comprehension:\begin{axiom}[Scheme of Separation] For every formula $\phi(x)$, this is anaxiom: for any $A$, the set $\Setabs{x \in A}{\phi(x)}$ exists.\end{axiom}Note that this is not a single axiom. It is a \emph{scheme} of axioms.There are \emph{infinitely many} Separation axioms; one for everyformula $\phi(x)$. The scheme can equally well be (and normally is)written down as follows:\begin{defish}For any formula $\phi(x)$ which does not contain ``$S$'', this is anaxiom:\[	\forall A \exists S \forall x(x \in S \liff (\phi(x) \land x \in A)).\]\end{defish}In keeping with the convention noted at the start of\olref[sth][][]{part}, the formulas~$\phi$ in the Separation axiomsmay have parameters.\footnote{For an explanation of what this means,see the discussion immediately after\olref[sfr][infinite][induction]{natinductionschema}.}Separation is immediately justified by our cumulative-iterativeconception of sets we have been telling. To see why, let $A$ be a set.So $A$ is formed by some stage~$S$ (by \stageshier). Since $A$ wasformed at stage~$S$, all of $A$'s members were formed before stage $S$(by \stagesacc). Now in particular, consider all the sets which aremembers of $A$ and which also satisfy $\phi$; clearly all of thesesets, too, were formed before stage~$S$. So they are formed into a set$\Setabs{x \in A}{\phi(x)}$ at stage~$S$ too (by \stagesacc).Unlike Na\"ive Comprehension, this avoid Russell's Paradox. For wecannot simply assert the existence of the set $\Setabs{x}{x \notinx}$. Rather, \emph{given} some set~$A$, we can assert the existence ofthe set $R_A = \Setabs{x \in A}{x \notin x}$. But all this proves isthat $R_A \notin R_A$ and $R_A \notin A$, none of which is veryworrying.However, Separation has an immediate and striking consequence:\begin{thm}\ollabel{thm:NoUniversalSet}There is no \emph{universal} set, i.e., $\Setabs{x}{x = x}$ does not exist.\end{thm}\begin{proof}For reductio, suppose $V$ is a universal set. Then by Separation, $R =\Setabs{x \in V}{x \notin x} = \Setabs{x}{x \notin x}$ exists,contradicting Russell's Paradox.\end{proof}The absence of a universal set---indeed, the open-endedness of thehierarchy of sets---is one of the most fundamental ideas behind thecumulative-iterative conception. So it is worth seeing that,intuitively, we could reach it via a different route. A universal setmust be !!a{element} of itself. But, on our cumulative-iterativeconception, every set appears (for the first time) in the hierarchy atthe first stage immediately after all of its !!{element}s. But thisentails that \emph{no} set is self-membered. For any self-membered setwould have to first occur immediately after the stage at which itfirst occurred, which is absurd. (We will see in\olref[sth][spine][rank]{defnsetrank} how to make this explanationmore rigorous, by using the notion of the ``rank'' of a set. However,we will need to have a few more axioms in place to do this.)Here are a few more consequences of Separation and Extensionality.\begin{prop}\ollabel{prop:emptyexists}If any set exists, then $\emptyset$ exists.\end{prop}\begin{proof}If $A$ is a set, $\emptyset = \Setabs{x \in A}{x \neq x}$ exists by Separation.\end{proof}\begin{prop}$A \setminus B$ exists for any sets $A$ and $B$\end{prop}\begin{proof}$A \setminus B = \Setabs{x \in A}{x \notin B}$ exists by Separation.\end{proof}It also turns out that (almost) arbitrary intersections exist:\begin{prop}\ollabel{prop:intersectionsexist}If $A \neq \emptyset$, then $\bigcap A = \Setabs{x}{(\forall y \in A)x \in y}$ exists.\end{prop}\begin{proof}Let $A \neq \emptyset$, so there is some $c \in A$. Then $\bigcap A =\Setabs{x}{(\forall y \in A)x \in y} = \Setabs{x \in c}{(\forall y \inA)x \in y}$, which exists by Separation.\end{proof}Note the condition that $A \neq \emptyset$, though; for $\bigcap\emptyset$ would be the universal set, vacuously, contradicting\olref{thm:NoUniversalSet}.\end{document}

content/set-theory/z/union.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{union}\olsection{Union}\olref[sth][z][sep]{prop:intersectionsexist} gave us intersections.But if we want arbitrary unions to exist, we need to lay down anotheraxiom:\begin{axiom}[Union] For any set $A$, the set $\bigcup A =\Setabs{x}{(\exists b \in A) x \in b}$ exists.\[	\forall A \exists U \forall x(x \in U \liff (\exists b \in A)x \in b)\]\end{axiom}This axiom is also justified by the cumulative-iterative conception.Let $A$ be a set, so $A$ is formed at some stage $S$ (by \stageshier).Every member of $A$ was formed \emph{before}  $S$ (by \stagesacc); so,reasoning similarly, every member of every member of $A$ was formedbefore $S$. Thus all of \emph{those} sets are available before $S$, tobe formed into a set at $S$. And that set is just $\bigcup A$.\end{document}

content/set-theory/z/pairs.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{pairs}\olsection{Pairs}The next axiom to consider is the following:\begin{axiom}[Pairs]For any sets $a, b$, the set $\{a, b\}$ exists.\[	\forall a \forall b \exists P \forall x (x \in P \liff (x = a \lor x = b))\]\end{axiom}Here is how to justify this axiom, using the iterative conception. Suppose $a$ is available at stage $S$, and $b$ is available at stage $T$. Let $M$ be whichever of stages $S$ and $T$ comes later. Then since $a$ and $b$ are both available at stage $M$, the set $\{a,b\}$ is a possible collection available at any stage after $M$ (whichever is the greater).But hold on!{} Why assume that there \emph{are} any stages after $M$? If there are none, then our justification will fail. So, to justify Pairs, we will have to add another principle to the story we told in \olref[sth][z][story]{sec}, namely:\begin{enumerate}	\item[] \stagessucc. There is no last stage.\end{enumerate}Is this principle justified? Nothing in Shoenfield's story stated\emph{explicitly} that there is no last stage. Still, even if it is(strictly speaking) an extra addition to our story, it fits well withthe basic idea that sets are formed in stages. We will simply acceptit in what follows. And so, we will accept the Axiom of Pairs too.Armed with this new Axiom, we can prove the existence of plenty more sets. For example:\begin{prop}\ollabel{prop:pairsconsequences}For any sets $a$ and $b$, the following sets exist:	\begin{enumerate}		\item\ollabel{singleton} $\{a\}$		\item\ollabel{binunion} $a \cup b$		\item\ollabel{tuples} $\tuple{a, b}$	\end{enumerate}\end{prop}\begin{proof}\olref{singleton}. By Pairs, $\{a, a\}$ exists, which is $\{a\}$ byExtensionality.\olref{binunion}. By Pairs, $\{a, b\}$ exists. Now $a \cup b = \bigcup\{a, b\}$ exists by Union.\olref{tuples}. By \olref{singleton}, $\{a\}$ exists. By Pairs, $\{a,b\}$ exists. Now $\{\{a\}, \{a, b\}\} = \tuple{a, b}$ exists, by Pairsagain.\end{proof}\begin{prob}Show that, for any sets $a, b, c$, the set $\{a, b, c\}$ exists.\end{prob}\begin{prob}Show that, for any sets $a_1, \ldots, a_n$, the set $\{a_1, \ldots,a_n\}$ exists.\end{prob}%\begin{proof} By two applications of Pairs, $\{\{a_1, a_2\}, \{a_1,%   a_3\}\}$ exists. By Union and Extensionality, $\bigcup \{\{a_1,%   a_2\}, \{a_1, a_3\}\} = \{a_1, a_2, a_3\}$ exists. Repeat this%   trick as often as necessary. \end{proof}\end{document}

content/set-theory/z/powerset.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{power}\olsection{Powersets}We will proceed with another axiom:\begin{axiom}[Powersets]For any set $A$, the set $\Pow{A} = \Setabs{x}{x \subseteq A}$ exists.\[	\forall A \exists P \forall x(x \in P \liff (\forall z \in x)z \in A)\]\end{axiom}Our justification for this is pretty straightforward. Suppose $A$ isformed at stage $S$. Then all of $A$'s members were available before$S$ (by \stagesacc). So, reasoning as in our justification forSeparation, every subset of $A$ is formed by stage $S$. So they areall available, to be formed into a single set, at any stage after $S$.And we know that there is some such stage, since $S$ is not the laststage (by \stagessucc). So $\Pow{A}$ exists.Here is a nice consequence of Powersets:\begin{prop}\label{thm:Products}Given any sets $A, B$, their Cartesian product $A \times B$ exists.\end{prop}\begin{proof}The set $\Pow{\Pow{A \cup B}}$ exists by Powersets and\olref[sth][z][pairs]{prop:pairsconsequences}. So by Separation, thisset exists:\[	C = \Setabs{z \in \Pow{\Pow{A \cup B}}}{(\exists x \in A)(\exists y \in B) z = \tuple{x, y}}.\]Now, for any $x \in A$ and $y \in B$, the set $\tuple{x, y}$ exists by\olref[sth][z][pairs]{prop:pairsconsequences}. Moreover, since $x, y\in A \cup B$, we have that $\{x\}, \{x, y\} \in \Pow{A \cup B}$, and$\tuple{x,y} \in \Pow{\Pow{A \cup B}}$. So $A \times B = C$.\end{proof}In this proof, Powerset interacts with Separation. And that is nosurprise. Without Separation, Powersets wouldn't be a very\emph{powerful} principle. After all, Separation tells us whichsubsets of a set exist, and hence determines just how ``fat'' eachPowerset is.\begin{prob}Show that, for any sets $A, B$: (i) the set of all relations withdomain $A$ and range $B$ exists; and (ii) the set of all functionsfrom $A$ to $B$ exists.\end{prob}\begin{prob}Let $A$ be a set, and let $\sim$ be an equivalence relation on $A$.Prove that the set of equivalence classes under $\sim$ on $A$, i.e.,$\equivclass{A}{\sim}$, exists.\end{prob}\end{document}

content/set-theory/z/infinity-again.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{infinity-again}	\olsection{Infinity}We already have enough axioms to ensure that there are infinitely manysets (if there are any). For suppose some set exists, and so$\emptyset$ exists (by \olref[sth][z][sep]{prop:emptyexists}). Now forany set~$x$, the set $x \cup \{x\}$ exists by\olref[sth][z][pairs]{prop:pairsconsequences}. So, applying this a fewtimes, we will get sets as follows:\begin{enumerate}	\item[0.] $\emptyset$ %& $0$ & stage $0$\\	\item[1.] $ \{\emptyset\}$ %& $1$ & stage $1$\\	\item[2.] $\{\emptyset, \{\emptyset\}\}$ %& $2$ & stage $2$\\	\item[3.] $\{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}$ %&$3$ & stage $3$\\	\item[4.] $\{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}, \{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}\}$% & $4$ & stage $4$ \end{enumerate}and we can check that each of these sets is distinct. We have started the numbering from $0$, for a few reasons. But one ofthem is this. It is not that hard to check that the set we havelabelled ``$n$'' has exactly $n$ members, and (intuitively) is formedat the $n$th stage. But. This gives us \emph{infinitely many} sets, but it does notguarantee that there is an \emph{infinite set}, i.e., a set withinfinitely many members. And this really matters: unless we can find a(Dedekind) infinite set, we cannot construct a Dedekind algebra. Butwe want a Dedekind algebra, so that we can treat it as the set ofnatural numbers. (Compare\olref[sfr][infinite][dedekindsproof]{sec}.)Importantly, the axioms we have laid down so far do \emph{not}guarantee the existence of any infinite set. So we have to lay down anew axiom:\begin{axiom}[Infinity]There is a set, $I$, such that $\emptyset \in I$ and $x \cup \{x\} \in I$ whenever $x \in I$.\begin{align*}	\exists I( & (\exists o \in I)\forall x\ x \notin o \land {}\\	& (\forall x \in I)(\exists s \in I)\forall z(z \in s \liff (z \in x \lor z = x)))\end{align*}\end{axiom}It is easy to see that the set $I$ given to us by the Axiom ofInfinity is Dedekind infinite. Its distinguished element is$\emptyset$, and the injection on $I$ is given by $s(x) = x\cup\{x\}$. Now,\olref[sfr][infinite][dedekind]{thm:DedekindInfiniteAlgebra} showedhow to extract a Dedekind Algebra from a Dedekind infinite set; and wewill treat this as our set of natural numbers. More precisely:\begin{defn}\ollabel{defnomega}Let $I$ be any set given to us by the Axiom of Infinity. Let $s$be the function $s(x) = x \cup \{x\}$. Let $\omega =\closureofunder{s}{\emptyset}$. We call the members of $\omega$ the\emph{natural numbers}, and say that $n$ is the result of $n$-manyapplications of $s$ to $\emptyset$.\end{defn}You can now look back and check that the set labelled ``$n$'', a fewparagraphs earlier, will be treated \emph{as} the number $n$. We will discuss this significance of this stipulation in\olref[sth][z][nat]{sec}. For now, it enables us to prove anintuitive result:\begin{prop}\ollabel{naturalnumbersarentinfinite}No natural number is Dedekind infinite.\end{prop}\begin{proof}The proof is by induction, i.e.,\olref[sfr][infinite][induction]{thm:dedinfiniteinduction}. Clearly $0= \emptyset$ is not Dedekind infinite. For the induction step, we willestablish the contrapositive: if (absurdly) $s(n)$ is Dedekindinfinite, then $n$ is Dedekind infinite. So suppose that $s(n)$ is Dedekind infinite, i.e., there is some!!{injection} $f$ with $\ran{f}\subsetneq \dom{f} = s(n) = n \cup\{n\}$. There are two cases to consider. \emph{Case 1: $n \notin \ran{f}$.} So $\ran{f} \subseteq n$, and $f(n) \in n$. Let $g = \funrestrictionto{f}{n}$; now $\ran{g} =\ran{f} \setminus \{f(n)\} \subsetneq n = \dom{g}$. Hence $n$ isDedekind infinite. \emph{Case 2: $n \in \ran{f}$.} Fix $m \in \dom{f} \setminus \ran{f}$, and define a function $h$ with domain $s(n) = n \cup \{n\}$:\[h(x) = 	\begin{cases}		f(x) & \text{if }f(x) \neq n\\		m & \text{if }f(x)=n	\end{cases}\]So $h$ and $f$ agree everywhere, except that $h(f^{-1}(n)) = m\neq n = f(f^{-1}(n))$. Since $f$ is !!a{injection}, $n \notin\ran{h}$; and $\ran{h} \subsetneq \dom{h} = s(n)$. Now $n$ isDedekind infinite, using the argument of Case 1.\end{proof}The question remains, though, of how we might \emph{justify} the Axiomof Infinity. The short answer is that we will need to add anotherprinciple to the story we have been telling. That principle is asfollows:\begin{enumerate}	\item[] \stagesinf. There is an infinite stage. That is, there is a stage which (a) is not the first stage, and which (b) has some stages before it, but which (c) has no immediate predecessor.\end{enumerate}The Axiom of Infinity follows straightforwardly from this principle.We know that natural number $n$ is formed at stage $n$. So the set$\omega$ is formed at the first infinite stage. And $\omega$ itselfwitnesses the Axiom of Infinity. This, however, simply pushes us back to the question of how we mightjustify \stagesinf. As with \stagessucc, it was not an explicit partof the story we told about the cumulative-iterative hierarchy. Butmore than that: nothing in the very idea of an iterative hierarchy, inwhich sets are formed stage by stage, forces us to think that theprocess involves an \emph{infinite} stage. It seems perfectly coherentto think that the stages are ordered like the natural numbers. This, however, gives rise to an obvious problem. In\olref[sfr][infinite][dedekindsproof]{sec}, we consideredDedekind's ``proof'' that there is a Dedekind infinite set (ofthoughts). This may not have struck you as very satisfying. But if\stagesinf{} is not ``forced upon us'' by the iterative conception ofset (or by ``the laws of thought''), then we are still left without anintrinsic justification for the claim that there is a Dedekindinfinite set.There is much more to say here, of course. But hopefully you are nowat a point to start thinking about what it might \emph{take} tojustify an axiom (or principle). In what follows we will simply take\stagesinf{} for granted.\end{document}

content/set-theory/z/milestone.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{milestone}\olsection{$\Z^-$: a Milestone}We will revisit \stagesinf{} in the next section. However, with theAxiom of Infinity, we have reached an important milestone. We now haveall the axioms required for the theory $\Zminus$. In detail:\begin{defn}The theory $\Zminus$ has these axioms: Extensionality, Union, Pairs, Powersets, Infinity, and all instances of the Separation scheme.\end{defn}The name stands for \emph{Zermelo} set theory (\emph{minus} somethingwhich we will come to later). Zermelo deserves the honour, since heessentially formulated this theory in his\citeyear{Zermelo1908Untersuchungen}.\footnote{For interestingcomments on the history and technicalities, see \citet[AppendixA]{Potter2004}.}This theory is powerful enough to allow us to do an enormous amount ofmathematics. In particular, you \emph{should} look back through\olref[sfr][][]{part}, and convince yourself that everything we did,na\"ively, could be done more formally within~$\Zminus$. (Once youhave done that for a bit, you might want to skip ahead and read\olref[sth][z][arbintersections]{sec}.) So, henceforth,and without any further comment, we will take ourselves to be workingin $\Zminus$ (at least).\end{document}

content/set-theory/z/nat.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}	\olfileid{sth}{z}{nat}\olsection{Selecting our Natural Numbers}%Let us take it for granted that the informal principle \stagesinf{}%can be justified. It is also, though, worth commenting on the%particular axiom we extracted from that informal principle. In \olref[infinity-again]{defnomega}, we explicitly definedthe expression ``natural numbers''. How should you understand thisstipulation? It is not a metaphysical claim, but just a decision to\emph{treat} certain sets as the natural numbers. We touched upon reasons for thinking this in\olref[sfr][rel][ref]{sec}, \olref[sfr][arith][ref]{sec} and\olref[sfr][infinite][dedekindsproof]{sec}. But we can make thesereasons even more pointed.Our Axiom of Infinity follows \citet{VonNeumann1925}. But here isanother axiom, which we could have adopted instead:\begin{defish}\emph{Zermelo's \citeyear{Zermelo1908Untersuchungen} Axiom ofInfinity.} There is a set $A$ such that $\emptyset \in A$ and$(\forall x \in A)\{x\} \in A$. \end{defish}Had we used Zermelo's axiom, instead of our (von Neumann-inspired)Axiom of Infinity, we would equally well have been given a Dedekindinfinite set, and so a Dedekind algebra. On Zermelo's approach, thedistinguished element of our algebra would again have been $\emptyset$(our surrogate for $0$), but the injection would have been given bythe map $x \mapsto \{x\}$, rather than $x \mapsto x \cup \{x\}$. Thesimplest upshot of this is that Zermelo treats $2$ as$\{\{\emptyset\}\}$, whereas we (with von Neumann) treat $2$ as$\{\emptyset, \{\emptyset\}\}$. Why choose one axiom of Infinity rather than the other? The mainpractical reason is that von Neumann's approach ``scales up'' tohandle transfinite numbers rather well. We will explore this from\olref[ordinals][]{chap} onwards. However, from the simpleperspective of \emph{doing arithmetic}, both approaches would doequally well. So if someone tells you that the natural numbers\emph{are} sets, the obvious question is: \emph{Which sets are they?} This precise question was made famous by \citet{Benacerraf1965}. Butit is worth emphasising that it is just the most famous example of aphenomenon that we have encountered many times already. The basicpoint is this. Set theory gives us a way to \emph{simulate} a bunch of``intuitive'' kinds of entities: the reals, rationals, integers, andnaturals, yes; but also ordered pairs, functions, and relations.However, set theory never provides us with a \emph{unique} choice ofsimulation. There are \emph{always} alternativeswhich---straightforwardly---would have served us just as well. \end{document}

content/set-theory/z/arbintersections.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{z}{arbintersections}\olsection{Appendix: Closure, Comprehension, and Intersection}In \olref[sth][z][milestone]{sec}, we suggested that you should lookback through the na\"ive work of \olref[sfr][][]{part} and check thatit can be carried out in~$\Zminus$. If you followed that advice,\emph{one} point might have tripped you up: the use of\emph{intersection} in Dedekind's treatment of \emph{closures}. Recall from \olref[sfr][infinite][dedekind]{Closure} that\begin{align*}  \closureofunder{f}{o} & = \bigcap\Setabs{X}{o \in X \text{ and $X$ is$f$-closed}}.\intertext{The general shape of this is a definition of the form:}  C & = \bigcap\Setabs{X}{\phi(X)}.\end{align*}But this should ring alarm bells: since Na\"ive Comprehension fails,there is no guarantee that $\Setabs{X}{\phi(X)}$ exists. It looksdangerously, then, like such definitions are \emph{cheating}. Fortunately, they are not cheating; or rather, if they \emph{are}cheating as they stand, then we can engage in some honest toil torender them kosher. That honest toil was foreshadowed in\olref[sth][z][sep]{prop:intersectionsexist}, when we explained why$\bigcap A$ exists for any $A \neq \emptyset$. But we will spell it outexplicitly.Given Extensionality, if we attempt to define $C$ as$\bigcap\Setabs{X}{\phi(X)}$, all we are really asking is for anobject $C$ which obeys the following:\begin{equation}\ollabel{bicondelimarbintersection}	\forall x(x \in C \liff \forall X(\phi(X) \lif x \in X))\tag{*}\end{equation}Now, suppose there is \emph{some} set, $S$, such that $\phi(S)$. Thento deliver \olref{bicondelimarbintersection}, we can simply define $C$using \emph{Separation}, as follows:\[	C = \Setabs{x \in S}{\forall X(\phi(X) \lif x \in X)}.\]We leave it as an exercise to check that this definition yields\olref{bicondelimarbintersection}, as desired. %  fix $x$. First suppose that $x \in C$, as (re)defined; then both $x%  \in S$ and $\forall X(\phi(X) \lif x \in X)$; but since%  $\phi(S)$, this reduces to the condition that $\forall X(\phi(X)%  \lif x \in X)$. Conversely, suppose $\forall X(\phi(X) \lif%  x \in X)$; then, since $\phi(S)$, we also have that $x \in S$; so%  $x \in c$, as (re)defined. And this general strategy will allow us to circumvent any apparent useof Na\"ive Comprehension in defining intersections. In the particularcase which got us started on this line of thought, namely that of$\closureofunder{f}{o}$, here is how that would work. We began theproof of \olref[sfr][infinite][dedekind]{closureproperties} by notingthat $o \in \ran{f}\cup\{o\}$ and that $\ran{f} \cup \{o\}$ is$f$-closed. So, we can define what we want thus:\[	\closureofunder{f}{o} = \Setabs{x \in \ran{f} \cup \{o\}}{(\forall X \ni o)(X \text{ is $f$-closed} \lif x \in X)}.\]\end{document}