[Math] Where in ordinary math do we need unbounded separation and replacement

foundationslo.logicset-theory

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

Best Answer

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.

Related Question