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

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

• What is ordinary mathematics? By unbounded do you mean any unbounded quantifier, or something else (e.g. arguments whose proof uses formulas of unbounded complexity)? – Asaf Karagila Feb 10 '13 at 17:27
• Without unbounded replacement, it may be impossible to define a function on the natural numbers recursively if one does not know in advance that the values of the function are all contained in some set. For example, the function $n \mapsto \omega + n$ cannot be constructed using only $\Delta_0$-replacement, even though each von Neumann ordinal $\omega + n$ exists. However, perhaps this specific example does not count as ordinary mathematics... – Zhen Lin Feb 10 '13 at 18:08
• Add a logic tag? – Jason Rute Feb 10 '13 at 21:09
• Should this be a wiki? – Andrej Bauer Feb 11 '13 at 6:03
• In my mind, I usually define ‘ordinary mathematics’ as mathematics that can be formulated in ETCS (or BZFC if you prefer). Of course, that begs the question, and I try not to take that definition too seriously. – Toby Bartels Feb 13 '13 at 16:22

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.

• Yes, I think often I don't need replacement in a constructive setting because I have available suitable inductive constructions. – Andrej Bauer Feb 10 '13 at 21:06
• And in 'ordinary mathematics', does one use an arbitrary endofunctor and need to construct free algebras? In all 'ordinary cases' wouldn't we have some sort of properties of the category at hand/objects of the category at hand/the endofunctor that allows a workaround? – David Roberts Feb 10 '13 at 22:51
• @David: of course many endofunctors do not have free algebras at all. That aside, it is certainly convenient to have a global result such as theorem 1 here: ncatlab.org/nlab/show/transfinite+construction+of+free+algebras, and I'm not sure one can prove that without a replacement scheme in the background set theory. But you're right that significant instances of such a result can be proven in say ETCS (without replacement); e.g., I think existence of free algebras for "polynomial" endofunctors is no problem. The small object argument is probably a good acid-test case to consider. – Todd Trimble Feb 11 '13 at 1:39
• Computer scientists like initial algebras of functors, and if they don't have to think about their existence they feel a bit like physicists who are allowed to differentiate everything they like. – Andrej Bauer Feb 11 '13 at 6:02
• Yes, I meant in the general context of the page you link to, rather than arbitrary endofunctors on arbitrary categories. – David Roberts Feb 11 '13 at 7:07

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.

• But Borel Determinacy is surely a great example of the sort of thing that is known and loved by logicians but which is never used in "ordinary mathematics" (by which I mean e.g. "the things talked about over the last 20 years in the Harvard number theory seminar"). So if this is what you are looking for then perhaps I've misunderstood the question? – user30035 Feb 10 '13 at 22:55
• Borel determinacy is a theorem in real analysis, and therefore part of "ordinary mathematics". Maybe it's not an important theorem in real analysis, but it is indisputably a theorem in real analysis. – arsmath Feb 11 '13 at 0:47
• Hm, I'd call it a theorem of descriptive set theory with applications that are occasionally useful to workers in real analysis. (Maybe you could place it on the border of real analysis, but not necessarily in the interior (-: .) Such quibbles aside, it seems to have "ordinary mathematics" content. – Todd Trimble Feb 11 '13 at 1:51
• Unimportant or underused... This one is a tough call! – François G. Dorais Feb 11 '13 at 2:28
• Well, let's not fret too much about what is ordinary. I am just trying to avoid having listed obvious stuff of the sort "there is life beyond $V_{\omega + \omega}$". I do think Borel determinacy is border-line (descriptive) set theory, but the cool thing is that replacement creeps up in a non-obvious way. – Andrej Bauer Feb 11 '13 at 6:01

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.

• +1 for the algebraic example, but I'm dubious that it counts as 'ordinary mathematics'. It certainly seems more ordinary than Borel determinacy, though. – David Roberts Mar 5 '13 at 5:03
• Game theory is not ordinary mathematics? Gale-Stewart games arose as an attempt to extend the determinacy of finite-length zero-sum games to infinite games. David Gale was a mathematical economist who's most famous for the Gale-Shapley stable matching algorithm that helped Shapley win the Nobel Prize in economics. Once determinacy of Gale-Stewart games for open and closed sets was shown, it's a natural question to wonder if it holds for sets higher in the Borel hierarchy. The theory of infinite games just turned out to be really, really hard. – arsmath Mar 5 '13 at 10:47

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.

• Actually, what they do is construct a small category of schemes starting from an arbitrary set of schemes, which is closed under the usual operations. This is so that sheafification and other topos-theoretic notions can be treated without worrying about size issues. In big-picture applications, such as FLT or other questions of number-theoretic interest, one can assume that the set of schemes one starts with is comparatively small, and I would be surprised if the general construction you mention wasn't a huge overkill. – David Roberts Feb 11 '13 at 1:44

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.

• There is an ambiguity in "Wiles's proof uses". Do we mean literally the proof Wiles gave, together with the cited prerequisites, which include Grothendieck-style category-theoretic work? Or do we mean a trimmed-down version that replaces that general machinery with the specific instances actually needed? The former would involve Grothendieck universes, which are way beyond $V_{\omega+\omega}$. The latter needs less than $V_{\omega+\omega}$. I believe Colin McLarty is the expert on trimming down the prerequisites for Wiles's proof. – Andreas Blass Feb 10 '13 at 20:20
• In short -- Andreas, your comment is absolutely correct, but I mean "use the trimmed-down version". It's just a historical accident that the person who wrote some of the things Wiles needed decided to write them in such generality that he got entangled in set-theoretic issues. There is no replacement or separation-applied-to-gigantic-sets or large cardinals or Grothendieck universes in Wiles' actual underlying argument. – user30035 Feb 10 '13 at 21:00
• For more on FLT and "large sets" (including BCnrd's opinion) mathoverflow.net/questions/35746/… – user9072 Feb 10 '13 at 22:30
• It is not true that Bourbaki's set theory "does not include the axiom [scheme] of replacement". Replacement (or some version thereof) is included in axiom scheme S8 (E.II.1.6). (At least in the 1970 version; I do not know about older versions.) – Fred Rohrer Feb 11 '13 at 6:27
• @FredRohrer according to Mathias, replacement did not appear in the older editions of Bourbaki, but was added later. dpmms.cam.ac.uk/~ardm/bourbaki.pdf – Benedict Eastaugh Feb 11 '13 at 10:51

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.