Set Theory

Replacement

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Introduction

Replacement is the axiom scheme which makes the difference between ZF\ZFsource and Z\Zsource. We helped ourselves to it throughout chapters “Ordinals” through “Stages and Ranks”. In this chapter, we will finally consider the question: is Replacement justified?

To make the question sharp, it is worth observing that Replacement is really rather strong. We will get a sense of just how strong it is, during this chapter (and again in section “ℵ-Fixed Points” in chapter “Cardinal Arithmetic”). But this will suggest that justification really is required.

We will discuss two kinds of justification. Roughly: an extrinsic justification is an attempt to justify an axiom by its fruits; an 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 Penelope Maddy (1988 and 1988).

The Strength of Replacement

We begin with a simple observation about the strength of Replacement: unless we go beyond Z\Zsource, we cannot prove the existence of any von Neumann ordinal greater than or equal to ω+ω\omega + \omegasource.

Here is a sketch of why. Working in ZF\ZFsource, consider the set Vω+ωV_{\omega+\omega}source. This set acts as the domain for a model for Z\Zsource. To see this, we introduce some notation for the relativization of a formula:

Definition one in this chapter

For any set MMsource, and any formula ϕ\phisource, let ϕM\phi^Msource be the formula which results by restricting all of ϕ\phisource's quantifiers to MMsource. That is, replace “∃x\lexists[x]source” with “(∃x∈M)(\lexists[x \in M])source”, and replace “∀x\lforall[x]source” with “(∀x∈M)(\lforall[x \in M])source”.

noindent It can be shown that, for every axiom ϕ\phisource of Z\Zsource, we have that ZF⊢ϕVω+ω\ZF \vdash \phi^{V_{\omega+\omega}}source. But ω+ω\omega+\omegasource is not in Vω+ωV_{\omega+\omega}source, by corollary two in chapter “Stages and Ranks”. So Z\Zsource is consistent with the non-existence of ω+ω\omega+\omegasource.

This is why we said, in section “Replacement” in chapter “Ordinals”, that theorem five in chapter “Ordinals” cannot be proved without Replacement. For it is easy, within Z\Zsource, to define an explicit well-ordering which intuitively should have order-type ω+ω\omega+\omegasource. Indeed, we gave an informal example of this in section “The General Idea of an Ordinal” in chapter “Ordinals”, when we presented the ordering on the natural numbers given by:

n⋖m iff either n<m and m−n is even,or n is even and m is odd.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.}source

But if ω+ω\omega+\omegasource does not exist, this well-ordering is not isomorphic to any ordinal. So Z\Zsource does not prove theorem five in chapter “Ordinals”.

Flipping things around: Replacement allows us to prove the existence of ω+ω\omega+\omegasource, and hence must allow us to prove the existence of Vω+ωV_{\omega+\omega}source. And not just that. For any well-ordering we can define, theorem five in chapter “Ordinals” tells us that there is some α\alphasource isomorphic with that well-ordering, and hence that VαV_\alphasource exists. In a straightforward way, then, Replacement guarantees that the hierarchy of sets must be very tall.

Over the next few sections, and then again in section “ℵ-Fixed Points” in chapter “Cardinal Arithmetic”, we'll get a better sense of better just how tall Replacement forces the hierarchy to be. The simple point, for now, is that Replacement really does stand in need of justification!

Extrinsic Considerations about Replacement

We start by considering an extrinsic attempt to justify Replacement. Boolos suggests one, as follows.

[…] 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. (George Boolos, 1971, 229)

The gist of Boolos's idea is that we should justify Replacement by its fruits. And the specific fruits he mentions are the things we have discussed in the past few chapters. Replacement allowed us to prove that the von Neumann ordinals were excellent surrogates for the idea of a well-ordering type (this is our “satisfactory if not ideal theory of infinite numbers”). Replacement also allowed us to define the VαV_\alphasources, establish the notion of rank, and prove ∈\insource-Induction (this amounts to our “theorems about the iterative conception”). Finally, Replacement allows us to prove the Transfinite Recursion Theorem (this is the “inductive definitions on well-founded relations”).

These are, indeed, desirable consequences. But do these desirable consequences suffice to justify Replacement? No. Or at least, not straightforwardly.

