alternative foundations of mathamatics

[Hendrik Boom]

There's a rollicking discussion of alternative foundations for mathemetics
going on the Foundations of Mathematics mailing list right now.
Archives at http://www.cs.nyu.edu/pipermail/fom/

Some of the discussion is about type theory, and in particular,
homotopy type theory.

-- hendrik

By the way, that's a actively moderated mailing list -- and moderation
involves more than just a human-mediated spam check. I recall I
had to explain why I wanted to be on it to start receiving it.

[Matt Oliveri]

AFAICT, the main disagreement between Harvey Friedman and the HoTT proponents is simply over what "foundation of math" should be allowed to mean.

The HoTTists would have that a foundation of math is any formal system rich enough to do mostly any kind of math.

Friedman has the very stringent additional requirement that the system have a self-contained explanation from first principles, that's "philosophically coherent" enough to compete with ZFC as a main tool for understanding foundational issues.

Of course, this additional requirement is of no use to a mathematician on a day-to-day basis. So I suppose it's understandable that they would want to relax and simplify the definition of "foundation of math". Of course the additional requirement is very important to the folks who think about foundations in the traditional sense.

Essentially this same divide seems to have existed for a long time, with the categorically-motivated "foundations" not caring to address foundationalist concerns.

John Baez said something interesting:
"Third, because people interested in categorical foundations are interested in formalizing mathematics in a way that fits how mathematicians actually think, and different mathematicians think in different ways at different times, we tend to prefer what you call a "multi-foundational" approach.  Personally I don't think the metaphor of "foundations" is even appropriate for this approach.   I prefer a word like "entrance".  A building has one foundation, which holds up everything else.  But mathematics doesn't need anything to hold it up: there is no "gravity" that pulls mathematics down and makes it collapse.  What mathematics needs is "entrances": ways to get in.  And it would be very inconvenient to have just one entrance."

They *know* that what they're doing is not really foundations! They just ended up calling 'em that anyway, somehow! Anyway, for some reason the conversation didn't end there. Not even close.