[FOM] Foundations

[Rempe-Gillen, Lasse]

I have been hesitant to comment on the current discussions concerning HoTT and set theory - I am an expert in neither, and moreover have not been able to keep up with all that has been written in this interesting exchange of ideas. Still, as a research mathematician outside of homotopy theory or category theory, I thought two thoughts might be worth sharing.

One of the first things that came to my mind with regards to the HoTT question was an analogy with programming languages, where different approaches will be appropriate in different settings. Indeed this is an analogy that I have seen made a number of times by others in the discussion. However, I believe it is not quite right. Programming languages are not the foundation of computer science; rather models of computation are.

So a claim that there is a new, and improved, general foundation of mathematics should perhaps be compared to a claim that some new model of computation must replace the Turing machine as the foundation of computer science. Clearly there would need to be some major evidence of clear and general advantage for this to ever be accepted generally (I cannot see it happening). If I understand correctly, this is one of the points that Harvey Friedman has been trying to make.

Of course, there are significant differences - in CS, one would expect a new model of computation to be swiftly shown equivalent to TMs, and then anyone might use one or the other as they choose. Things are a bit more complicated in FOM, but the analogy still seems useful.


My second point is that I am uncomfortable, as a mathematician, with some of the language used by the proponents of HoTT. As they are the main representatives of research mathematics (as opposed to the FOM point of view) in this discussion, it might be worth adding my voice.

As much as I greatly respect John Baez, on the Google+ thread referenced in recent posts, he seems to claim to represent "modern mathematicians"; e.g. he states that HoTT apparently reflects 'how modern mathematicians actually think'. This effectively dismisses vast parts of active mathematical research as not being "moden mathematics". I find it hard to see how HoTT would be a better foundation for my work in complex analysis than set theory. I suspect the same would be true for a majority of recent Fields Medalists.

I know a number of colleagues, whom I trust enormously, who are very excited about HoTT, so there is clearly something there. But what they all have in common is that they already have a very category-theoretical approach to mathematics. My suspicion is that this is a development of great benefit to certain mathematicians, but falls short of representing a feasible foundation for mathematics as a whole.

In any case, it should be clarified what is HoTT's relation to established set-theoretical foundations, so that we [other mathematicians] can understand the status of results established using its formalism.


--------------------------------------------------------------
Professor Lasse Rempe-Gillen
Dept. of Math. Sciences, Univ. of Liverpool, Liverpool L69 7ZL
Office 520; tel. +44 (0)151 794 4025, fax +44 (0)151 794 4061
http://pcwww.liv.ac.uk/~lrempe
--------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160412/a08ed72d/attachment-0001.html>