[FOM] Foundational Challenge

[Timothy Y. Chow]

Peter LeFanu Lumsdaine wrote:

> The question of whether this theorem meets Harvey's test is interesting,

I think you mean Joe Shipman?

> but has to acknowledge both sides of the difference between the theorems.
> I've seen seen each direction of it argued polemically before without
> acknowledgement of the other - ("the HoTT theorem is simpler and far 
> more general" / "the simplicity is an illusion, you still need to deduce 
> the real theorem about topological spaces from it") - and that kind of 
> argument gets old fast.

Indeed, some version of this debate has appeared on FOM previously, e.g.,

https://cs.nyu.edu/pipermail/fom/2014-October/018283.html

Shipman's suggestion seems to be to focus on the arithmetical content of 
the theorem, so as not to prejudice the challenge unduly in favor of ZFC.

Of course, this means that one has to find an arithmetical formulation of 
pi_n(S^n) = Z that everyone agrees captures the essence of the theorem.

Alternatively, if one wants to tip the balance in favor of HoTT, then one 
could ask for a ZFC proof of the HoTT theorem.  I'm not sure what Harvey 
Friedman would say about that---perhaps the HoTT theorem is not 
"philosophically coherent" enough to be a real mathematical theorem in its 
own right?

Tim