Who needs Replacement anyway?

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' blog1 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?

1 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.]

• It always bothers me when people from category theory question Replacement. The idea behind the categorical approach, as I understand it, is that functions are more important than elements. Replacement tells you the universe is closed under definable functions. Functions! – Asaf Karagila Jun 8 '15 at 6:09
• The example with $(X, P (X), P^2 (X), \ldots)$ is more subtle than it looks. For instance, imagine a model of ETCS with non-standard naturals: then you wouldn't even be able to define $P^n (X)$ for all natural numbers $n$, let alone apply replacement to that "function". These two issues – the "large" recursion principle and the axiom of replacement – seem to be intertwined in category-theoretic formulations of set theory. – Zhen Lin Jun 8 '15 at 7:21
• I'm not sure if Borel determinacy counts as "ordinary" enough. But the reason why I mention it is that Harvey Friedman proved that Replacement is actually needed for the proof. So no "hack" is available. – Monroe Eskew Jun 8 '15 at 8:15
• Perhaps one could frame the question as follows: is a suitable formulation in set theory of the principle that David wants simply equivalent to the replacement axiom? Or is it provable in a weaker set theory? – Joel David Hamkins Jun 8 '15 at 12:42
• This question seems quite related: mathoverflow.net/questions/121406/… – Emil Jeřábek Jun 8 '15 at 13:37

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

• I was trying to avoid stating personal opinions, but I guess they are only shallowly disguised... The two main objections I have with ETCS as a foundational theory are: (1) there is no clear guiding ontology to judge the validity of the axioms and (2) it doesn't appear to be self-justifying in the same manner as PA and ZFC. I could be wrong on both counts but I never found anything. Otherwise it's a pretty fine theory that works really well in practice. I'd be happier if it had dependent families similar to those in type theory but then the need for replacement would probably be obvious. – François G. Dorais Jun 8 '15 at 11:12
• @Todd: I use "ontology" in your first understanding, which does entail Platonistic view of mathematical objects. In my first paragraph, I explain how replacement is justified by this Platonist view of the universe of sets. In my comment above, it refers to my own view. Of course, some may not share this view, in which case that lacuna of ETCS is moot. I don't think the axioms are a mish-mash, they are well motivated by the success of topos theory, which is modeled after the structure of Set. But this is too indirect for me to serve as a theory of existence. – François G. Dorais Jun 8 '15 at 14:09
• FWIW, I believe most people use "ontology" the way François does. If I am confronted with a set of axioms, even in a non-foundational context, usually the first question I have is, "What's an example of something that satisfies these axioms?" In ordinary mathematics, if you can't give any examples, that's usually a deal-breaker, unless you can give a compelling conjectural example. In foundations, of course, "giving an example" comes with Goedelian caveats, but I still want to see an example. If no example is forthcoming then I'll complain that the axioms have "no clear ontology." – Timothy Chow Jun 8 '15 at 14:47
• Thanks all, for having this discussion with me. So it seems "ontology" stands as a kind of rubric for recursive processes for the ability to create new sets from old (ultimately from nothing, if atoms aren't assumed). François said somewhere that one of his main mathematical complaints about ETCS is that it has a weak grasp of induction, and I think I can appreciate the idea that what traditional set theories (like ZFC) are are really highly elaborated studies in recursion. If this accords with what you guys are saying, I think I have a better idea of it now. – Todd Trimble Jun 8 '15 at 19:11
• Todd seems satisfied with the word "ontology" now, but I want to comment why we don't use something like "recursion" instead. The fundamental desire is still for a clear picture of the universe of things of interest. The typical way to get such a picture is to state some simple rules for creating new things and to say that we're interested in everything that emerges. That's where recursive processes come in. But the recursive processes are a means toward an end of describing everything there is. Hence, "ontology." – Timothy Chow Jun 9 '15 at 2:12

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 classifer 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 equicalent

• that's interesting about Mathias' example, I wouldn't have expected that. In ETCS, one posits the existence of binary products of sets, and doesn't have Replacement, so something must be going on with the other assumptions. Do you know what they are? – David Roberts Jun 9 '15 at 8:06
• @Thomas, Adam: Can you please provide a reference for the equivalence established by Mathias? – Ali Enayat Jun 9 '15 at 9:28
• Isn’t the proof obvious, actually? If $F$ is a definable function, define a pairing function $(x,y)_F$ so that $(x,y)_F=((x,y),F(x))$, where $(x,y)$ is the standard pairing. Then $F[X]$ can be defined by bounded separation and union from $X\times_F\{0\}$. – Emil Jeřábek Jun 9 '15 at 11:52
• Thomas, the result about pairs is awesome. Even more since a couple years back I realized (when writing some answer on Math.SE) that really formalizing things in set theory we write "proof schema" where "ordered pair" or "function" are really just placeholders for definitions that work, and the proof is essentially the same proof. I never thought that this intuitive understanding is in fact the full fledged power of the Replacement schema. And that's pretty awesome! – Asaf Karagila Jun 9 '15 at 15:58
• Jerabek is absolutely right; that is Mathias' proof. However i fear that the cuteness of Mathias' factoid is distracting attention from the generality of the message, namely that replacement is purely and simply a global principle of implementation-insensitivity. It has a set-theoretic form, but its true meaning lies outside set theory – Thomas Forster Jun 10 '15 at 9:56

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.

• Sure, this is a nice example, but do people implicitly use the small powerset functor when using naive class/set theory in practice? (I should add that I like the use of the pretopos of classes -- it demystifies a lot of things when using classes even in ZFC) – David Roberts Aug 22 '16 at 2:41
• @DavidRoberts Well, for me the AST itself is part of my mathematical practice :D – მამუკა ჯიბლაძე Aug 22 '16 at 5:34