[FOM] FOMUS/alternative foundations

[Louis Garde]

Thanks for your long answer, now I understand your point of view.

Le 23/03/2016 21:56, Harvey Friedman a écrit :

How does your first sentence compare with Garde:

"But my impression is that the more radical proposals, particularly
  HOTT, philosophical coherence is proudly thrown away."

This sentence was not from me, but from  you, I was just reacting on it !


You explain well in your answer that it is usually useless to try to 
explain "ideas" without solid facts behind:

"4. To the extent that it has any general purpose merits, I expect that
brief, simple, clear, convincing, well constructed, totally
transparent, accounts of at least something impressive can be and will
be presented that fits nicely on a moderate length FOM posting, so
that it can be readily contemplated, absorbed, and discussed."


I agree that though the HoTT book is very well written, your requirement 
is not met.
But I do not think it can be met, because you have to take time to think 
a bit differently to understand how it works and the interest of it.
Long discussions won't help...

I also agree with Sam Sanders's feedback on missing features for Type 
Theory as a foundation of mathematics.

When I took time to understand HoTT, it became clear to me that it 
grasps "something" related to foundation of mathematics that set theory 
does not.
This "something" is I think what category theory brings to foundation of 
mathematics, a direct approach to identify and study mathematical 
structures.
An an amateur, I was very surprised to realize that the understanding of 
the interest of category theory was not shared among people interested 
in "foundation of mathematics".

May be the real difference is one's intuitions of mathematical objects:
- with the classical foundations, mathematical objets are 'sets', 
structures are constructions on sets.
- with category theory and HoTT, mathematical objets are 'structures', 
and sets are just some specific structures.
But it's just my understanding of it as an amateur of logic, interested 
in "foundation of mathematics"...

Louis.