Bourbaki and foundations

[Timothy Y. Chow]

On Fri, 13 May 2022, Lawrence Paulson wrote:
> I wrote a blog post a while back trying to clarify some of these points, 
> in particular my view that a foundation has only one real purpose, 
> namely to justify how mathematics is done:
> 
> https://lawrencecpaulson.github.io/2022/03/16/Types_vs_Sets.html

Near the end of this blog post, you wrote, "Axiomatic set theory also 
gives us a critical warning: you risk inconsistency if you assume 
collections that are too big. ... Their very starting point, Set, is the 
category of all Zermelo–Frankel sets. What on Earth do they need all of 
them for? No one has ever told me."  Perhaps this is just a rhetorical 
flourish that is not intended to be taken too seriously, but if we set 
aside the debate about categories versus sets as a foundation, there are 
certainly very good reasons to consider the category of all X, where X is 
some kind of mathematical object, and it's not clear that such a category 
is "too big."

Categories illuminate the structure of the mathematical objects we are 
studying.  They simplify many conceptually straightforward but fussy 
arguments that otherwise would be tedious and error-prone.  Brian Conrad 
has a quip: "Before functoriality, people lived in caves."  There are many 
constructions in (for example) algebraic topology and algebraic geometry 
that are most naturally stated in terms of category theory.  As one random 
example, etale cohomology might not be impossible to define without 
category theory, but it would be painful, and it's unclear why you would 
even try unless you were strongly committed to avoiding categories.

When I say that it's not clear that (for example) the category of all 
schemes is "too big," I mean that the things people want to *do* with the 
category of all doohickeys are not the sorts of things that trigger 
paradoxes.  Often there is some concrete context in the back of their 
minds in which these abstract constructions are intended to be executed; 
in that context, everything can in principle be done using much weaker 
axioms and much smaller sets than the official account makes it seem. 
This is obvious to those who actually work with these things; Brian 
Conrad, again, emphasizes that if you actually understand the proof of 
Fermat's Last Theorem, then it's obvious that the axiom of universes is 
not really needed.

So you might ask, if there is no real need for such "big" things, why 
introduce them at all?  The same question can be raised about the axioms 
of set theory.  Why assume that *every* set has a power set or that an 
*arbitrary* Cartesian product of *arbitrary* nonempty sets is nonempty? 
Well, it's a lot simpler to make such an assumption than to build in extra 
hypotheses.  Extra hypotheses force you to constantly pause along the way 
to check that they continue to be satisfied, and irrelevant bookkeeping is 
precisely what one is trying to avoid when one axiomatizes.  (This may be 
a reason that Solovay's model never caught on with the general 
mathematical public---checking that you only need Dependent Choice is kind 
of annoying.)  The only reason to introduce the hypotheses is if you're 
genuinely worried about something bad happening, and most categorical 
constructions aren't really dangerous.

This isn't to say that one *never* has to worry about ambitious 
constructions running into paradoxes.  Peter Scholze asked an interesting 
question on MathOverflow that illustrates some of the concerns of those 
working on the front lines:

https://mathoverflow.net/questions/382270/reflection-principle-vs-universes

It is not necessary to understand all the technical details to recognize 
that, like so many things in life, there is a tradeoff between security 
and convenience.  If Risk Assessment is uppermost in your mind, as it is 
for security professionals and as it seems to be for Lawrence Paulson, 
then you're going to want to build in as many safeguards as you can.  But 
for most users and customers, Essential Guidance and convenience are their 
primary concerns.

Tim