Who needs Replacement anyway?

Question

The set theory ETCS famously comes without the Replacement axiom schema (or an equivalent) that is part of ZFC. One (to me, not apparently useful) set that one cannot build in ETCS is $\coprod_{n\in \mathbb{N}} P^n(\mathbb{N})$. Jacob Lurie pointed out on Michael Harris' blog¹ the example of taking a Banach space $V$ and considering the colimit of the sequence $V \to V^{**}\to V^{*4} \to \cdots$. Yemon Choi responded to a foolish suggestion of mine that this sequence (or rather, the related cosimplicial object) is in fact of use.

This got me to thinking that from a category-theoretic point of view, we are used to not having enough colimits (say in geometric settings, like schemes, manifolds, and so on) or limits (for instance in settings like finite groups etc), and this is deftly sidestepped by using a colimit completion. One can consider ind-schemes, or differentiable stacks, etc etc. Why should ETCS be any different, apart from intending to be the primordial category?

What stops me from working, when I need to, in a slightly larger category that is in a sense a colimit-completion of an ETCS category, with the understanding that most of the time I'm interested in objects in my original category, but sometimes constructions I'm interested in sit outside it? The original example above is perfectly well represented as the sequence $k\mapsto \coprod_{0\leq n\leq k} P^n(\mathbb{N})$, with the obvious inclusions between them.

Note that I'm not asking that arbitrary objects in the completed category are necessarily the stuff of ordinary mathematics, or that the completed category is a topos, or a model of ETCS. But what can go wrong with this approach? What are the usual uses of Replacement in "ordinary mathematics" (almost anything that's not ZFC-and-friends) that could/couldn't be sorted by the method proposed above?

---

¹ The context of the discussion was the effect on ordinary mathematics the discovery that ZFC was inconsistent. Tom Leinster argues (and I agree) that the most likely culprit would be Replacement, since the rest of ZFC is essentially equivalent to ETCS, and the axioms of ETCS encode the operations on sets that underly day-to-day practice of people who aren't set theorists.