Here is a simple problem. Whilst we have stated some desirable consequences of Replacement, we could have obtained many of them via other 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\LTsource for short.Footnote: The first versions of LT\LTsource are offered by Richard Montague (1965) and Dana Scott (1974); this was simplified, and given a book-length treatment, by Michael Potter (2004); and Tim Button (2021) has recently simplified LT\LTsource further. LT\LTsource's axioms are just Extensionality, Separation, and the claim that every set is a subset of some level, where “level” is cunningly defined so that the levels behave like our friends, the VαV_\alphasources. So ZF\ZFsource proves LT\LTsource; but LT\LTsource is much weaker than ZF\ZFsource. In fact, LT\LTsource does not give you Pairs, Powersets, Infinity, or Replacement. Let Zr\Zrsource be the result of adding Infinity and Powersets to LT\LTsource; this delivers Pairs too, so, Zr\Zrsource is at least as strong as Z\Zsource. But, in fact, Zr\Zrsource is strictly stronger than Z\Zsource, since it adds the claim that every set has a rank (hence my suggestion that we call it Zr\Zrsource). Indeed, Zr\Zrsource delivers: a perfectly satisfactory theory of ordinals; results which stratify the hierarchy into well-ordered stages; a proof of ∈\insource-Induction; and a version of Transfinite Recursion.

In short: although Boolos didn't know this, all of the desirable consequences which he mentions could have been arrived at without Replacement; he simply needed to use Zr\Zrsource rather than Z\Zsource.

(Given all of this, why did we follow the conventional route, of teaching you ZF\ZFsource, rather than LT\LTsource and Zr\Zrsource? There are two reasons. First: for purely historical reasons, starting with LT\LTsource is rather nonstandard; we wanted to equip you to be able to read more standard discussions of set theory. Second: when you are ready to appreciate LT\LTsource and Zr\Zrsource, you can simply read Michael Potter 2004 and Tim Button 2021.)

Of course, since Zr\Zrsource is strictly weaker than ZF\ZFsource, there are results which ZF\ZFsource proves which Zr\Zrsource leaves open. So one could try to justify Replacement on extrinsic grounds by pointing to one of these results. But, once you know how to use Zr\Zrsource, it is quite hard to find many examples of things that are (a) settled by Replacement but not otherwise, and (b) are intuitively true. (For more on this, see Michael Potter 2004, §13.2.)

The bottom line is this. To provide a compelling extrinsic justification for Replacement, one would need to find a result which cannot be achieved without Replacement. And that's not an easy enterprise.

Let's consider a further problem which arises for any attempt to offer a purely extrinsic justification for Replacement. (This problem is perhaps more fundamental than the first.) Boolos does not just point out that Replacement has many desirable consequences. He also states that Replacement has “(apparently) no undesirable” consequences. But this parenthetical caveat, “apparently,” is surely absolutely crucial.

Recall how we ended up here: Naïve Comprehension ran into inconsistency, and we responded to this inconsistency by embracing the cumulative-iterative conception of set. This conception comes equipped with a story which, we hope, assures us of its consistency. But if we cannot justify Replacement from within that story, then we have (as yet) no reason to believe that ZF\ZFsource is consistent. Or rather: we have no reason to believe that ZF\ZFsource is consistent, apart from the (perhaps merely contingent) fact that no one has discovered a contradiction yet. In exactly that sense, Boolos's comment seems to come down to this: “(apparently) ZF\ZFsource is consistent”. We should demand greater reassurance of consistency than this.

This issue will affect any purely extrinsic attempt to justify Replacement, i.e., any justification which is couched solely in terms of the (known) consequences of ZF\ZFsource. As such, we will want to look for an intrinsic justification of Replacement, i.e., a justification which suggests that the story which we told about sets somehow “already” commits us to Replacement.

Limitation-of-size

Perhaps the most common attempt to offer an “intrinsic” justification of Replacement comes via the following notion:

  1. limofsize. Any things form a set, provided that there are not too many of them.

