[FOM] Foundational Challenge

[Peter LeFanu Lumsdaine]

On Mon, Jan 13, 2020 at 12:29 AM Timothy Y. Chow <tchow at math.princeton.edu>
wrote:
>
> Joe Shipman wrote:
> > I claim that alternative foundations for mathematics ought to meet a
> > similar test---help working mathematicians find new results or reach old
> > ones more easily.
> >
> > Examples, please.
>
> In case you missed it in my other FOM post, here's a paper that explains
> how the authors have formalized pi_n(S^n) = Z in homotopy type theory.
>
> https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf

Just to forestall misinterpretations of what this paper shows: the version
of “pi_n(S^n) = Z” it proves is formally rather different from the
analogous theorem(s) of traditional algebraic topology — they’re “morally”
the same, and related to each other by interpretations of HoTT into ZFC,
but the comparison is a bit subtle.

The difference is somewhat analogous to giving a theorem about the
combinatorics of finite sets in ZF^– (or some other finite set theory),
versus giving it in PA using some coding/model of finite sets as numbers.
In ZF^–, the sets are “native”/“primitive” objects.  In PA, there’s a
coding involved: so the PA version is in some senses stronger (since it
tells us something about the specific coding), but in other senses weaker
(since the ZF^– proof can be interpreted in other models of finite set
theory as well).

Similarly, the HoTT statement/proof of “pi_n(S^n) = Z” is in a foundational
system that has spaces as native/primitive objects; most traditional
versions of the theorem in ZFC use set-based models of spaces (e.g.
topological spaces or simplicial sets).  So the HoTT version of the theorem
is in some senses weaker than the traditional ones (deducing those from it
requires showing that some set-based model of spaces is indeed a model of
type theory), but also in some senses stronger than them (since it can be
interpreted in other models of spaces as well).

The question of whether this theorem meets Harvey’s test is interesting,
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.

Best,
–Peter.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200113/7ed089d1/attachment-0001.html>