[FOM] TypesHoTT discussion

[Harvey Friedman]

I just replied to Roux Cody in his public email that was forwarded to
me. His original email is at
https://plus.google.com/110536551627130071099/posts/6TiKLxjSCnu I
think that his posting and my reply would be of interest to FOM
readers.

reply to cody

"... what could be a constructive and interesting mailing list on the
Foundations of Mathematics (affectionately FOM)"

FOM is the most constructive and interesting mailing list on f.o.m.,
though it has not even come close to realizing its potential.

"has become a toxic cesspool of argument and posturing."

What I see on the FOM is:

i. Announcements of research progress.
ii. Announcements of meetings.
iii. Links to papers and books.
iv. Questions at various levels of technicality about f.o.m. related matters.
v. Answers or proposed answers to such questions.
vi. Inquiries concerning references and the literature on various
f.o.m. related matters.
vii. Discussion of some topics in f.o.m.

I think you are mainly critical of vii and not i-vi?

The discussion gets particularly intense when points of view that are
seriously alternative to the conventional wisdom in standard f.o.m.
are presented.

Generally speaking, when such seriously alternative views are
presented, several principal contributors to the list will inevitably
call for direct simple explanations that can be readily absorbed and
debated.

This is a normal reaction and is very productive and healthy, since it
places a burden on alternative ideas and conceptions to be
particularly transparent and convincing.

Furthermore, those that call for such transparent clarity are
generally honest, in that they are perfectly willing to be subjected
to that same standard.

"The reason is very standard, and is caused by what I suspect has been
the downfall of tens of thousands of mailing lists: the complete
domination of the list by an un-moderated and belligerent poster."

I do not "completely dominate", I am not "un-moderated", and I am not
"belligerent" in the usual sense of the word.

Most of my postings, even those that are non technical, probably do
not get replied to. The technical ones rarely get replied to. I also
don't seem to have a good track record of changing anybody's opinions.

"Anyone who's been on the list will instantly recognize the person in
question with no difficulty. The real killer here is the inability to
moderate: the person in question is a respected member of the
community, and also a moderator of the list himself."

I am not a moderator of the FOM. Martin Davis is the sole moderator. I
am on the Editorial Board. My postings are moderated like everyone
else's. The Editorial Board is consulted by the moderator whenever
there is an issue concerning moderation. Anybody on the Editorial
Board who is viewed as an interested party - especially if they are
the author of a suspect post - is automatically excluded from the
discussion in the Editorial Board.

Over the years, many of my postings have been rejected as
inappropriate, or accepted only upon revision.

"But apparently Type Theory (and HoTT in particular, though I'm not
sure the person in question really knows the difference)"

most specifically, some bizarre axiom of univalence...

"can inspire just as much vitriol, presumably because there's not
enough brainpower in the world to study more than 1 foundational
system at once."

I study classical f.o.m. and also constructive f.o.m. following
Hetying, Brouwer, Bishop.

"Amusingly, set theory, or rather, the ZFC variant, which is proposed
as the One True Foundation which cannot be improved in any way, "

It can be sugared, and/or augmented with large cardinal axioms.

"was under remarkably similar criticism at it's inception about a
century ago. This seems like a classic case of "get off of my
foundational lawn, you darn kids!". In the case of set theory,
foundations of mathematics were so young and shaky that some of the
"con" party were even advocating against the ability to mathematically
describe the foundations of mathematics at all! Poincare was one of
the big proponents of this, amusingly, he made some rather
embarrassing mathematical errors of his own, suggesting he might have
benefited from a more formal mindset (though his actual contributions
shouldn't be understated!)."

ZFC has been the gold standard f.o.m. for about 100 years, and
generally accepted, for very very good reasons.

"The attacks on HoTT and type theory aren't quite as eloquent, though.
On one hand, there is the argument that type theory is just not as
convenient as set theory in the practice of computerized
formalization. One might be able to make this case, but it's tougher
to make if one hasn't been involved in the design of a such a system,
or indeed any large scale formalization of this sort."

I invite you to join the discussion! ZFC and especially the big
earlier developments leading up to it involved many great philosophers
who made a business of taking philosophical coherence very seriously.
Prima facie, departing from that tradition for f.o.m. looks to be a
particularly bad idea.

"The more recent attack is on the "philosophical coherence" of the
foundation. This is particularly annoying to me, since Martin-Löf has
written extensively on this, but this was brushed aside when
mentioned. This seems like a pretty clear sign that level headed
discussion is not going to happen. I guess I could have reached this
conclusion years ago, when similar debates were already happening on
this list."

The fact that someone has written extensively on something doesn't
mean that it is convincing to everybody - or even many people -
involved. If somebody can make a clear and convincing case of
philosophical coherence, especially in comparison with what is already
accepted as philosophically coherent, in an appropriate FOM posting,
then that would further the discussion.

Harvey Friedman