| > Any arising confusion is unfortunate, but as long as it's clear what people mean, I don't see the issue and anyone who actually is able to differentiate between (1) and (2) should be able to understand what is meant from context. I don't think this is true at all! For example, maybe it is the case that HoTT proponents care solely about (2), and not (1), in which case my criticisms are misguided. But this is not at all the impression I get from reading what they write. Given I'm sensitive to the distinction between (1) and (2), and given I apparently can't infer the difference from context, what are we to conclude? That I just have poor reading comprehensions skills? Maybe so – in which case please help people like me out and use more precise terminology. OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology. > Sure and if this was the aim of HoTT, dismissing it for this reason would be legitimate, but it's not, as one can see by the reaction of HoTT people to these question: They'll deflect to (2) and do some spiel about 'entrances', because that's what they care about and refer to. I went back to the introduction to the HoTT book [0] to check, to make sure I'm not misremembering things. And they literally say: 'we therefore believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.' This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1). And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.' > Then why are there so many people arguing for ZFC as an option for (2)? Not only are there proof assistants based on ZFC and people who advocate for this, a lot of the inane ZFC vs ETCS or HoTT discussions on FOM are absolutely about (2). Hell, even Harvey Friedman has engaged often enough in this e.g. arguing that the ability to make nonsensical statements is actually good because mathematicians start their work by making statements that are often nebulous or wrong. Yeah, I agree with you. There's no a priori reason to believe ZFC is a good choice for this. > Are you referring to the development and study of formal systems such as CIC/intuitionistic type theory/HoTT or the actual development of proof assistants that implement these formal systems (Coq, Agda, Lean, etc)? Calling the former engineering seems quite strange to me and I don't see how you could reasonably claim that it's not metamathematics. Well, metamathematically speaking, the development and study of these formal systems is boring. They don't have anything interesting to say about consistency or provability or whatever, and (as I understand it) they're all mutually intepretable with ZFC (at least the versions used to actually formalize things in practice). So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants. > It's significant and needed work, but there hasn't been any significant news for non-mathematicians. From the point of someone not familiar with mathematics, they've essentially been doing the same thing for about four years. I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy. For a long time many people didn't take formalization seriously because it never touched "real" math, and now you're telling me I can do "real" math with it? To the point where undergrads are formalizing the standard undergrad/grad curriculum? That's huge! [0] https://hott.github.io/book/nightly/hott-online-1287-g1ac940... |
Sure, I just don't think it's going to happen. The HoTT (and category theory) people largely don't care about (1), so they typically don't need to differentiate. More cynically, it's probably also just better marketing, a new 'foundation' certainly sounds more impressive than just a new 'mathematical framework', especially because (1) is generally pretty esoteric.
>This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1).
I don't think so, look at how they actually define 'unformalized mathematics':
"Indeed, many of the proofs described in this book were actually first done in a fully formalized form in a proof assistant, and are only now being “unformalized” for the first time — a reversal of the usual relation between formal and informal mathematics."
The idea is essentially that using HoTT formalisms informally can lead to new insight, which is exactly what part 2 of the book focuses on and they're making it clear that it's about general mathematics rather than metamathematics. If they were talking about (1), you'd expect them to at least do some actual metamathematics with it!
I think your next sentence actually serves to support this further.
>And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.'
And now consider how the sentence actually ends "- and convenient machine implementations, which can serve as a practical aid to the working mathematician". You could argue that it being a practical aid only refers to the convenient machine implementations, but how would 'homootopical content' or 'an "invariant" conception' remotely help with (1)? To me this makes it pretty clear that the aim is to have a practical 'foundation' for the average working mathematician i.e. (2).
>So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants.
Sure, that I don't disagree with, it's definitely in the area of 'applied metamathematics' and there's a reason type theory field is more on the CS side. I just think that you would generally get some pretty strange looks if you called e.g. research on sequent calculus an 'engineering problem', even though it's typically done with the intent of eventually getting a practical system.
>I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy
My point is that often there has been no 'visible' (for a non-mathematician) progress made, so it's curious to me that despite this it still gets posted here every few months. I would have expected some attention if some larger milestone was reached (e.g. formalizing most of an undergrad degree), it's the consistency that is surprising to me.