[FOM] foundations meeting/FOMUS/discussion

[Staffan Angere]

Harvey Friedman:
>>> Among the obvious merits of ZFC as a foundation for mathematics, there
>>> is one that I often see not sufficiently emphasized. That is, its
>>> PHILOSOPHICAL COHERENCE.
>>>
>>> ../..
>>>
>>> But my impression is that the more radical proposals, particularly
>>> HOTT, philosophical coherence is proudly thrown away.
>
> That is my understanding, which may or may not be correct. (However,
> see below for a pointer to an internet manuscript ).This certainly
> prima facie precludes HOTT as any kind of reasonable "foundation for
> mathematics" in any standard sense.

Caveat: I am not a member of the HoTT community, but just a philosopher enthusiastic about the project. First of all, not everyone agrees on ZFC's high "philosophical coherence". It was built piece-by-piece, and while some parts can be given coherent interpretations, it is not obvious that the whole can. I think a good classic critique of ZFC's coherence is Hallett's "Cantorian Set Theory and Limitation of Size".

Second, HoTT has an extremely high degree of philosophical coherence. Part of this is because Martin-Löf's original system was built with just that purpose in mind; his Bibliopolis book

https://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf

gives lots of philosophical arguments for why the extensional version of his system looks the way it does. 

That book does not however treat the intensional version, which HoTT is based on. But HoTT gets coherence from its geometric interpretation: every rule of the system can be motivated by that. When you are used to it, it is therefore a very intuitive system, which is probably roughly the same as what can be said for ZFC. The difference is that instead of visualizing in terms of collections of things or Venn diagrams, you visualize in terms of spaces and paths.

So the reason I (and I assume some other philosophers too) am excited about HoTT is precisely because of its philosophical coherence rather than, say, its computational properties. Those properties are important, but it shares them with other systems too. HoTT, on the other hand, is rare among challengers to ZFC in that provides not only a formal system but also very useful intuitive interpretations. This means that it can be used to give an alternate way of looking at or thinking about mathematical structures, which I have often found very enlightening.

...
> I found the following on the Internet:
> http://www.bristol.ac.uk/media-library/sites/arts/research/homotopy-type/documents/identity-in-hott-part-one.pdf
>Unfortunately, I do not see any indication of who the authors are of
>this internet manuscript, which is a bit strange and frustrating.

I assume that this has been prepared for blind review, which is why it doesn't have the authors stated. From the other papers they cite as being by them, however, we can see that (at least some of them) are philosophers at the University of Bristol, which has several philosophers interested in HoTT. I will not say more at the moment, since the paper may very well be under review by someone reading FOM right now.

The best introduction to HoTT is definitely the book



Best wishes,
Staffan