[FOM] foundations meeting/FOMUS/discussion

[Louis Garde]

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
> PHILOSOPHICAL COHERENCE.
>
> ../..
>
> 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 
types.

Louis.