36
$\begingroup$

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

$\endgroup$
63
  • 13
    $\begingroup$ 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! $\endgroup$
    – Asaf Karagila
    Commented Jun 8, 2015 at 6:09
  • 7
    $\begingroup$ @Asaf but functions in etcs come with a specified codomain! And saying functions are more important is not quite right: the structure of the category is what is important, and that includes sets and functions. $\endgroup$
    – David Roberts
    Commented Jun 8, 2015 at 6:10
  • 16
    $\begingroup$ 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. $\endgroup$
    – Zhen Lin
    Commented Jun 8, 2015 at 7:21
  • 8
    $\begingroup$ 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. $\endgroup$ Commented Jun 8, 2015 at 8:15
  • 6
    $\begingroup$ 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? $\endgroup$ Commented Jun 8, 2015 at 12:42

6 Answers 6

40
$\begingroup$

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

$\endgroup$
45
  • 7
    $\begingroup$ 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. $\endgroup$ Commented Jun 8, 2015 at 11:12
  • 4
    $\begingroup$ @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. $\endgroup$ Commented Jun 8, 2015 at 14:09
  • 10
    $\begingroup$ 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." $\endgroup$ Commented Jun 8, 2015 at 14:47
  • 9
    $\begingroup$ 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. $\endgroup$ Commented Jun 8, 2015 at 19:11
  • 7
    $\begingroup$ 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." $\endgroup$ Commented Jun 9, 2015 at 2:12
29
$\begingroup$

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.

$\endgroup$
21
  • 1
    $\begingroup$ 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? $\endgroup$
    – David Roberts
    Commented Jun 9, 2015 at 8:06
  • 6
    $\begingroup$ @Thomas, Adam: Can you please provide a reference for the equivalence established by Mathias? $\endgroup$
    – Ali Enayat
    Commented Jun 9, 2015 at 9:28
  • 9
    $\begingroup$ 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\}$. $\endgroup$ Commented Jun 9, 2015 at 11:52
  • 4
    $\begingroup$ 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! $\endgroup$
    – Asaf Karagila
    Commented Jun 9, 2015 at 15:58
  • 7
    $\begingroup$ 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 $\endgroup$ Commented Jun 10, 2015 at 9:56
11
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ Interesting, thanks! $\endgroup$
    – David Roberts
    Commented Nov 19, 2022 at 0:16
9
$\begingroup$

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.

$\endgroup$
6
  • 2
    $\begingroup$ Sebastian Vasey showed how to remove the application of Erdös-Rado in the proof of Kim's lemma for simple theories in this paper. $\endgroup$ Commented Aug 1 at 19:43
  • $\begingroup$ Abstract says: We present a new proof of the existence of Morley sequences in simple theories. We avoid using the Erdős–Rado theorem and instead use only Ramsey’s theorem and compactness. The proof shows that the basic theory of forking in simple theories can be developed using only principles from “ordinary mathematics,” answering a question of Grossberg, Iovino, and Lessmann, as well as a question of Baldwin. Nice. $\endgroup$
    – David Roberts
    Commented Aug 2 at 0:59
  • $\begingroup$ Thanks for this example, certainly infinite combinatorics is a place where the boundary of 'generic mathematics' is (close to) being breached. I guess if one is not just thinking of a binary yes/no on usages of Replacement instances, but keeping track of what principles one needs, then the above seems to use the "all beths exist" axiom that was discussion in the Large Sets series of n-category café posts. $\endgroup$
    – David Roberts
    Commented Aug 2 at 1:04
  • $\begingroup$ From the end of the paper pointed out by @AlexKruckman We end by pointing out that all the results of this paper could be formalized in a weak fragment of ZFC, such as ZFC - Replacement - Power set + "for any set X of size $\leq |T|$, $P(P(X))$ exists." Heh, even nicer. So you don't even need an actual model of (something equivalent to) ETCS. $\endgroup$
    – David Roberts
    Commented Aug 2 at 1:08
  • $\begingroup$ @DavidRoberts Well first of all Vasey's article doesn't remove the use of Erdös–Rado from many of the other places in model theory where it is used, and second of all in one of my model theory papers I actually needed to assume the existence of an Erdős cardinal to prove something about countable objects, and despite my best efforts I do not see how to remove that. $\endgroup$ Commented Aug 2 at 1:58
6
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ I think his system "MC" includes AC: Suitable set theories include the elementary theory of the category of sets (ETCS) (Lawvere, 1965), and the fragment of ZFC without replacement or foundation and with separation only for bounded formulas. This fragment is Mathias’s ZBQC minus foundation or his Mac minus foundation and transitive containment. Equiconsistency of finite order arithmetic and all these named set theories follows from Mathias (2001). I haven't gone through to double check if AC is explicitly used, but I presume so. $\endgroup$
    – David Roberts
    Commented Sep 13 at 4:31
3
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ 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) $\endgroup$
    – David Roberts
    Commented Aug 22, 2016 at 2:41
  • 3
    $\begingroup$ @DavidRoberts Well, for me the AST itself is part of my mathematical practice :D $\endgroup$ Commented Aug 22, 2016 at 5:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .