Set Theory

Replacement

content/set-theory/replacement/replacement.tex

% Part: set-theory% Chapter: replacement\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{sth}{replacement}{Replacement}\olimport{introduction}\olimport{strength}\olimport{extrinsic}\olimport{limofsize}\olimport{absinf}\olimport{ref}\olimport{refproofs}\olimport{finiteaxiomatizability}\OLEndChapterHook\end{document}

content/set-theory/replacement/introduction.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{intro}\olsection{Introduction}Replacement is the axiom scheme which makes the difference between $\ZF$and~$\Z$. We helped ourselves to it throughout\crefrange{sth:ordinals::chap}{sth:spine::chap}. In this chapter, wewill finally consider the question: is Replacement justified? To make the question sharp, it is worth observing that Replacement is reallyrather \emph{strong}. We will get a sense of just how strong it is, during this chapter (and again in \olref[sth][card-arithmetic][fix]{sec}). But this will suggest that justification really is required. We will discuss two kinds of justification. Roughly: an \emph{extrinsic} justification is an attempt to justify an axiom by its fruits; an \emph{intrinsic} justification is an attempt to justify an axiom by suggesting that it is vindicated by the mathematical concepts in question. We will get a greater sense of what this means during this chapter, but it is just the tip of an iceberg. For more, see in particular \citeauthor{Maddy1988a} (\citeyear{Maddy1988a} and \citeyear{Maddy1988b}).\end{document}

content/set-theory/replacement/strength.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{strength}\olsection{The Strength of Replacement}We begin with a simple observation about the strength of Replacement: unless we go beyond $\Z$, we cannot prove the existence of any von Neumannordinal greater than or equal to $\omega + \omega$. Here is a sketch ofwhy. Working in~$\ZF$, consider the set $V_{\omega+\omega}$. This set actsas the domain for a \emph{model} for~$\Z$. To see this, we introduce some notation for the \emph{relativization} of a formula: \begin{defn}\ollabel{formularelativization}	For any set $M$, and any formula $\phi$, let $\phi^M$ be the formula which results by restricting all of $\phi$'s quantifiers to $M$. That is, replace ``$\lexists[x]$'' with ``$(\lexists[x \in M])$'', and	replace ``$\lforall[x]$'' with ``$(\lforall[x \in M])$''. \end{defn}\noindentIt can be shown that, for every axiom $\phi$ of~$\Z$, we have that $\ZF \vdash\phi^{V_{\omega+\omega}}$. But $\omega+\omega$ is not \emph{in}$V_{\omega+\omega}$, by  \olref[spine][rank]{ordsetrankalpha}. So $\Z$ isconsistent with the non-existence of $\omega+\omega$.This is why we said, in \olref[ordinals][replacement]{sec}, that\olref[ordinals][ordtype]{thmOrdinalRepresentation} cannot be provedwithout Replacement. For it is easy, within~$\Z$, to define anexplicit well-ordering which intuitively \emph{should} have order-type$\omega+\omega$. Indeed, we gave an informal example of this in\olref[ordinals][idea]{sec}, when we presented the ordering on thenatural numbers given by:\begin{align*}	n \lessdot m \text{ iff }&\text{either }n < m\text{ and }m-n\text{ is even,}\\	& \text{or $n$ is even and $m$ is odd.}\end{align*}But if $\omega+\omega$ does not exist, this well-ordering is notisomorphic to any ordinal. So $\Z$ does \emph{not} prove\olref[ordinals][ordtype]{thmOrdinalRepresentation}. Flipping things around: Replacement allows us to prove the existenceof $\omega+\omega$, and hence must allow us to prove the existence of$V_{\omega+\omega}$. And not just that. For \emph{any} well-orderingwe can define, \olref[ordinals][ordtype]{thmOrdinalRepresentation}tells us that there is some $\alpha$ isomorphic with thatwell-ordering, and hence that $V_\alpha$ exists. In a straightforwardway, then, Replacement guarantees that the hierarchy of sets must be\emph{very tall}. Over the next few sections, and then again in\olref[card-arithmetic][fix]{sec}, we'll get a better sense of betterjust \emph{how} tall Replacement forces the hierarchy to be. Thesimple point, for now, is that Replacement really \emph{does} stand inneed of justification!\end{document}

