Bourbaki and foundations
Timothy Y. Chow
tchow at math.princeton.edu
Thu May 19 00:32:46 EDT 2022
John Baldwin wrote:
> However, Voevodsky raises different objections at
> https://www.ias.edu/ideas/2014/voevodsky-origins
>
> "There were two main problems with the existing foundational systems,
> which made them inadequate. Firstly, existing foundations of mathematics
> were based on the languages of predicate logic and languages of this
> class are too limited. Secondly, existing foundations could not be used
> to directly express statements about such objects as, for example, the
> ones in my work on 2-theories. "
>
> I would appreciate anyone who can further clarify this objection.
This topic has been discussed on FOM before; see for example
https://cs.nyu.edu/pipermail/fom/2011-June/015541.html
Basically, Voevodsky was unhappy with the technical nuisances that arise
if one tries to formalize higher category theory in ZFC. If you don't
know what higher category theory is, there's a brief introduction here:
https://ncatlab.org/nlab/show/higher+category+theory
Intuitively, when we define the category of all sets, we want to consider
the set of all sets, but we know we can't formally do that. One way to
circumvent the problem while staying within ZFC is to speak instead of the
*class* of all sets, and to define classes as formulas. However, in
higher category theory, one (roughly speaking) wants to iterate the
process of categorification an arbitrary number of times. The dodge of
defining classes to be formulas doesn't cut it.
One of the standard ways to deal with this issue is to introduce
universes. This more or less solves the problem, but at a cost: you have
increased the logical strength of your foundational system. Maybe you
don't care, but some people find it annoying that the impression is
created that higher category theory "requires strong axioms" when it
arguably doesn't really. For any theorem of higher category theory that
people really care about, it seems that a reflection argument can be
crafted to prove conservativity over ZFC. The trouble, however, is that
it isn't so easy to write down a meta-theorem to take care of all such
worries in one fell swoop. I gave the following link in one of my
previous FOM posts, but here it is again if you want a more detailed
discussion of this point:
https://mathoverflow.net/questions/382270/reflection-principle-vs-universes
Voevodsky felt that Homotopy Type Theory, which is based on the Calculus
of Inductive Constructions plus the Univalence Axiom, allowed one to build
the foundations of higher category theory in a more natural and less
technically annoying manner. Again, when Voevodsky said that traditional
foundations are "limited" or "inadequate," I don't think the claim was
that it's *impossible* to use ZFC or ZFC + universes; the claim was that
doing so is cumbersome and does not highlight the essential structure of
the entities one is studying. In particular, formulating the subject
using Homotopy Type Theory shows that logical strength of many of the
fundamental theorems is lower than you might think; this ought to be a
selling point for any fan of reverse mathematics.
By the way, it's worth noting that Jacob Lurie, who understands higher
category theory as well as anyone in the world, is (or was, the last time
I checked) not completely convinced that Homotopy Type Theory is *the* way
to approach the foundations of higher category theory. See the discussion
in the comments here:
https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/
I mention Lurie not to cast doubt on Voevodsky's views, but to emphasize
again that what's being debated is not whether traditional foundations
*can* do the job, but whether an alternative approach is easier or more
elegant or more enlightening. It should not be surprising that such
questions are a matter of opinion and are up for debate and discussion.
Tim
More information about the FOM
mailing list