27
$\begingroup$

In a recent lecture at the Vladimir Voevodsky's Memorial Conference, Deligne wondered whether "the axioms used are strong enough for the intended purpose." (See his remark from roughly minute 40 in this video: What do we mean by "equal" ? - by Pierre Deligne.)

Can anyone comment on his doubt, and class of examples ? Are his worries to be taken seriously ?

$\endgroup$
  • 1
    $\begingroup$ I believe I watched that video, but can't recall the comment (I'll have to check out the time stamp you mention)—but HoTT+AC proves at least the consistency of ZFC (and even, for every $n$, the consistency of ZFC+$\exists\, n$ inaccessible cardinals). When I check the video I will measure up the examples against this. $\endgroup$ – David Roberts Mar 1 '19 at 15:30
  • 5
    $\begingroup$ There was a short discussion of this on the n-forum: nforum.ncatlab.org/discussion/9059/what-is-deligne-asking $\endgroup$ – Michael Bächtold Mar 1 '19 at 17:00
  • 3
    $\begingroup$ You may also look at Mirna Dzamonja's paper "A new foundational crisis in mathematics, is it really happening". $\endgroup$ – Mohammad Golshani Mar 2 '19 at 10:58
  • 5
    $\begingroup$ @MohammadGolshani I would not recommend that paper. $\endgroup$ – Mike Shulman Mar 8 '19 at 5:28
  • 3
    $\begingroup$ @ThomasKlimpel That's precisely one of the statements that I believe to be a caricature. I have never heard anyone in the HoTT community make any such claim, nor do I think it sensible to imagine that HoTT has anything to do with computers "doing our mathematics for us". To be sure there are people who believe that that is the future of mathematics, but they have nothing to do with HoTT as far as I know. $\endgroup$ – Mike Shulman Mar 11 '19 at 11:40
16
$\begingroup$

It is a bit difficult to understand what he is asking. The already-linked nForum discussion includes some clarification about his example, which at the meeting took us a while to figure out.

More broadly, I think that what he is asking is whether everything we can prove in ZFC about classically-defined homotopy theory (in terms of topological spaces or simplicial sets, say) is also provable in HoTT about synthetically defined homotopy theory. As he says, this is not answered by the result that one can construct a model of ZFC inside HoTT, since the classically-defined homotopy theory in that model of ZFC need not coincide with the synthetic homotopy theory in the model of HoTT that we started from.

If HoTT is understood as constructive, without LEM and AC, then the answer to this question is a simple "no": there are things we can prove about classical homotopy theory using LEM and AC that are not provable in constructive synthetic homotopy theory. For instance, as proven by Andreas Blass in Cohomology detects failures of the axiom of choice, and reformulated in HoTT here, the axiom of choice is equivalent to the statement that every discrete set has vanishing $H^1$ with coefficients in any (not necessarily abelian) group. There are also important open problems in HoTT related to this, e.g. whether it is provable that a set-indexed wedge of circles is always a 1-type (which is true classically, and also in all known models of HoTT, particularly in every Grothendieck $(\infty,1)$-topos, but for which no internal proof in HoTT is known --- as far as I know).

I believe that if we add LEM and AC, the answer is probably still no. There are other "classicality axioms" for synthetic homotopy theory that I would not expect to be implied by LEM+AC, such as Whitehead's principle (a map inducing isomorphisms on all homotopy groups is an equivalence) or sets cover. An example is claimed here to show that HoTT+LEM does not imply Whitehead's principle, at least; I am not sure about LEM+AC, but I would be surprised since AC is only a statement about sets.

I think it is a very interesting question whether there is some finite list of "classicality" axioms we can add to HoTT that together ensure everything provable about classical homotopy theory in ZFC is also provable about synthetic homotopy theory in HoTT + those axioms. The combination LEM + AC + Whitehead's principle + sets cover is actually not a bad guess for such a list, since by "sets cover" we might be able to inductively build an internal "simplicial set" surjecting dimensionwise onto any given type and then use Whitehead's principle to show this is a realization equivalence. But that vague idea is a long way from a proof.

So are his worries to be taken seriously? I would say yes, but they should not be considered "worries" but rather opportunities! These are interesting research questions that could not even be asked pre-HoTT. If we discover that there is a sufficient list of classicality axioms, then that is a nice theorem that should resolve everyone's "worries". But if we continue discovering new classicality axioms that are not implied by those we already knew, then I think that's an exciting situation too. By expanding the world of mathematical foundations to include higher types, HoTT allows us to formulate and study the relationships between new axioms that didn't even make sense before.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.