[EDIT: On reflection, I'm putting words into Tom's mouth a little here. The actual point he has made is that if a contradiction were found with using Replacement, it wouldn't affect most mathematicians, but it a contradiction were found in ETCS (equivalently, BZC) then we could start to worry. If we assume that 'ordinary' mathematics is consistent, as it seems to be, then one might make the---justified or not---leap that a little-used axiom is the place a contradiction might be found, if one existed. As others have pointed out in the comments below, Comprehension is also a contender for a 'risky' axiom.]

Answer 1

I think the main reason replacement is seen as an essential part of ZF is that it naturally follows from the ontology of set theory, as do the other axioms of ZF. The ontology of set theory is rooted in the idea that sets are obtained by an iterative process along a wellordered "ordinal clock", where at each step all the sets whose elements were generated earlier now appear. It is intuitively clear that, in order to be exhaustive, this process must go on for a long, long time. From this point of view, the replacement axiom can be intuitively stated: no set can be used as an indexing of a family of ordinals that reaches to the end of the ordinal timeline. This is a natural consequence of the idea that the iterative process should be exhaustive.

Another interesting aspect of replacement is that (in most formulations of ZFC) it is logically equivalent to reflection. (Informally: for any formula $\sigma(\vec{x})$ in the language of set theory, if $V \models \sigma(\vec{x})$ then there is an ordinal $\alpha$ such that $V_\alpha \models \sigma(\vec{x})$.) This is an extremely useful principle. One of its side effects is that ZFC is "self-justifying" in the sense that any finite fragment of ZFC is realized in a level $V_\alpha$ of the cumulative hierarchy. In other words, if one were to test set theory by examining a finite fragment of the axioms within the universe of sets, one would see that this finite fragment is not only consistent but that it has a model $V_\alpha$ that arises from the same iterative process that all sets do. In particular, ZFC comes very close to proving its own consistency even though we know this is not possible after Gödel. This feature makes ZFC very appealing as a foundational theory. (Note that PA has a similar self-justifying feature, but ETCS doesn't appear to have this.)

Another, more practical, use of replacement is to obtain "cheap universes". Grothendieck universes have proven useful for handling large objects. Unfortunately, one cannot prove their existence in ZFC. It is nevertheless often true that a "reasonable theorem" proven using Grothendieck universes is actually provable in ZFC. The reason is that the proof often doesn't make full use of all the features of Grothendieck universe, a finite fragment of those features often suffices and in such cases reflection provides a set $V_\alpha$ with all the necessary features to make the argument work. ETCS doesn't appear to have a good way of obtaining "cheap universes". This also hints at an alternative to replacement, which is to have a hierarchy of universes similar to those used in dependent type theory.

Operations on dependent families is where the need for replacement arises most. It's actually really hard to even talk about dependent families in the language of ETCS. The main issue with ETCS isn't necessarily that it can't prove the existence of coproducts like $\coprod_{n \in \mathbb{N}} \mathcal{P}^n(\mathbb{N})$, but that it has a hard time even talking about the family of all $\mathcal{P}^n(\mathbb{N})$ in the first place. Introducing universes would be an interesting way to get around that problem but there are other means, all of which are likely to make the need for replacement-like principles clear.

As for the proposed workaround, it's unclear you would get much more by this kind of process. Rather than ETCS, I'll work in BZC extended with terms for powersets and union and a constant symbol for $\omega$. The exponential-bounded formulas are defined like bounded formulas except that the bounding terms can involve powerset and union.

Fact. If $\phi(x,y)$ is an exponentially-bounded formula such that BZC proves that $\forall x \exists y \phi(x,y)$ then there is a standard number $n$ such that BZC proves that $\forall x \exists y(\phi(x,y) \land |y| \leq |\mathcal{P}^n(x \cup \omega)|)$.

Proof. Find a model $M$ of BZC and consider $x \in M$. Let $M' = \bigcup_n \{z \in M : |z| \leq |\mathcal{P}^n(x \cup \omega)|\}$ where $n$ ranges over the standard numbers only. Note that $M'$ is model of BZC that contains $x$. By hypothesis, there is a $y \in M'$ such that $M' \models \phi(x,y)$. Note that exponential-bounded formulas are absolute between $M'$ and $M$ since the only sets that we need to look at to figure out that $\phi(x,y)$ is true are in $M'$. Thus $M \models \phi(x,y)$ and also $M \models |y| \leq |\mathcal{P}^n(x \cup \omega)|$ by definition of $M'$. Now the fact that there is a fixed standard $n$ that provably works for all $x$ follows by a compactness argument. $\square$

The examples $\omega, \mathcal{P}(\omega), \mathcal{P}^2(\omega), \ldots$ and $V, V^{\ast}, V^{\ast\ast},\ldots$ are definable by a formula of the form $\exists z\phi(x,y,z)$ where $\phi(x,y,z)$ is exponential-bounded. Because of the nice biinterpretation between ETCS and BZC, for these and similar examples, either ETCS doesn't prove that the $n$-th iterate exists for every natural number $n$, or ETCS already proves that replacement holds in this particular instance.

Let me also address one aspect of the footnote, which states that replacement would be "the most likely culprit" if ZFC were found to be inconsistent. The "standard objection" to axiomatic set theory is actually with comprehension. If you think about it, comprehension is a rather bold statement: every formula in the language of set theory can be used to define a subset of a given set. The issue is that formulas can be complex beyond (human) understanding, it's hard to justify the use of comprehension for formulas we can't understand. In fact, it's not clear that comprehension is fully justified by the ontology of set theory described above. (Note that the same kind objection applies to PA, where one asks for induction to hold for arbitrary formulas.)

Answer 2

The real reason for the importance of replacement is not the fact that it proves the existence of large sets, but that it is a kind of global implementation-insensitivity principle. Suppose I have a kind of abstract mathematical entity that arises from equivalence classes for an equivalence relation. (Think: cardinals, ordinals). There are various ways of implementing such objects in set theory, but in all such cases one has a classifier, which is a function that sends two things to the same value iff they are equivalent in the relevant sense. A classifier for cardinality sends two things to the same thing iff they are in bijection with each other. The values are the implementations of (in this case) cardinals. Clearly if I have two classifiers (for cardinals, to persist with this example) then I get two implementations of cardinals, and they will of course be isomorphic. So certainly they give rise to the same first-order theory. That is of course what we want: it shouldn't matter what implementation we use. But what about the second order theory? If we want to show that the isomorphism lifts to sets of cardinals, then we need replacement. There is a rather cute illustration of this phenomenon due to Adrian Mathias. Suppose you want to ensure that $X \times Y$ exists whatever your pairing/unpairing kit is, then you have to assume replacement. The assumptions are equivalent.

Answer 3

Here's an example of a published, nontrivial use of the the product of the sequence $\{ V, V^{*}, V^{**}, \ldots \}$ in a functional analysis paper, for the specific case of $V = \mathbb{R}^{\mathbb{N}}$ (where $*$ means algebraic dual). If we could form this product, we could also form the vector space colimit of $V \rightarrow V^{**} \rightarrow V^{****} \rightarrow \cdots$ using only separation (because the coproduct vector space is a sub-vector space of the product).

It occurs in Section 5 of Kōmura's Some Examples on Linear Topological Vector Spaces (Math. Annalen 153, pp. 150–162 (1964)), while giving an example of a Montel space $E$ that is not complete (with respect to the usual uniformity on a locally convex space implied by its topology). By its construction, $E$ is also an example of an incomplete reflexive nuclear space. I won't repeat the construction here as it involves many details, but $E$ is a dense (linear and topological) subspace of $$ \prod_{n=0}^\infty (\mathbb{R}^{\mathbb{N}})^{*^n}. $$ In fact Kōmura actually uses $\mathbb{R}^{\beth_n}$ instead of $(\mathbb{R}^{\mathbb{N}})^{*^n}$, but these are well known to be isomorphic (Erdős-Kaplansky).

Unfortunately I do not know if this is "essential". That is to say, I don't know if anybody has found a continuum-sized example, and I strongly suspect that nobody has shown that this fact implies any non-trivial instances of the axiom of replacement.

Answer 4

I don't know if this counts as 'ordinary' mathematics (given its historical connection to set theory), but we use replacement a fair amount in model theory. The two most prominent places are in the use of very large 'monster models' of first-order theories and in applications of the Erdős–Rado theorem (specifically for extracting indiscernible sequences). The use of replacement in model theory in this regard is discussed extensively in Baldwin's paper How Big Should the Monster Model Be?

Monster models are something which can in principle be worked around, but are convenient enough to be a mainstay of model theory. There are varying levels of 'monstrosity' that are needed in proofs but building a monster model of a theory $T$ of size $\kappa$ commonly involves a construction of size $\beth_{\kappa^+}$. (This is because it's useful to have not just the size of the monster model be much bigger than the size of the theory but also the cofinality of the size of the monster model, which motivates the use of the successor of $\kappa$.)

The application of the Erdős–Rado theorem in model theory is mostly through the following technical result of Shelah:

Proposition. For any set of parameters $A$ and sequence $(b_i)_{i<\lambda}$ of elements, if $\lambda \geq \beth_{(2^{|A|+|T|})^+}$, then there is an $A$-indiscernible sequence $(c_i)_{i<\omega}$ that is finitely based on $(b_i)_{i < \lambda}$.

If I recall correctly, the bound in this result is known to be sharp.

Both of these concepts are sometimes used relative to an already big set of parameters. I don't know an example offhand, but it's entirely within the realm of possibility that a published model theory paper has involved sets of parameters of size $\beth_{\beth_{\omega_1}^+}$

It should also be noted that these results are used to prove things even about merely countable objects. As discussed in Baldwin's paper, the above proposition was used in the original proof of Kim's lemma (which is important in the structure of simple theories). Baldwin says that it is open whether these kinds of basic facts about simple theories are provable in $\mathsf{ZC}$, but I believe that at one point I was told that these are now known to be provable over weak theories. Regardless, the Erdős–Rado technique is still the conceptually clearer proof and is used in many other ways in model theory.

Answer 5

Isn't replacement needed or at least the most natural way to construct projective/injective resolutions? Say we want a free resolution of $M$. Consider the free module $F_1$ with $M$ as the set of generators, with a natural surjection to $M$. Then consider the kernel of this map, and the free module $F_2$ with this kernel as the set of generators, etc. This even provides a canonical (choice-free) resolution.

McLarty's The large structures of Grothendieck founded on finite order arithmetic seems to develop heavy machinery in algebraic geometry over weak systems without replacement, but he does point out that all previous authors used replacement, and that to get rid of replacement you need some tedious estimation on how much the size of the set increases at each step. I can't quite tell whether he assumes choice.

Answer 6

In this context, I believe, it is relevant to mention the setup of algebraic set theory. One of the key axioms for classes of small maps is that of quotient (if $fg$ is small and $g$ is (regular, effective...) epi then $f$ is small); this axiom is recognized as being a form of replacement.

Without this axiom, for example, it is problematic to define the covariant small powerset functor on the ambient pretopos of classes.