[FOM] FOMUS/alternative foundations
louis.garde at free.fr
Thu Mar 24 02:30:34 EDT 2016
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
This "something" is I think what category theory brings to foundation of
mathematics, a direct approach to identify and study mathematical
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"...
More information about the FOM