Where in ordinary math do we need unbounded separation and replacement?

Question

[I have updated the question after initial comments in the hope of clarifying it.]

I do quite a bit of reasoning, typically about topology and metric spaces, in "non-standard" foundations, such as inside of a particular topos, in type theory, or a predicative constructive setting. These typically do not have anything corresponding to unbounded separation or replacement (the constructive set theory CZF does have collection, though).

I have a pretty good feel when restricted forms of excluded middle and choice are needed, and what things powersets give us over predicative math, etc. But I never ever wish I had unbounded separation and replacement. Why is that? Is it just because of the kind of math I do, or are these two really not needed very much in ordinary math?

To make the question more specific: what are some well-known definitions and theorems in "ordinary" mathematics which require unbounded separation or replacement?

The obvious uses of replacement and unbounded separation come from set theory, so we should avoid listing those. Ideally, I am looking for theorems and definitions in algebra, topology, and analysis.

Here is a non example from order theory, which was suggested in the comments. Under the usual encoding of ordinals as hereditarily transitive transitive sets, the rank of the function $n \mapsto \omega + n$ is $\omega + \omega$ and so we need replacement to show its existence. However, even PA can speak about this sort of small countable ordinals, so we are seeing here an artifact of a particular encoding. A different encoding of countable ordinals would make this function easy to define (for example we could view the countable ordinals as orders of subsets of $\mathbb{N}$).

The only example of unbounded separation I can think of right now comes from category theory. In a large category $C$ the definition of epi is unbounded, as it requires quantification over all objects of $C$. I am looking for something that is not so directly linked to a question of size.

Answer 1

I asked the same question about the replacement axiom not long ago at the $n$-Category Café, and the answer I got back from Mike Shulman is that it's used for example in the transfinite construction of free algebras, which really refers to a body of connected results in category theory as described here. The essential use made of replacement is in the transfinite compositions; this also occurs in the small object argument.

Having said that, a part of me still wonders whether there aren't workarounds. In many cases an initial algebra of a functor is situated inside a terminal coalgebra of the same functor, and the construction of the latter often doesn't require transfinite compositions (this is the case, e.g., for polynomial endofunctors). Paul Taylor in his book Practical Foundations of Mathematics has a section on general recursion using a theory of well-founded coalgebras, which is manifestly meaningful in contexts where one does without replacement, such as ETCS, and I wonder to what extent this could be put to use to construct free algebras without resorting to replacement.

Answer 2

I would put this as a comment but I cannot. Even within set theory many of the things we use replacement for can also be done using union, power set, and comprehension. However, Harvey Friedman has showed that you need replacement for Borel Determinacy.

Answer 3

This very matter is discussed in depth by Mathias, in Chapter 9 of his The Stength of Mac Lane Set Theory https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf. There he shows that to prove

$\;\;$ "for all $n$ there exist $n$ pairwise nonequinumerous infinite sets"

requires some use of unbounded Separation, and to prove

$\;\;$ "there exists an infinite set of pairwise nonequinumerous infinite sets"

requires some use of Replacement. He also discusses various refinements in connection with formula complexity and stratifiability. For example, Coret showed that that the stratified instances of Replacement are already theorems of Zermelo set theory, whence "requires some Replacement" entails "requires some unstratifiable Replacement".

Algebraists might prefer these assertions concerning sequences of $\mathbb R$-linear spaces defined though duality: $L_1=\mathbb{R}[t]$ and $L_{k+1}=L_k^*$. In this setting,

$\;\;$ "for all $n$ the sequence $L_1,\ldots, L_n$ exists"

requires some use of unbounded Separation, and

$\;\;$ "the sequence $L_1, L_2, \ldots $ exists"

requires some use of Replacement.

Whether or not these assertions count as ordinary mathematics, I find them considerably easier to grasp than Borel Determinacy, which seems vastly more intricate. Then again, maybe the second example counts as "there's life beyond $V_{\omega+\omega}$".

Meanwhile, some of the motivation of this question resonates with mine in posing these questions:

When must it be sets rather than proper classes, or vice-versa, outside of foundational mathematics?

Can one exhibit an explicit Kuratowski infinite set without invoking Replacement?

Some of the comments on the first (Sets vs Classes) allude to various constructions in homotopy theory involving long-running transfinite recursions - and even large cardinals - so presumably there is some Replacement involved.

Answer 4

This would be set theory rather than `ordinary math'. Still, it's interesting to observe that without Unbounded Separation many of the customarily equivalent formulations of finiteness diverge. For example, it is no longer the case that the system of Zermelo naturals and the system of von Neumann naturals are isomorphic. This is discussed in "Natural Number Arithmetic in the Theory of Finite Sets" by Mayberry-Pettigrew, http://arxiv.org/abs/0711.2922.

Answer 5

The Stacks Project, which is a thorough introduction to algebraic stacks, including necessary background, uses the axiom of replacement when constructing categories of schemes closed under certain operations. (I believe the purpose of this is to avoid using universes.)

In the construction, they explicitly work with $V_\alpha$, and prove by transfinite induction that there exists a big enough $\alpha$ so that the category of schemes contained in $V_\alpha$ is closed under certain operations.

Answer 6

I believe that Bourbaki do not include the axiom of replacement in their treatment of set theory (my source is that a logician, Adrian Mathias, once told me this; I confess I never checked). Given that they were attempting to write something like "the foundations of mathematics" at the time, one might be tempted to conclude that Cartan, Chevalley, Weil and whoever the others were had actively decided that replacement was just "something for the set theorists".

I vaguely remember from my UG days that $V_{\omega+\omega}$ was a model for ZF with replacement removed; however my instinct would have been to ask an even stronger version of the question: forget replacement or whatever -- does "normal" mathematics ever get anywhere near $V_{\omega+\omega}$? I am pretty sure that e.g. Wiles' proof of FLT never uses a set anywhere near the "complexity" of something not in $V_{\omega+\omega}$.

Wiles uses some commutative algebra in his proof, and I always remember the unique time I ever saw a transfinite induction in a book that wasn't a book on set theoretical/foundational issues -- it was in Matsumura's "Commutative Algebra" where he proves that...I think it was the proof that projective modules over a local ring were free, which I think he does by transfinite induction on the cardinality of the module. However I suspect that...meh...I was going to argue that Wiles and his references never use cardinalities greater than something like $2^{2^{2^{\aleph_0}}}$, but on the other hand I guess without CH this can be pretty large.