content/set-theory/replacement/extrinsic.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{extrinsic}\olsection[Extrinsic Considerations]{Extrinsic Considerations about Replacement}We start by considering an \emph{extrinsic} attempt to justifyReplacement. Boolos suggests one, as follows. \begin{quote}  [\ldots] the reason for adopting the axioms of replacement is quite  simple: they have many desirable consequences and (apparently) no  undesirable ones. In addition to theorems about the iterative  conception, the consequences include a satisfactory if not ideal  theory of infinite numbers, and a highly desirable result that  justifies inductive definitions on well-founded relations.  \citep[229]{Boolos1971}\end{quote}		The gist of Boolos's idea is that we should justify Replacement by itsfruits. And the specific fruits he mentions are the things we havediscussed in the past few chapters. Replacement allowed us to provethat the von Neumann ordinals were excellent surrogates for the ideaof a well-ordering type (this is our ``satisfactory if not idealtheory of infinite numbers''). Replacement also allowed us to definethe $V_\alpha$s, establish the notion of rank, and prove$\in$-Induction (this amounts to our ``theorems about the iterativeconception''). Finally, Replacement allows us to prove the TransfiniteRecursion Theorem (this is the ``inductive definitions on well-foundedrelations''). These are, indeed, desirable consequences. But do these desirableconsequences suffice to \emph{justify} Replacement? \emph{No}. Or atleast, not straightforwardly. Here is a simple problem. Whilst we have stated some desirableconsequences of Replacement, we could have obtained many of them viaother means. This is not as well known as it ought to be, though, so we should pause to explain the situation. There is a simple theory of sets, Level Theory, or $\LT$ for short.\footnote{The first versions of $\LT$ are offered by \citet{Montague1965} and \citet{Scott1974}; this was simplified, and given a book-length treatment, by \citet{Potter2004}; and \citet{ButtonLT1} has recently simplified $\LT$ further.} $\LT$'s axioms are just Extensionality, Separation, and the claim that every set is a subset of some \emph{level}, where ``level'' is cunningly defined so that the levels behave like our friends, the $V_\alpha$s. So $\ZF$ proves $\LT$; but $\LT$ is \emph{much} weaker than $\ZF$. In fact, $\LT$ does not give you Pairs, Powersets, Infinity, or Replacement. Let $\Zr$ be the result of adding Infinity and Powersets to $\LT$; this delivers Pairs too, so, $\Zr$ is at least as strong as $\Z$. But, in fact, $\Zr$ is strictly stronger than $\Z$, since it adds the claim that every set has a rank (hence my suggestion that we call it $\Zr$). Indeed, $\Zr$ delivers: a perfectly satisfactory theory of ordinals;results which stratify the hierarchy into well-ordered stages; a proofof $\in$-Induction; and a \emph{version} of Transfinite Recursion. Inshort: although Boolos didn't know this, all of the desirableconsequences which he mentions could have been arrived at\emph{without} Replacement; he simply needed to use $\Zr$ rather than $\Z$. (Given all of this, why did we follow the conventional route, ofteaching you $\ZF$, rather than $\LT$ and $\Zr$? There are two reasons. First: for purely historical reasons, starting with $\LT$ is rather nonstandard; we wanted toequip you to be able to read more standard discussions of set theory. Second: when you are ready toappreciate $\LT$ and $\Zr$, you can simply read \citealt{Potter2004} and \citealt{ButtonLT1}.)Of course, since $\Zr$ is strictly weaker than $\ZF$, there are results which$\ZF$ proves which $\Zr$ leaves open. So one could try to justifyReplacement on extrinsic grounds by pointing to one of these results.But, once you know how to use $\Zr$, it is quite hard to find manyexamples of things that are (a) settled by Replacement but nototherwise, and (b) are intuitively true. (For more on this, see\citealt[\S13.2]{Potter2004}.)The bottom line is this. To provide a compelling extrinsicjustification for Replacement, one would need to find a result which\emph{cannot} be achieved without Replacement. And that's not an easyenterprise. Let's consider a further problem which arises for any attempt to offera purely extrinsic justification for Replacement. (This problem isperhaps more fundamental than the first.) Boolos does not just pointout that Replacement has many desirable consequences. He also statesthat Replacement has ``(apparently) no undesirable'' consequences. Butthis parenthetical caveat, ``apparently,'' is surely absolutelycrucial.Recall how we ended up here: Na\"ive Comprehension ran intoinconsistency, and we responded to this inconsistency by embracing thecumulative-iterative conception of set. This conception comes equippedwith a story which, we hope, assures us of its consistency. But if wecannot justify Replacement from within that story, then we have (asyet) no reason to believe that $\ZF$ is consistent. Or rather: we haveno reason to believe that $\ZF$ is consistent, apart from the (perhapsmerely contingent) fact that no one has discovered a contradiction\emph{yet}. In exactly that sense, Boolos's comment seems to come downto this: ``(apparently) $\ZF$ is consistent''. We should demandgreater reassurance of consistency than this. This issue will affect any \emph{purely} extrinsic attempt to justifyReplacement, i.e., any justification which is couched solely in termsof the (known) consequences of $\ZF$. As such, we will want to lookfor an \emph{intrinsic} justification of Replacement, i.e., ajustification which suggests that the story which we told about setssomehow ``already'' commits us to Replacement. \end{document}