This principle will immediately vindicate Replacement. After all, any set formed by Replacement cannot be any larger than any set from which it was formed. Stated precisely: suppose you form a set τ[A]={τ(x):x∈A}\funimage{\tau}{A} = \Setabs{\tau(x)}{x \in A}source using Replacement; then τ[A]≼A\cardle{\funimage{\tau}{A}}{A}source; so if the elements of AAsource were not too numerous to form a set, their images are not too numerous to form τ[A]\funimage{\tau}{A}source.

The obvious difficulty with invoking limofsize to justify Replacement is that we have not yet laid down any principle like limofsize. Moreover, when we told our story about the cumulative-iterative conception of set in chapters “The Iterative Conception” through “Steps towards Z”, nothing ever hinted in the direction of limofsize. This, indeed, is precisely why Boolos at one point wrote: “Perhaps one may conclude that there are at least two thoughts `behind' set theory” (1989, p. 19). On the one hand, the ideas surrounding the cumulative-iterative conception of set are meant to vindicate Z\Zsource. On the other hand, limofsize is meant to vindicate Replacement.

But the issue it is not just that we have thus far been silent about limofsize. Rather, the issue is that limofsize (as just formulated) seems to sit quite badly with the cumulative-iterative notion of set. After all, it mentions nothing about the idea of sets as formed in 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 two rather different projects for blocking the set-theoretic paradoxes. The cumulative-iterative notion of set blocks Russell's paradox by saying, roughly: we should never have expected a Russell set to exist, because it would not be “formed” at any stage. By contrast, limofsize is meant to rule out the Russell set, by saying, roughly: we should never have expected a Russell set to exist, because it would have been too big.

Put like this, then, let's be blunt: considered as a reply to the paradoxes, limofsize stands in need of much more justification. Consider, for example, this version of Russell's Paradox: no pug sniffs exactly the pugs which don't sniff themselves (see section “Russell's Paradox (again)” in chapter “The Iterative Conception”). If you ask “why is there no such pug?”, it is not a good answer to be told that such a pug would have to sniff too many pugs. So why would it be a good intuitive explanation, of the non-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.

Replacement and “Absolute Infinity”

We will now put limofsize behind us, and explore a different family of (intrinsic) attempts to justify Replacement, which do take seriously the idea of the sets as formed in stages.

When we first outlined the iterative process, we offered some principles which explained what happens at each stage. These were stageshier, stagesord, and stagesacc. Later, we added some principles 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-th stage.

It is reasonable to suggest that these two latter principles fall out of some a broader principle, like:

  1. stagesinex. There are absolutely infinitely many stages; the hierarchy is as tall as it could possibly be.

Obviously this is an informal principle. But even if it is not immediately entailed by the cumulative-iterative conception of set, it certainly seems consonant with it. At the very least, and unlike limofsize, it retains the idea that sets are formed stage-by-stage.

The hope, now, is to leverage stagesinex into a justification of Replacement. So let us see how this might be done.

In section “The General Idea of an Ordinal” in chapter “Ordinals”, we saw that it is easy to construct a well-ordering which (morally) should be isomorphic to ω+ω\omega+\omegasource. Otherwise put, we can easily imagine a stage-by-stage iterative process, whose order-type (morally) is ω+ω\omega+\omegasource. As such, if we have accepted stagesinex, then we should surely accept that there is at least an ω+ω\omega+\omegasource-th stage of the hierarchy, i.e., Vω+ωV_{\omega+\omega}source, for the hierarchy surely could continue thus far.

This thought generalizes as follows: for any well-ordering, the process of building the iterative hierarchy should run at least as far as that well-ordering. And we could guarantee this, just by treating theorem five in chapter “Ordinals” as an axiom. This would tell us that any well-ordering is isomorphic to a von Neumann ordinal. Since each von Neumann ordinal will be equal to its own rank, theorem five in chapter “Ordinals” will then tell us that, whenever we can describe a well-ordering in our set theory, the iterative process of set building must outrun that well-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 theorem five in chapter “Ordinals”. (This observation is made by Michael Potter (2004), §13.2; we will prove it in section “Appendix: Finite axiomatizability” in chapter “Replacement”.)

The upshot is that, if we are going to understand stagesinex in such a way as to yield Replacement, then it cannot merely say that the hierarchy outruns any well-ordering. It must make a stronger claim than that. To this end, Joseph R. Shoenfield (1977) proposed a very natural strengthening of the idea, as follows: the hierarchy is not cofinal with any set.Footnote: Gödel seems to have proposed a similar thought; see Michael Potter (2004), p. 223. For discussion of Gödel and Joseph R. Shoenfield, see Luca Incurvati (2020), 90–5. In slightly more detail: if τ\tausource is a mapping which sends sets to stages of the hierarchy, the image of any set AAsource under τ\tausource does not exhaust the hierarchy. Otherwise put (schematically):

  1. stagescofin. If AAsource is a set and τ(x)\tau(x)source is a stage for every x∈Ax \in Asource, then there is a stage which comes after each τ(x)\tau(x)source for x∈Ax \in Asource.

It is obvious that ZF\ZFsource proves a suitably formalised version of stagescofin. Conversely, we can informally argue that stagescofin justifies Replacement.Footnote: It would be harder to prove Replacement using some formalisation of stagescofin, since Z\Zsource on its own is not strong enough to define the stages, so it is not clear how one would formalise stagescofin. One option, though, is to work in some extension of LT\LTsource, as discussed in section “Extrinsic Considerations about Replacement” in chapter “Replacement”. For suppose (∀x∈A)∃!yϕ(x,y)(\forall x \in A)\lexists![y][\phi(x,y)]source. Then for each x∈Ax \in Asource, let σ(x)\sigma(x)source be the yysource such that ϕ(x,y)\phi(x,y)source, and let τ(x)\tau(x)source be the stage at which σ(x)\sigma(x)source is first formed. By stagescofin, there is a stage VVsource such that (∀x∈A)τ(x)∈V(\forall x \in A)\tau(x)\in Vsource. Now since each τ(x)∈V\tau(x) \in Vsource and σ(x)⊆τ(x)\sigma(x) \subseteq \tau(x)source, by Separation we can obtain {y∈V:(∃x∈A)σ(x)=y}={y:(∃x∈A)ϕ(x,y)}\Setabs{y \in V}{(\exists x \in A)\sigma(x) = y} = \Setabs{y}{(\exists x \in A)\phi(x,y)}source.

Exercise one in this chapter

Formalize stagescofin within ZF\ZFsource.

So stagescofin vindicates Replacement. And it is at least plausible that stagesinex vindicates stagescofin. For suppose stagescofin fails. So the hierarchy is cofinal with some set AAsource, i.e., we have a map τ\tausource such that for any stage SSsource there is some x∈Ax \in Asource such that S∈τ(x)S \in \tau(x)source. In that case, we do have a way to get a handle on the supposed “absolute infinity” of the hierarchy: it is exhausted by the range of τ\tausource applied to AAsource. And that compromises the thought that the hierarchy is “absolutely infinite”. Contraposing: stagesinex entails stagescofin, which in turn justifies Replacement.

This represents a genuinely promising attempt to provide an intrinsic justification for Replacement. But whether it ultimately works, or not, we will have to leave to you to decide.

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).

Theorem: Reflection Schema

[Reflection Schema] For any formula ϕ\phisource:

∀α∃β>α(∀x1…,xn∈Vβ)(ϕ(x1,…,xn)↔ϕVβ(x1,…,xn))\forall \alpha \exists \beta > \alpha (\forall x_1 \ldots, x_n \in V_\beta)(\phi(x_1, \ldots, x_n) \liff \phi^{V_\beta}(x_1, \ldots, x_n))source

noindent As in definition one in chapter “Replacement”, ϕVβ\phi^{V_\beta}source is the result of restricting every quantifier in ϕ\phisource to the set VβV_\betasource. So, intuitively, Reflection says this: if ϕ\phisource is true in the entire hierarchy, then ϕ\phisource is true in arbitrarily many initial segments of the hierarchy.

Richard Montague (1961) and Azriel Lévy (1960) showed that (suitable formulations of) Replacement and Reflection are equivalent, modulo Z\Zsource, so that adding either gives you ZF\ZFsource. (We prove these results in section “Appendix: Results surrounding Replacement” in chapter “Replacement”.) Given this equivalence, one might hope to justify Reflection and Replacement via stagesinex as follows: given stagesinex, the hierarchy should be very, very tall; so tall, in fact, that nothing we can say about it is sufficient to bound its height. And we can understand this as the thought that, if any sentence ϕ\phisource 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 an intrinsic justification for Replacement. But there is much too much to say about it here. You must now decide for yourself whether it succeeds.Footnote: Though you might like to continue by reading Luca Incurvati (2020), 95–100.

Appendix: Results surrounding Replacement

In this section, we will prove Reflection within ZF\ZFsource. We will also prove a sense in which Reflection is equivalent to Replacement. And we will prove an interesting consequence of all this, concerning the strength of Reflection/Replacement. Warning: this is easily the most advanced bit of mathematics in this textbook.

We'll start with a lemma which, for brevity, employs the notational device of overlining to deal with sequences of variables or objects. So: “a¯k\overline{a}_ksource” abbreviates “ak1a_{k_1}source, dots, akna_{k_n}source”, where nnsource is determined by context.

Lemma one in this chapter

For each 1≤i≤k1 \leq i \leq ksource, let ϕi(v¯i,x)\phi_i(\overline{v}_i, x)source be a formula. Then for each α\alphasource there is some β>α\beta > \alphasource such that, for any a¯1,…,a¯k∈Vβ\overline{a}_1, \ldots, \overline{a}_k \in V_\betasource and each 1≤i≤k1 \leq i \leq ksource:

∃xϕi(a¯i,x)→(∃x∈Vβ)ϕi(a¯i,x)\exists x\phi_i(\overline{a}_i, x) \rightarrow (\exists x \in V_\beta) \phi_i(\overline{a}_i, x)source

Proof

We define a term μ\musource as follows: μ(a¯1,…,a¯k)\mu(\overline{a}_1, \ldots, \overline{a}_k)source is the least stage, VVsource, which satisfies all of the following conditionals, for 1≤i≤k1 \leq i \leq ksource:

∃xϕi(a¯i,x)→(∃x∈V)ϕi(a¯i,x))\exists x\phi_i(\overline{a}_i, x) \rightarrow (\exists x \in V) \phi_i(\overline{a}_i, x))source

It is easy to confirm that μ(a¯1,…,a¯k)\mu(\overline{a}_1, \ldots, \overline{a}_k)source exists for all a¯1,…,a¯k\overline{a}_1, \ldots, \overline{a}_ksource. Now, using Replacement and our recursion theorem, define:

S0=Vα+1Sn+1=Sn∪⋃{μ(a¯1,…,a¯k):a¯1,…,a¯k∈Sn}S=⋃m<ωSn.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.source

Each SnS_nsource, and hence SSsource itself, is a stage after VαV_\alphasource. Now fix a¯1\overline{a}_1source, dots, a¯k∈S\overline{a}_k \in Ssource; so there is some n<ωn < \omegasource such that a¯1\overline{a}_1source, dots, a¯k∈Sn\overline{a}_k \in S_nsource. Fix some 1≤i≤k1 \leq i \leq ksource, and suppose that ∃xϕi(a¯i,x)\exists x \phi_i(\overline{a}_i,x)source. So (∃x∈μ(a¯1,…,a¯k))ϕi(a¯i,x)(\exists x \in \mu(\overline{a}_1, \ldots, \overline{a}_k))\phi_i(\overline{a}_i, x)source by construction, so (∃x∈Sn+1)ϕi(a¯i,x)(\exists x \in S_{n+1})\phi_i(\overline{a}_i, x)source and hence (∃x∈S)ϕi(a¯i,x)(\exists x \in S)\phi_i(\overline{a}_i, x)source. So SSsource is our VβV_\betasource.

noindent We can now prove theorem “Reflection Schema” in chapter “Replacement” quite straightforwardly:

Proof

[Proof] Fix α\alphasource. Without loss of generality, we can assume ϕ\phisource's only connectives are ∃\existssource, ¬\lnotsource and ∧\landsource (since these are expressively adequate). Let ψ1,…,ψk\psi_1, \ldots, \psi_ksource enumerate each of ϕ\phisource's subformulas according to complexity, so that ψk=ϕ\psi_k = \phisource. By lemma one in chapter “Replacement”, there is a β>α\beta > \alphasource such that, for any a¯i∈Vβ\overline{a}_i \in V_\betasource and each 1≤i≤k1 \leq i \leq ksource:

∃xψi(a¯i,x)→(∃x∈Vβ)ψi(a¯i,x)row label *\label{reflectionnicelybehaved} \exists x\psi_i(\overline{a}_i, x) \rightarrow (\exists x \in V_\beta) \psi_i(\overline{a}_i, x)\tag{*}source

By induction on complexity of ψi\psi_isource, we will show that ψi(a¯i)↔ψiVβ(a¯i)\psi_i(\overline{a}_i) \leftrightarrow \psi_i^{V_\beta}(\overline{a}_i)source, for any a¯i∈Vβ\overline{a}_i \in V_\betasource. If ψi\psi_isource is atomic, this is trivial. The biconditional also establishes that, when ψi\psi_isource is a negation or conjunction of subformulas satisfying this property, ψi\psi_isource itself satisfies this property. So the only interesting case concerns quantification. Fix a¯i∈Vβ\overline{a}_i \in V_\betasource; then:

(∃xψi(a¯i,x))Vβ iff (∃x∈Vβ)ψiVβ(a¯i,x)by definition iff (∃x∈Vβ)ψi(a¯i,x)by hypothesis iff ∃xψi(a¯i,x)by equation star in chapter Replacement(\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}}source
References in this expression: equation (*) in chapter “Replacement”.

This completes the induction; the result follows as ψk=ϕ\psi_k = \phisource.

We have proved Reflection in ZF\ZFsource. Our proof essentially followed Richard Montague (1961). We now want to prove in Z\Zsource that Reflection entails Replacement. The proof follows Azriel Lévy (1960), but with a simplification.

Since we are working in Z\Zsource, we cannot present Reflection in exactly the form given above. After all, we formulated Reflection using the “VαV_\alphasource” notation, and that cannot be defined in Z\Zsource (see section “Z and ZF: A Milestone” in chapter “Stages and Ranks”). So instead we will offer an apparently weaker formulation of Replacement, as follows:

Definition two in this chapter

Weak-Reflection. For any formula ϕ\phisource, there is a transitive set SSsource such that 00source, 11source, and any parameters to ϕ\phisource are elements of SSsource, and (∀x¯∈S)(ϕ↔ϕS)(\forall \overline{x} \in S)(\phi \liff \phi^S)source.

To use this to prove Replacement, we will first follow Azriel Lévy (1960), first part of Theorem 2 and show that we can “reflect” two formulas at once:

Lemma: in set theory Z plus Weak-Reflection.

[in Z+Weak-Reflection\Z + \text{Weak-Reflection}source.] For any formulas ψ,χ\psi, \chisource, there is a transitive set SSsource such that 00source and 11source (and any parameters to the formulas) are elements of SSsource, and (∀x¯∈S)((ψ↔ψS)∧(χ↔χS))(\forall \overline{x} \in S)((\psi \liff \psi^S) \land (\chi \liff \chi^S))source.

Proof

Let ϕ\phisource be the formula (z=0∧ψ)∨(z=1∧χ)(z = 0 \land \psi) \lor (z = 1 \land \chi)source.

Here we use an abbreviation; we should spell out “z=0z = 0source” as “∀tt∉z\forall t\, t \notin zsource” and “z=1z =1source” as “∀s(s∈z↔∀tt∉s)\forall s(s \in z \liff \forall t\, t \notin s)source”. But since 0,1∈S0, 1 \in Ssource and SSsource is transitive, these formulas are absolute for SSsource; that is, they will apply to the same object whether we restrict their quantifiers to SSsource.Footnote: More formally, letting ξ\xisource be either of these formulas, ξ(z)↔ξS(z)\xi(z) \liff \xi^S(z)source.

By Weak-Reflection, we have some appropriate SSsource such that:

(∀z,x¯∈S)(ϕ↔ϕS)i.e. (∀z,x¯∈S)(((z=0∧ψ)∨(z=1∧χ))↔(((z=0∧ψ)∨(z=1∧χ))S)i.e. (∀z,x¯∈S)(((z=0∧ψ)∨(z=1∧χ))↔(((z=0∧ψS)∨(z=1∧χS)))i.e. (∀x¯∈S)((ψ↔ψS)∧(χ↔χS))(\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))source

The second claim entails the third because “z=0z = 0source” and “z=1z=1source” are absolute for SSsource; the fourth claim follows since 0≠10 \neq 1source.

noindent We can now obtain Replacement, just by following and simplifying Azriel Lévy (1960), Theorem 6:

Theorem: in set theory Z + Weak-Reflection

[in Z\Zsource + Weak-Reflection] For any formula ϕ(v,w)\phi(v,w)source, and any AAsource, if (∀x∈A)∃!yϕ(x,y)(\forall x \in A)\lexists![y][\phi(x,y)]source, then {y:(∃x∈A)ϕ(x,y}\Setabs{y}{(\exists x \in A)\phi(x,y}source exists.

Proof

Fix AAsource such that (∀x∈A)∃!yϕ(x,y)(\forall x \in A)\lexists![y][\phi(x,y)]source, and define formulas:

ψ is (ϕ(x,z)∧A=A)χ is ∃yϕ(x,y)\psi &\text{ is } (\phi(x, z) \land A = A)\\ \chi &\text{ is } \lexists[y][\phi(x, y)]source

Using the lemma on reflect, since AAsource is a parameter to ψ\psisource, there is a transitive SSsource such that 0,1,A∈S0, 1, A \in Ssource (along with any other parameters), and such that:

(∀x,z∈S)((ψ↔ψS)∧(χ↔χS))(\forall x,z \in S)((\psi \liff \psi^S) \land (\chi \liff \chi^S))source

So in particular:

(∀x,z∈S)(ϕ(x,z)↔ϕS(x,z))(∀x∈S)(∃yϕ(x,y)↔(∃y∈S)ϕS(x,y))(\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))source

Combining these, and observing that A⊆SA \subseteq Ssource since A∈SA \in Ssource and SSsource is transitive:

(∀x∈A)(∃yϕ(x,y)↔(∃y∈S)ϕ(x,y))(\forall x \in A)(&\exists y\phi(x, y) \liff (\exists y \in S)\phi(x, y))source

Now (∀x∈A)(∃!y∈S)ϕ(x,y)(\forall x \in A)(\lexists![y \in S])\phi(x, y)source, because (∀x∈A)∃!yϕ(x,y)(\forall x \in A)\lexists![y][\phi(x, y)]source. Now Separation yields {y∈S:(∃x∈A)ϕ(x,y)}={y:(∃x∈A)ϕ(x,y)}\Setabs{y \in S}{(\exists x \in A) \phi(x, y)} = \Setabs{y}{(\exists x \in A) \phi(x, y)}source.

Appendix: Finite axiomatizability

We close this chapter by extracting some results from Replacement. The first result is due to Richard Montague (1961); note that it is not a proof within ZF\ZFsource, but a proof about ZF\ZFsource:

Theorem three in this chapter

ZF\ZFsource is not finitely axiomatizable. More generally: if T\Th{T}source is finite and T⊢ZF\Th{T} \Proves \ZFsource, then T\Th{T}source is inconsistent.

(Here, we tacitly restrict ourselves to first-order sentences whose only non-logical primitive is ∈\insource, and we write T⊢ZF\Th{T} \Proves \ZFsource to indicate that T⊢ϕ\Th{T} \Proves \phisource for all ϕ∈ZF\phi \in \ZFsource.)

Proof

Fix finite T\Th{T}source such that T⊢ZF\Th{T} \Proves \ZFsource. So, T\Th{T}source proves Reflection, i.e.\ theorem “Reflection Schema” in chapter “Replacement”. Since T\Th{T}source is finite, we can rewrite it as a single conjunction, θ\thetasource. Reflecting with this formula, T⊢∃β(θ↔θVβ)\Th{T} \Proves \exists \beta(\theta \liff \theta^{V_\beta})source. Since trivially T⊢θ\Th{T} \Proves \thetasource, we find that T⊢∃βθVβ\Th{T} \Proves \exists \beta\ \theta^{V_\beta}source.

Now, let ψ(X)\psi(X)source abbreviate:

θX∧X is transitive∧(∀Y∈X)(Y is transitive→¬θY)\theta^X \land X\text{ is transitive} \land (\forall Y \in X)(Y\text{ is transitive}\lif \lnot \theta^{Y})source

roughly this says: XXsource is a transitive model of θ\thetasource, and ∈\insource-minimal in this regard. Now, recalling that T⊢∃βθVβ\Th{T} \Proves \exists \beta\ \theta^{V_\beta}source, by basic facts about ranks within ZF\ZFsource and hence within T\Th{T}source, we have:

T⊢∃Mψ(M).row label *\Th{T} \Proves \exists M \psi(M). \tag{*}\label{Mpsi}source

Using the first conjunct of ψ(X)\psi(X)source, whenever T⊢σ\Th{T} \Proves \sigmasource, we have that T⊢∀X(ψ(X)→σX)\Th{T} \Proves \forall X(\psi(X) \lif \sigma^X)source. So, by equation (*) in chapter “Replacement”:

T⊢∀X(ψ(X)→(∃Nψ(N))X)Using this, and equation star in chapter Replacement again:T⊢∃M(ψ(M)∧(∃Nψ(N))M)In particular, then:T⊢∃M(ψ(M)∧(∃N∈M)((N is transitive)N∧(θN)M))So, by elementary reasoning concerning transitivity:T⊢∃M(ψ(M)∧(∃N∈M)(N is transitive∧θN))\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))source
References in this expression: equation (*) in chapter “Replacement”.

So that T\Th{T}source is inconsistent.Footnote: This “elementary reasoning” involves proving certain “absoluteness facts” for transitive sets.

Here is a similar result, noted by Michael Potter (2004), 223:

Proposition one in this chapter

Let T\Th{T}source extend Z\Zsource with finitely many new axioms. If T⊢ZF\Th{T} \Proves \ZFsource, then T\Th{T}source is inconsistent. (Here we use the same tacit restrictions as for theorem three in chapter “Replacement”.)

Proof

Use θ\thetasource for the conjunction of all of T\Th{T}source's axioms except for the (infinitely many) instances of Separation. Defining ψ\psisource from θ\thetasource as in theorem three in chapter “Replacement”, we can show that T⊢∃Mψ(M)\Th{T} \Proves \exists M \psi(M)source.

As in theorem three in chapter “Replacement”, we can establish the schema that, whenever T⊢σ\Th{T} \Proves \sigmasource, we have that T⊢∀X(ψ(X)→σX)\Th{T} \Proves \forall X(\psi(X) \lif \sigma^X)source. We then finish our proof, exactly as in theorem three in chapter “Replacement”.

However, establishing the schema involves a little more work than in theorem three in chapter “Replacement”. After all, the Separation-instances are in T\Th{T}source, but they are not conjuncts of θ\thetasource. However, we can overcome this obstacle by proving that T⊢∀X(X is transitive→σX)\Th{T} \Proves \forall X(X\text{ is transitive} \lif \sigma^X)source, for every Separation-instance σ\sigmasource. We leave this to the reader.

Exercise two in this chapter

Show that, for every Separation-instance σ\sigmasource, we have: Z⊢∀X(X is transitive→σX)\Z \Proves \forall X(X\text{ is transitive} \lif \sigma^X)source. (We used this schema in proposition one in chapter “Replacement”.)

Exercise three in this chapter

Show that, for every ϕ∈Z\phi \in \Zsource, we have ZF⊢ϕVω+ω\ZF \Proves \phi^{V_{\omega+\omega}}source.

Exercise four in this chapter

Confirm the remaining schematic results invoked in the proofs of theorem three in chapter “Replacement” and proposition one in chapter “Replacement”.

As remarked in section “Replacement and “Absolute Infinity”” in chapter “Replacement”, this shows that Replacement is strictly stronger than theorem five in chapter “Ordinals”. Or, slightly more strictly: if Z\Zsource + “every well-ordering is isomorphic to a unique ordinal” is consistent, then it fails to prove some Replacement-instance.

Source disclosures