3 ms·

What does it mean for "a thing to be the actual thing"? I don't think any formalization you can write down will "actually" be the number 7 (though I'm happy to

What does it mean for "a thing to be the actual thing"? I don't think any formalization you can write down will "actually" be the number 7 (though I'm happy to consider any attempt to do this with an open mind). > You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held. > There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically. I don't understand this comment. Studying set theory has said a lot about mathematical practice - for instance, about what we can and can't hope to prove in certain systems, or about what axioms are needed for what statements. That's important stuff! More generally, there's the question of what you hope to accomplish by supplying a foundation for mathematics. Any value claim about some foundational system is contingent on what goal you have. As I said above, if that goal is actually writing down computer-checkable formalized versions of complex proofs, then ZFC is perhaps not the foundation you want to use. But, historically speaking, that was not what people had in mind. There was a desire to reduce mathematical reasoning to a few philosophically basic concepts so that we could be confident in its coherence and consistency. And a desire for providing a framework for studying mathematical reasoning itself. I think it's really important to understand this historical context, otherwise you end up with misleading claims like "ZFC is a bad foundational system because it doesn't help me formalize my research papers." Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics (or even exist on equal footing, creating a plurality of foundational systems). If you take the goal of a foundational system to be practically formalizing proofs, we have no evidence HoTT is particularly suited for this, and (as far as I know) no serious movement by the HoTT community to actually realize this vision (relative to what the Lean community is doing). I'm not claiming the first mover in some space should always dominate, just that if the HoTT people want to arguing for their foundational system on the grounds that it assists in formalizing math, maybe they should actually demonstrate their superiority by formalizing some math. For a longer comment on this, see: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa.... So if we disregard formalization, the arguments in favor of HoTT that remain are philosophical ones. But, as I've explained elsewhere in this thread, I find them all misguided. They all basically seem like arguments about aesthetics but don't actually tell me why HoTT is better than ZFC for the philosophical goals mentioned above.

ogogmad 4y ago
OK listen, spekcular. You haven't responded to any of my comments about constructive logic. > But, historically speaking, that was not what people had in mind. You have opinions about what you'd like from foundations. They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc. > Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics Nobody's really saying that. That's your own combative fanatasy or confusion. You're not a logician; you don't know foundations; and you're ignorant of logic-in-CS, based on your inability to understand some of the terms used and the following remark you've made: > It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions. That word salad alone should make people stop listening to you. But this is HN, so *shrug*. You are right maybe about combinatorics, but in this sort of maths, you are useless and oddly narrow-minded.
- spekcular 4y ago
  With respect, I find your point of view "oddly narrow-minded," and not representative of what most mathematicians think about these issues. Taking these points in order: 1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice. 2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean). My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals. 3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others. Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic. 4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.

ogogmad 4y ago

OK listen, spekcular. You haven't responded to any of my comments about constructive logic. > But, historically speaking, that was not what people had in mind. You have opinions about what you'd like from foundations. They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc. > Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics Nobody's really saying that. That's your own combative fanatasy or confusion. You're not a logician; you don't know foundations; and you're ignorant of logic-in-CS, based on your inability to understand some of the terms used and the following remark you've made: > It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions. That word salad alone should make people stop listening to you. But this is HN, so *shrug*. You are right maybe about combinatorics, but in this sort of maths, you are useless and oddly narrow-minded.

spekcular 4y ago
With respect, I find your point of view "oddly narrow-minded," and not representative of what most mathematicians think about these issues. Taking these points in order: 1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice. 2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean). My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals. 3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others. Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic. 4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.