| The FOM folk are in general incredibly bearish on proof assistants, so of course they don't care. If you only care about an 'ultimate' foundation that is the best fit to evaluate other systems, rather than a foundation that is amenable to actively working with it, of course you have no reason to care about HoTT. If you share their opinion, alright, but I personally find this incredibly myopic. >People definitely say this. See, for instance: https://mathoverflow.net/questions/90820/set-theories-withou.... And note that not just the questioner but also many commenters assent to that claim. See also the paper Set Theory and Structures by Barton and Friedman, starting p. 15: http://philsci-archive.pitt.edu/14633/1/2017_04_set_theory_u.... I haven't read through all comments, but as far as I see people are actually just criticizing that the encoding is always relevant - that is, they can't talk about objects without encodings, but they don't actually care about the theorems regarding the encoding itself. I think this is fundamentally different from saying 'set theory proves 4 is an element of pi' because otherwise you could levy the same criticism against type theory! After all, there's nothing preventing people from encoding the natural numbers as sets in type theory. The benefit of type theory is that instead you can talk about objects without regard for the encoding which isn't possible with ZFC. >I am not totally sure about the distinction you are trying to draw here. But I reject the claim that, properly understood, ZFC allows you to prove or state such a thing.
>Now, of course pi is not, philosophically speaking, the same as the set used to encode it. (And in fact there are many ways to do this encoding.) So one cannot even state questions like "Is 3 a member of pi?" in set theory, because 3 and pi are not sets. I guess it matters on how you view it exactly. Under your view you can't state it, but this comes at the cost of not being able to make any at all statements about objects rather than just specific encodings! I'd wager that the vast majority of people would be unsatisfied with this for actively doing mathematics. When people want to talk about the natural numbers, they don't actually care about the specific encoding, they just want to talk about the objects. The way I see it, if I want to talk about the objects 4 and pi in set theory, I have to consider an arbitrary set that encodes it. Now, because these are still just sets, I can state '4 is an element of pi', but not prove it, because whether it's actually true depends on the specific encoding. This isn't great either, but I think this is a lot closer to how people actually work. >If my concern is studying the foundations of mathematics, I have not seen a reason why I ought to prefer HoTT over ZFC. When studying foundations itself ZFC is king, but no one is contesting that. Even HoTT fanatics will admit that its complexity makes it less amenable for certain situations. >If my concern is formalizing mathematics, Lean seems to be doing a much better job I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics? Then your dislike of HoTT is even more confounding to me. HoTT is just an extension of intuitionistic type theory. If there's a mature HoTT implementation that stands the test of time (e.g. potentially a fully fleshed out version of cubical type theory), Lean is almost certainly going to incorporate it. Univalence is very much part of 'natural' reasoning, if I show a property for one encoding, I want to be able to transfer that to any other encoding. There's even already an experimental library for Lean that allows you to use univalence. It's just that generally Lean is a lot more conservative rather than experimental. They're not doing a better job because their theoretical foundation is better - it's simply that Kevin Buzzard and his troop is actually putting in the work of doing a lot of formalization. >And HoTT gets something like 10x more attention than Lean does on HN. Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory, whereas Lean is 'just' people formalizing existing mathematics. I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years. Not only that, but HN isn't a mathematics forum - his work seems about as popular as Coq and Agda here, even though the latter have a far more material impact on software engineering. HoTT is uncharacteristically popular as well, but at the very least there's a chance that it could change the face of formal verification! |
> If you share their opinion, alright, but I personally find this incredibly myopic.
I want to distinguish between two senses of "foundation of mathematics":
1) An ontologically minimal language to formalize mathematical reasoning and facilitate proving things about (in)consistency, provability, and relative theory strength, and generally doing metamathematics.
2) A language to actually carry out the details of formalizing mathematics, perhaps jointly by humans and computers, in the sense of the Xena Project and proof assistants.
Here is a claim which might annoy you, but really ought to be uncontroversial: the correct meaning of the term "foundation of mathematics" is the first one. This is what it has meant for about a hundred years, at least, and what someone working professionally in the reverse mathematics/set theory/model theory/logic communities will understand the phrase to mean if you use it in conversation with them.
Now, given this, and given you agree that ZFC does a better job at function (1) above, I think this explains why the FOM people (and more generally those in the communities I listed) find it strange when HoTT is suggested as a "foundation of mathematics." (I can't speak to their opinions on proof assistants, though.) You can see this quite explicitly when Harvey Friedman starts asking questions of the HoTT people; he always asks something about ontological parsimony, remarks how simple the ZFC axioms are (and tells a story about explaining them to his barber, or whatever), and remarks how homotopy is much too sophisticated a concept to be truly foundational.
Moreover, they are going to regard any criticism that ZFC is deficient because it's a poor choice for function (2) as totally besides the point. That's akin to arguing that Turing machines are a poor choice for the foundations of computational theory because it's hard to program them in practice. The same response to applies to your second point about how type theory is "closer to how people actually work"; this was never a figure of merit in the first place.
So, I indeed share this view, but I don't think it's myopic. I think it follows immediately from what a "foundation of mathematics" is.
> I'm not sure I understand. So you _do_ accept intuitionistic type theory as a valid alternative to ZFC when one actually wants to formalize mathematics?
Yes, with the caveat noted below. The practical formalization of mathematics is an engineering problem, not properly speaking one of foundations, as discussed above. This is not to say it's not a deep and interesting problem, just that the difficulties there are mostly orthogonal to those encountered when doing, e.g. metamathematics. One ought to do whatever makes formalization easiest for practitioners.
> Because HoTT is actually experimental research that could be a breakthrough for intuitionistic type theory
This is not compelling to me because I think intuitionism is boring and misguided. I think the majority of practicing mathematicians feel the same way. Of course, you can just add axioms to make it classical, but I'd wager the emphasis on intuitionism is another thing that turns people off from HoTT.
> I'm actually rather surprised that Kevin Buzzard's work is so popular here - he's certainly doing great work, but there hasn't really been any significant news for the past years.
He and his crew have actually formalized a good chunk of real mathematics. That's fairly significant, in my mind.
(You have probably already read this, but in case someone reading this post doesn't know what I mean: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....)
Also, given that it's an engineering problem, there are going to be a bunch of difficulties that only pop up once you start playing with it. So the fact that a group of people have started playing with it, and found some of these problems, and iterated Lean in response – that's good!