Bourbaki and foundations

[Timothy Y. Chow]

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