22

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

Andrej Bauer
  • 47,834
  • 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
  • 1
    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
  • Zhen Lin: Can you modify that and talk about the various hierarchies (Borel, arithmetical, analytical, projective, etc.) which are constructed by induction, and/or transfinite inductions? – Asaf Karagila Feb 10 '13 at 19:01
  • I mean unbounded quantifiers. @Zhen: I added a clarification which excludes your example. – Andrej Bauer Feb 10 '13 at 19:11
  • It's very difficult to say what "ordinary mathematics" is -- I would even say that this sort of phrase could be interpreted as being "subjective and argumentative" :-) Let me suggest a related, perhaps more precise, question, which might capture the flavor of what you're after -- you could ask whether the proofs of the Poincare Conjecture or FLT use things like replacement. In the case of FLT I'm pretty sure that Wiles' proof does not use replacement. – user30035 Feb 10 '13 at 20:08
  • 1
    Add a logic tag? – Jason Rute Feb 10 '13 at 21:09
  • @Zhen - what is the codomain of this function? Isn't it just $\omega + \omega$? So if one thinks structurally, i.e. isomorphism invariantly, one is trying to define a function whose codomain is isomorphic (as a set) to $\mathbb{N}$ But also, it makes no sense structurally to define a function with a codomain you cannot prove exists (one could of course say $\exists \omega + \omega \Rightarrow \exists (\n \mapsto \omega + n)$). – David Roberts Feb 10 '13 at 22:45
  • 1
    Should this be a wiki? – Andrej Bauer Feb 11 '13 at 06:03
  • @David – My example does not make sense in structural set theory by design. I am thinking of the fact that $V_{\omega + \omega}$ is a model of Mac Lane set theory (hence of $\Delta_0$-separation). $V_{\omega + \omega}$ believes there exist uncountable well-ordered sets (using the Hartogs construction, say), but obviously it does not believe in the von Neumann ordinal $\omega + \omega$. – Zhen Lin Feb 11 '13 at 08:24
  • 3
    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
  • 2
    My last comment above should say BZC, not BZFC. (The F is what adds Replacement, so it's exactly what we do not want. Hopefully, nobody was confused, since there is no BZFC; Replacement implies unbounded Separation.) – Toby Bartels Oct 29 '19 at 17:24
  • 1
    I've been vocal in this space, but these days I prefer the term "generic mathematics" (and "generic mathematician"), rather than "ordinary mathematics". The term is less loaded, and conveys a better idea for me of what is meant. The allusion to mathematical genericity is entirely intentional. – David Roberts Jul 22 '21 at 02:17
  • 1
    @TobyBartels: Your last comment replacement seems to say that bounded replacement implies unbounded separation. But I don't think so. – user21820 Jun 17 '22 at 13:31
  • @user21820 : I meant that unbounded Replacement implies unbounded Separation. But it would make sense to interpret BZFC as incorporating only bounded Replacement, like in Kripke–Platek set theory, so my parenthetical remark is wrong for that reason. – Toby Bartels Jun 19 '22 at 05:03
  • @TobyBartels: Yes I have always viewed bounded ZFC as having both bounded specification and replacement. By the way, do you know if bounded ZFC proves Borel determinacy? – user21820 Jun 19 '22 at 06:19
  • @user21820 : I don't know, but this post (by Tom Leinster) argues that BD doesn't require very much in the way of Replacement. – Toby Bartels Jun 20 '22 at 09:50
  • @TobyBartels: Thanks, yes I saw that post, so we know that if there are no other 'dangerous moves' then all we need is to be able to construct (Pow^k)(ℕ) for any countable ordinal k. But I don't know whether we can do that in BZFC, nor whether we can obtain the ordinal rank of any Borel set in BZFC. Even KP^P+AC (where KP^P is as defined by Mathias in "The Strength of Mac Lane Set Theory" (Section 6.1)), which has inbuilt Powerset, is not obviously sufficient. – user21820 Jun 20 '22 at 10:12
  • Agreed. I'm not familiar enough with models of various set theories to say that it can't be done, but I still don't see how to do it. – Toby Bartels Jun 21 '22 at 15:13

6 Answers6

21

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.

Cody Dance
  • 603
  • 3
  • 8
  • That's what I am looking for! Thanks. – Andrej Bauer Feb 10 '13 at 21:08
  • 4
    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
  • 7
    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 00:47
  • 6
    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 01:51
  • 4
    Unimportant or underused... This one is a tough call! – François G. Dorais Feb 11 '13 at 02:28
  • 1
    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 06:01
  • Friedman showed, and others refined, that you need iterations of the powerset construction countable-ordinal-many times, applied to the game tree in question. Replacement is usually used to construct these, but it's a very localised usage. Starting from a Polish space, and payoff from a Borel set therein, I believe it's enough to ask that $\beth_\alpha$ exists for all countable ordinals $\alpha$. – David Roberts Jul 22 '21 at 02:15
20

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.

Todd Trimble
  • 52,336
  • 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
  • 1
    @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: http://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 01:39
  • 5
    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 06: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 07:07
13

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.

Community
  • 1
Adam Epstein
  • 2,440
  • +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 05 '13 at 05:03
  • 4
    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 05 '13 at 10:47
  • 2
    @arsmath it's been a long time, but yes, game theory is 'ordinary' mathematics (these days I would say "generic" instead, the term is less loaded). Game theory with payoff sets being arbitrary Borel sets of trees labelled by an arbitrary set? Less so, though I take my hat off to the people who get results in this area. If someone finds a use of nontrivial Borel determinacy for a non-Polish space in economics, they deserve more than a Nobel prize! – David Roberts Jul 22 '21 at 02:12
  • But KP^P+AC proves these. So arguably only bounded specification and replacement are needed for them. No? – user21820 Jun 17 '22 at 13:20
6

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.

Adam Epstein
  • 2,440
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.

arsmath
  • 6,720
  • 5
    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 01:44
4

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.

user30035
  • 529
  • 6
    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
  • 1
    Grothendieck's proof of his criterion for an abelian category to have enough injectives (brilliantly generalizing the case of modules over a ring) uses transfinite induction on Hom-sets. Unrelated to that, Kisin is the real expert on trimming down the prerequisites for Wiles' proof. :) – user30180 Feb 10 '13 at 20:47
  • 1
    Wiles does use many facts from EGA/SGA, but Brian Conrad has told me that he has explicitly checked that he needs none of the Grothendieck-universe business. He might (indeed he does) assert that some ring represents some functor defined on e.g. the category of all complete local Noetherian rings with residue field some fixed finite field, but he does not need that e.g. this category, or some subcategory of "small" objects, is a set, and any representing-functor arguments can simply be replaced with assertions which are not category-theoretic in nature but which do the job. – user30035 Feb 10 '13 at 20:50
  • 2
    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
  • 7
    For more on FLT and "large sets" (including BCnrd's opinion) http://mathoverflow.net/questions/35746/inaccessible-cardinals-and-andrew-wiless-proof/ –  Feb 10 '13 at 22:30
  • 2
    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 06:27
  • 2
    @FredRohrer according to Mathias, replacement did not appear in the older editions of Bourbaki, but was added later. https://www.dpmms.cam.ac.uk/~ardm/bourbaki.pdf – Benedict Eastaugh Feb 11 '13 at 10:51