[FOM] foundations meeting/FOMUS/discussion

Louis Garde louis.garde at free.fr
Sat Mar 19 12:18:30 EDT 2016

Le 18/03/2016 04:40, Harvey Friedman a écrit :
> Among the obvious merits of ZFC as a foundation for mathematics, there
> is one that I often see not sufficiently emphasized. That is, its
> ../..
> But my impression is that the more radical proposals, particularly
> HOTT, philosophical coherence is proudly thrown away. If my impression
> is correct, then that would make it rather unlikely that HOTT could
> play a significant general purpose role in any kind of foundation for
> mathematics addressing refined notions of "workable" as we are
> discussing.
Could you clarify what you mean by "philosophical coherence"?
Don't you think that constructiveness brings a very strong 
"philosophical coherence" ?

With my own understanding, the philosophical coherence of Martin Löf's 
intuitionistic type theory is at least as strong as ZFC's one.
And, to put it very briefly, HoTT is a natural extension of it: its 
definition of identity types makes it applicable to homotopy theory, but 
you do not need homotopy concepts to justify the rules defining identity 


More information about the FOM mailing list