Bourbaki and foundations
Timothy Y. Chow
tchow at math.princeton.edu
Fri May 13 07:45:39 EDT 2022
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
More information about the FOM
mailing list