content/set-theory/replacement/limofsize.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{limofsize}\olsection{Limitation-of-size}Perhaps the most common attempt to offer an ``intrinsic'' justification ofReplacement comes via the following notion:\begin{enumerate}	\item[] \limofsize. Any things form a set, provided that there are	not too many of them.\end{enumerate}This principle will immediately vindicate Replacement. After all, anyset formed by Replacement cannot be any larger than any set from whichit was formed. Stated precisely: suppose you form a set$\funimage{\tau}{A} = \Setabs{\tau(x)}{x \in A}$ using Replacement;then $\cardle{\funimage{\tau}{A}}{A}$; so if the !!{element}s of $A$were not too numerous to form a set, their images are not too numerousto form $\funimage{\tau}{A}$. The obvious difficulty with invoking \limofsize{} to justifyReplacement is that we have \emph{not} yet laid down any principlelike \limofsize. Moreover, when we told our story about thecumulative-iterative conception of set in\crefrange{sth:story::chap}{sth:z::chap}, nothing ever \emph{hinted}in the direction of \limofsize. This, indeed, is precisely why Boolosat one point wrote: ``Perhaps one may conclude that there are at leasttwo thoughts `behind' set theory'' \citeyearpar[p.~19]{Boolos1989}. Onthe one hand, the ideas surrounding the cumulative-iterativeconception of set are meant to vindicate~$\Z$. On the other hand,\limofsize{} is meant to vindicate Replacement. But the issue it is not just that we have thus far been \emph{silent}about \limofsize. Rather, the issue is that \limofsize{} (as justformulated) seems to sit quite badly with the cumulative-iterativenotion of set. After all, it mentions nothing about the idea of setsas formed in \emph{stages}.This is really not much of a surprise, given the history of these``two thoughts'' (i.e., the cumulative-iterative conception of set,and \limofsize). These ``two thoughts'' ultimately amount to tworather  different projects for blocking the set-theoretic paradoxes.The cumulative-iterative notion of set blocks Russell's paradox bysaying, roughly: \emph{we should never have expected a Russell set toexist, because it would not be ``formed'' at any stage}. By contrast,\limofsize{} is meant to rule out the Russell set, by saying, roughly:\emph{we should never have expected a Russell set to exist, because itwould have been too big}. Put like this, then, let's be blunt: considered as a reply to theparadoxes, \limofsize{} stands in need of \emph{much} morejustification. Consider, for example, this version of Russell'sParadox: \emph{no pug sniffs exactly the pugs which don't sniffthemselves} (see \olref[sth][story][rus]{sec}). If you ask ``why is there no such pug?'', it is not agood answer to be told that such a pug would have to sniff too manypugs. So why would it be a good intuitive explanation, of thenon-existence of a Russell set, that it would have to be ``too big''to exist? In short, it's forgivable if you are a bit mystified concerning the ``intuitive''motivation for \limofsize. \end{document}

content/set-theory/replacement/absinf.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{absinf}\olsection{Replacement and ``Absolute Infinity''}We will now put \limofsize{} behind us, and explore a differentfamily of (intrinsic) attempts to justify Replacement, which do takeseriously the idea of the sets as formed in stages.When we first outlined the iterative process, we offered someprinciples which explained what happens at each stage. These were\stageshier, \stagesord, and \stagesacc. Later, we added someprinciples which told us something about the number of stages:\stagessucc{} told us that the process of set-formation never ends,and \stagesinf{} told us that the process goes through an infinite-thstage. It is reasonable to suggest that these two latter principles fall outof some a broader principle, like:\begin{enumerate}	\item[] \stagesinex. There are absolutely infinitely many stages;	the hierarchy is as tall as it could possibly be.\end{enumerate}Obviously this is an informal principle. But even if it is notimmediately \emph{entailed} by the cumulative-iterative conception ofset, it certainly seems \emph{consonant} with it. At the very least,and unlike \limofsize, it retains the idea that sets are formedstage-by-stage. The hope, now, is to leverage \stagesinex{} into a justification ofReplacement. So let us see how this might be done. In \olref[ordinals][idea]{sec}, we saw that it is easy toconstruct a well-ordering which (morally) should be isomorphic to$\omega+\omega$. Otherwise put, we can easily imagine a stage-by-stageiterative process, whose order-type (morally) is $\omega+\omega$. Assuch, if we have accepted \stagesinex, then we should surely acceptthat there is at least an $\omega+\omega$-th stage of the hierarchy,i.e., $V_{\omega+\omega}$, for the hierarchy surely \emph{could}continue thus far. This thought generalizes as follows: for any well-ordering, theprocess of building the iterative hierarchy should run at least as faras that well-ordering. And we could guarantee this, just by treating\olref[ordinals][ordtype]{thmOrdinalRepresentation} as an\emph{axiom}. This would tell us that any well-ordering is isomorphicto a von Neumann ordinal. Since each von Neumann ordinal will be equalto its own rank, \olref[ordinals][ordtype]{thmOrdinalRepresentation}will then tell us that, whenever we can describe a well-ordering inour set theory, the iterative process of set building must outrun thatwell-ordering. This idea certainly seems like a corollary of \stagesinex.Unfortunately, if our aim is to extract Replacement from this idea,then we face a simple, technical, barrier: Replacement is strictly stronger than\olref[ordinals][ordtype]{thmOrdinalRepresentation}. (This observation is made by \citet[\S13.2]{Potter2004}; we will prove it in \olref[sth][replacement][finiteaxiomatizability]{sec}.)The upshot is that, if we are going to understand \stagesinex{} insuch a way as to yield Replacement, then it cannot \emph{merely} saythat the hierarchy outruns any well-ordering. It must make a strongerclaim than that. To this end, \cite{Shoenfield:AST} proposed a verynatural strengthening of the idea, as follows: the hierarchy is not\emph{cofinal} with any set.\footnote{G\"odel seems to have proposed asimilar thought; see \citet[p.~223]{Potter2004}. For discussion of G\"odel and \citeauthor{Shoenfield:AST}, see \citet[90--5]{Incurvati2020}.} In slightly more detail:if $\tau$ is a mapping which sends sets to stages of the hierarchy,the image of any set $A$ under $\tau$ does not exhaust the hierarchy.Otherwise put (schematically): \begin{enumerate}	\item[] \stagescofin. If $A$ is a set and $\tau(x)$ is a stage for	every $x \in A$, then there is a stage which comes after each	$\tau(x)$ for $x \in A$.\end{enumerate}It is obvious that $\ZF$ proves a suitably formalised version of\stagescofin. Conversely, we can informally argue that \stagescofin{}justifies Replacement.\footnote{It would be harder to proveReplacement using some formalisation of \stagescofin, since $\Z$ onits own is not strong enough to define the stages, so it is not clearhow one would formalise \stagescofin. One option, though, is towork in some extension of $\LT$, as discussed in \olref[sth][replacement][extrinsic]{sec}.} For suppose $(\forall x \in A)\lexists![y][\phi(x,y)]$. Then for each $x \in A$, let $\sigma(x)$ be the $y$ suchthat $\phi(x,y)$, and let $\tau(x)$ be the stage at which $\sigma(x)$is first formed. By \stagescofin, there is a stage $V$ such that$(\forall x \in A)\tau(x)\in V$. Now since each $\tau(x) \in V$ and$\sigma(x) \subseteq \tau(x)$, by Separation we can obtain $\Setabs{y\in V}{(\exists x \in A)\sigma(x) = y} = \Setabs{y}{(\exists x \inA)\phi(x,y)}$.\begin{prob}	Formalize \stagescofin{} within $\ZF$.\end{prob}So \stagescofin{} vindicates Replacement. And it is at least plausiblethat \stagesinex{} vindicates \stagescofin. For suppose \stagescofin{}fails. So the hierarchy is cofinal with some set~$A$, i.e., we have amap $\tau$ such that for any stage~$S$ there is some $x \in A$ suchthat $S \in \tau(x)$. In that case, we do have a way to get a handleon the supposed ``absolute infinity'' of the hierarchy: it is\emph{exhausted} by the range of $\tau$ applied to $A$. And thatcompromises the thought that the hierarchy is ``absolutely infinite''.Contraposing: \stagesinex{} entails \stagescofin, which in turnjustifies Replacement.This represents a genuinely promising attempt to provide anintrinsic justification for Replacement. But whether it ultimatelyworks, or not, we will have to leave to you to decide.\end{document}

content/set-theory/replacement/ref.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{ref}\olsection{Replacement and Reflection}Our last attempt to justify Replacement, via \stagesinex, begins with a deep and lovely result:\footnote{A reminder: all formulas can have parameters (unless explicitly stated otherwise).}%In this, I will use overlining, such as $x_1, \ldots, x_n$, to%abbreviate ``$x_1, \ldots, x_n$'': \begin{thm}[Reflection Schema]\ollabel{reflectionschema}For any formula $\phi$:\[\forall \alpha \exists \beta > \alpha (\forall x_1 \ldots, x_n \inV_\beta)(\phi(x_1, \ldots, x_n) \liff \phi^{V_\beta}(x_1, \ldots, x_n))\]\end{thm}\noindent As in \olref[sth][replacement][strength]{formularelativization}, $\phi^{V_\beta}$ is the result of restricting everyquantifier in $\phi$ to the set~$V_\beta$. So, intuitively, Reflectionsays this: if $\phi$ is true in the entire hierarchy, then $\phi$ istrue in arbitrarily many \emph{initial segments} of the hierarchy. \citet{Montague1961} and \citet{Levy1960} showed that (suitableformulations of) Replacement and Reflection are equivalent,modulo~$\Z$, so that adding either gives you~$\ZF$. (We prove these results in \olref[sth][replacement][refproofs]{sec}.) Given thisequivalence, one might hope to justify Reflection  and Replacement via\stagesinex{} as follows: given \stagesinex, the hierarchy should bevery, very tall; so tall, in fact, that nothing we can say about it issufficient to bound its height. And we can understand this as thethought that, if any sentence~$\phi$ is true in the entire hierarchy,then it is true in arbitrarily many initial segments of the hierarchy.And that is just Reflection. Again, this seems like a genuinely promising attempt to provide anintrinsic justification for Replacement. But there is much too much tosay about it here. You must now decide for yourself whether itsucceeds.\footnote{Though you might like to continue by reading \citet[95--100]{Incurvati2020}.}\end{document}

content/set-theory/replacement/refproofs.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{sth}{replacement}{refproofs}\olsection{Appendix: Results surrounding Replacement}In this section, we will prove Reflection within $\ZF$. We will alsoprove a sense in which Reflection is equivalent to Replacement. And wewill prove an interesting consequence of all this, concerning thestrength of Reflection/Replacement. \emph{Warning: this is easily themost advanced bit of mathematics in this textbook.} We'll start with a lemma which, for brevity, employs the notationaldevice of \emph{overlining} to deal with sequences of variables orobjects. So: ``$\overline{a}_k$'' abbreviates ``$a_{k_1}$, \dots,$a_{k_n}$'', where $n$ is determined by context.\begin{lem}\ollabel{lemreflection}For each $1 \leq i \leq k$, let $\phi_i(\overline{v}_i, x)$ be aformula. Then for each $\alpha$there is some $\beta > \alpha$ such that, for any $\overline{a}_1,\ldots, \overline{a}_k \in V_\beta$ and each $1 \leq i \leq k$:\[	\exists x\phi_i(\overline{a}_i, x) \rightarrow (\exists x \in V_\beta) \phi_i(\overline{a}_i, x)\]\end{lem}\begin{proof}We define a term $\mu$ as follows: $\mu(\overline{a}_1, \ldots,\overline{a}_k)$ is the least stage, $V$, which satisfies all of thefollowing conditionals, for $1 \leq i \leq k$:\[\exists x\phi_i(\overline{a}_i, x) \rightarrow (\exists x \in V) \phi_i(\overline{a}_i, x))\]It is easy to confirm that $\mu(\overline{a}_1, \ldots, \overline{a}_k)$ exists for all $\overline{a}_1, \ldots, \overline{a}_k$. Now, using Replacement and our recursion theorem, define:\begin{align*}	S_0 & = V_{\alpha+1}\\	S_{n+1} & = S_n \cup \bigcup	\Setabs{\mu(\overline{a}_1, \ldots, \overline{a}_k)}	{\overline{a}_1, \ldots, \overline{a}_k \in S_n} \\	S &= \bigcup_{m < \omega} S_n.\end{align*}Each $S_n$, and hence $S$ itself, is a stage after $V_\alpha$. Now fix$\overline{a}_1$, \dots,~$\overline{a}_k \in S$; so there is some $n <\omega$ such that $\overline{a}_1$, \dots, $\overline{a}_k \in S_n$.Fix some $1 \leq i \leq k$, and suppose that $\exists x\phi_i(\overline{a}_i,x)$. So $(\exists x \in \mu(\overline{a}_1,\ldots, \overline{a}_k))\phi_i(\overline{a}_i, x)$ by construction, so$(\exists x \in S_{n+1})\phi_i(\overline{a}_i, x)$ and hence$(\exists x \in S)\phi_i(\overline{a}_i, x)$. So $S$ is our $V_\beta$.\end{proof}\noindent We can now prove \olref[sth][replacement][ref]{reflectionschema} quitestraightforwardly:\begin{proof}[Proof] Fix $\alpha$. Without loss of generality, we can assume $\phi$'s onlyconnectives are $\exists$, $\lnot$ and $\land$ (since these areexpressively adequate). Let $\psi_1, \ldots, \psi_k$ enumerate each of$\phi$'s subformulas according to complexity, so that $\psi_k = \phi$.By \olref{lemreflection}, there is a $\beta > \alpha$ such that, forany $\overline{a}_i \in V_\beta$ and each $1 \leq i \leq k$:\begin{align}\label{reflectionnicelybehaved}	\exists x\psi_i(\overline{a}_i, x) \rightarrow 	(\exists x \in V_\beta) \psi_i(\overline{a}_i, x)\tag{*}\end{align}By induction on complexity of $\psi_i$, we will show that$\psi_i(\overline{a}_i) \leftrightarrow\psi_i^{V_\beta}(\overline{a}_i)$, for any  $\overline{a}_i \inV_\beta$. 	If $\psi_i$ is atomic, this is trivial. The biconditionalalso establishes that, when $\psi_i$ is a negation or conjunction ofsubformulas satisfying this property, $\psi_i$ itself satisfies thisproperty. So the only interesting case concerns quantification. Fix$\overline{a}_i \in V_\beta$; then:\begin{align*}	(\exists x \psi_i(\overline{a}_i, x))^{V_\beta}	&\text{ iff }	(\exists x \in V_\beta)\psi_i^{V_\beta}(\overline{a}_i, x)	&&\text{by definition}\\	&\text{ iff }	(\exists x \in V_\beta)\psi_i(\overline{a}_i,  x)	&&\text{by hypothesis}\\	&\text{ iff }	\exists x \psi_i(\overline{a}_i, x)	&&\text{by \eqref{reflectionnicelybehaved}}\end{align*}This completes the induction; the result follows as $\psi_k = \phi$.\end{proof}We have proved Reflection in $\ZF$. Our proof essentiallyfollowed \citet{Montague1961}. We now want to prove in $\Z$ thatReflection entails Replacement. The proof follows \citet{Levy1960},but with a simplification. Since we are working in $\Z$, we cannot present Reflection in exactlythe form given above. After all, we formulated Reflection using the``$V_\alpha$'' notation, and that cannot be defined in $\Z$ (see\olref[sth][spine][zf]{sec}). So instead we will offer an apparentlyweaker formulation of Replacement, as follows:\begin{defish}\emph{Weak-Reflection.} For any formula $\phi$, there is a transitiveset $S$ such that $0$, $1$, and any parameters to $\phi$ are!!{element}s of $S$, and $(\forall \overline{x} \in S)(\phi \liff\phi^S)$.\end{defish}To use this to prove Replacement, we will first follow \citet[firstpart of Theorem 2]{Levy1960} and show that we can ``reflect'' twoformulas at once:\begin{lem}[in $\Z + \text{Weak-Reflection}$.]\ollabel{lem:reflect}For any formulas $\psi, \chi$, there is a transitive set $S$ such that$0$ and $1$ (and any parameters to the formulas) are !!{element}s of$S$, and $(\forall \overline{x} \in S)((\psi \liff \psi^S) \land (\chi\liff \chi^S))$.\end{lem}\begin{proof}Let $\phi$ be the formula $(z = 0 \land \psi) \lor (z = 1 \land \chi)$. Here we use an abbreviation; we should spell out ``$z = 0$'' as``$\forall t\, t \notin z$'' and ``$z =1$'' as ``$\forall s(s \in z\liff \forall t\, t \notin s)$''. But since $0, 1 \in S$ and $S$ istransitive, these formulas are \emph{absolute} for $S$; that is, theywill apply to the same object whether we restrict their quantifiers to$S$.\footnote{More formally, letting $\xi$ be either of theseformulas, $\xi(z) \liff \xi^S(z)$.}By Weak-Reflection, we have some appropriate $S$ such that:\begin{align*}	(\forall z, \overline{x} \in S)(&\phi \liff \phi^S)\\	\text{i.e. }(\forall z, \overline{x} \in S)(&((z = 0 \land \psi) \lor (z = 1 \land \chi)) \liff {}\\	&\phantom{(}((z = 0 \land \psi) \lor (z = 1 \land \chi))^S)\\	\text{i.e. }(\forall z, \overline{x} \in S)(&((z = 0 \land \psi) \lor (z = 1 \land \chi))\liff {}\\	&\phantom{(}((z = 0 \land \psi^S) \lor (z = 1 \land \chi^S)))\\	\text{i.e. }(\forall \overline{x} \in S)(&(\psi \liff \psi^S) \land (\chi \liff \chi^S))\end{align*}The second claim entails the third because ``$z = 0$'' and ``$z=1$''are absolute for $S$; the fourth claim follows since $0 \neq 1$.\end{proof}\noindent We can now obtain Replacement, just by following and simplifying \citet[Theorem 6]{Levy1960}:\begin{thm}[in $\Z$ + Weak-Reflection]\label{thm:replacement} For any formula $\phi(v,w)$, and any $A$, if $(\forall x \in A)\lexists![y][\phi(x,y)]$, then$\Setabs{y}{(\exists x \in A)\phi(x,y}$ exists.\end{thm}\begin{proof}Fix $A$ such that $(\forall x \in A)\lexists![y][\phi(x,y)]$, anddefine formulas:\begin{align*}	\psi &\text{ is } (\phi(x, z) \land A = A)\\	\chi &\text{ is } \lexists[y][\phi(x, y)]\end{align*}Using \olref{lem:reflect}, since $A$ is a parameter to $\psi$, thereis a transitive~$S$ such that $0, 1, A \in S$  (along with any otherparameters), and such that:\[	(\forall x,z \in S)((\psi \liff \psi^S) \land (\chi \liff \chi^S))\]So in particular:\begin{align*}	(\forall  x, z \in S)(&\phi(x, z) \liff \phi^S(x, z))\\	(\forall x \in S)(&\exists y\phi(x, y) \liff (\exists y \in S)\phi^S(x, y)) \end{align*}Combining these, and observing that $A \subseteq S$ since $A \in S$ and $S$ is transitive:\begin{align*}	(\forall x \in A)(&\exists y\phi(x, y) \liff (\exists y \in S)\phi(x, y))\end{align*}Now $(\forall x \in A)(\lexists![y \in S])\phi(x, y)$, because$(\forall x \in A)\lexists![y][\phi(x, y)]$. Now Separation yields$\Setabs{y \in S}{(\exists x \in A) \phi(x, y)} = \Setabs{y}{(\existsx \in A) \phi(x, y)}$. \end{proof}\end{document}

content/set-theory/replacement/finiteaxiomatizability.tex

\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}	\olfileid{sth}{replacement}{finiteaxiomatizability}\olsection{Appendix: Finite axiomatizability}We close this chapter by extracting some results from Replacement. The first result is due to \citet{Montague1961}; note that it is not a proof \emph{within} $\ZF$, but a proof \emph{about} $\ZF$:\begin{thm}\ollabel{zfnotfinitely}	$\ZF$ is not finitely axiomatizable. More generally: if $\Th{T}$ is finite and $\Th{T} \Proves \ZF$, then $\Th{T}$ is inconsistent.		(Here, we tacitly restrict ourselves to first-order sentences whose only non-logical primitive is $\in$, and we write $\Th{T} \Proves \ZF$ to indicate that $\Th{T} \Proves \phi$ for all $\phi \in \ZF$.)\end{thm}\begin{proof}	Fix finite $\Th{T}$ such that $\Th{T} \Proves \ZF$. So, $\Th{T}$ proves Reflection, i.e.\ \olref[sth][replacement][ref]{reflectionschema}. Since $\Th{T}$ is finite, we can rewrite it as a single conjunction, $\theta$. Reflecting with this formula, $\Th{T} \Proves \exists \beta(\theta \liff \theta^{V_\beta})$. Since trivially $\Th{T} \Proves \theta$, we find that $\Th{T} \Proves \exists \beta\ \theta^{V_\beta}$. 		Now, let $\psi(X)$ abbreviate:	\[		\theta^X \land X\text{ is transitive} \land (\forall Y \in X)(Y\text{ is transitive}\lif \lnot \theta^{Y})	\]	roughly this says: $X$ is a transitive model of $\theta$, and $\in$-minimal in this regard. Now, recalling that $\Th{T} \Proves \exists \beta\ \theta^{V_\beta}$, by basic facts about ranks within $\ZF$ and hence within $\Th{T}$, we have:	\begin{equation}		\Th{T} \Proves \exists M \psi(M). \tag{*}\label{Mpsi}	\end{equation}	Using the first conjunct of $\psi(X)$, whenever $\Th{T} \Proves \sigma$, we have that $\Th{T} \Proves \forall X(\psi(X) \lif \sigma^X)$. So, by \eqref{Mpsi}:	\begin{align*}		\Th{T} &\Proves \forall X(\psi(X) \lif (\exists N \psi(N))^X)\\	\intertext{Using this, and \eqref{Mpsi} again:}		\Th{T} &\Proves \exists M(\psi(M) \land (\exists N \psi(N))^M)	\intertext{In particular, then:}		\Th{T} &\Proves \exists M(\psi(M) \land (\exists N \in M)((N\text{ is transitive})^N \land (\theta^N)^M))	\intertext{So, by elementary reasoning concerning transitivity:}		\Th{T} &\Proves \exists M(\psi(M) \land (\exists N \in M)(N\text{ is transitive} \land \theta^N))	\end{align*} 	So that $\Th{T}$ is inconsistent.\footnote{This ``elementary reasoning'' involves proving certain ``absoluteness facts'' for transitive sets.}\end{proof}Here is a similar result, noted by \citet[223]{Potter2004}:\begin{prop}\ollabel{finiteextensionofZ}	Let $\Th{T}$ extend $\Z$ with finitely many new axioms. If $\Th{T} \Proves \ZF$, then $\Th{T}$ is inconsistent. (Here we use the same tacit restrictions as for \olref{zfnotfinitely}.)\end{prop}\begin{proof}	Use $\theta$ for the conjunction of all of $\Th{T}$'s axioms \emph{except} for the (infinitely many) instances of Separation. Defining $\psi$ from $\theta$ as in \olref{zfnotfinitely}, we can show that $\Th{T} \Proves \exists M \psi(M)$. 		As in \olref{zfnotfinitely}, we can establish the schema that, whenever $\Th{T} \Proves \sigma$, we have that $\Th{T} \Proves \forall X(\psi(X) \lif \sigma^X)$. We then finish our proof, exactly as in \olref{zfnotfinitely}.		However, establishing the schema involves a little more work than in \olref{zfnotfinitely}. After all, the Separation-instances are in $\Th{T}$, but they are not conjuncts of $\theta$. However, we can overcome this obstacle by proving that $\Th{T} \Proves \forall X(X\text{ is transitive} \lif \sigma^X)$, for every Separation-instance $\sigma$. We leave this to the reader. \end{proof}\begin{prob}	Show that, for every Separation-instance $\sigma$, we have: $\Z \Proves \forall X(X\text{ is transitive} \lif \sigma^X)$. (We used this schema in \olref[sth][replacement][finiteaxiomatizability]{finiteextensionofZ}.)\end{prob}\begin{prob}	Show that, for every $\phi \in \Z$, we have $\ZF \Proves \phi^{V_{\omega+\omega}}$.\end{prob}\begin{prob}	Confirm the remaining schematic results invoked in the proofs of \olref[sth][replacement][finiteaxiomatizability]{zfnotfinitely} and  \olref[sth][replacement][finiteaxiomatizability]{finiteextensionofZ}.\end{prob}As remarked in \olref[sth][replacement][absinf]{sec}, this shows that Replacement is strictly stronger than\olref[ordinals][ordtype]{thmOrdinalRepresentation}. Or, slightly more strictly: if $\Z$ + ``every well-ordering is isomorphic to a unique ordinal'' is consistent, then it fails to prove some Replacement-instance.	%	By assumption, $\psi^{V_\alpha}$ has the form: 	%	\[	%		(\forall A \in V_\alpha)(\exists S \in V_\alpha)(\forall x \in V_\alpha)(x \in S \liff (\phi^{V_\alpha}(x) \land x \in A))	%	\]	%	To establish this holds, fix $A \in V_\alpha$. Using Separation, obtain: 	%	\[	%		S = \Setabs{x \in A}{\phi^{V_\alpha}(x)}	%	\]	%	Now $S \in V_\alpha$, since $S \subseteq A \in V_\alpha$, and clearly $(\forall x \in V_\alpha)(x \in S \liff (\phi^{V_\alpha}(x) \land x \in A)$.\end{document}