6 ms·

Frankly we are sick of set theorist traditionalists complaining about type theory, category theory, and other new things without actually bothering to understan

Frankly we are sick of set theorist traditionalists complaining about type theory, category theory, and other new things without actually bothering to understand them at all. After multiple decades, it's clear you all are never going to bother to learn our stuff nearly as well as we bothered to learn your stuff. This "debate" is thus completely unproductive without any good agreed-upon foundation to argue form. (How ironic!)

spekcular 5y ago
First, I'm not a set theorist. Second, one of the major motivations for introducing type theory in mathematics was to assist with computer-aided formalization efforts, which has had some success and has a promising future (e.g. the stuff the Lean community has been doing lately). This is great! I'm not complaining at all. But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century. Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-299 https://mathematicswithoutapologies.wordpress.com/2015/05/13... (And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")
- Ericson2314 5y ago
  > evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics This is still gatekeeping who gets to use the word "foundations". I will go read https://mathematicswithoutapologies.wordpress.com/2015/05/13 https://mathematicswithoutapologies.wordpress.com/2015/05/13 but my hopes are not high for a sudden breakthrough.
  - spekcular 5y ago
    I'm sorry, but this is not gatekeeping; that term has an established meaning and mathematical history, and corresponds to a productive vein of research going back to Gödel (at least). If you'd like to argue that the study of foundations should be expanded to include the things that HoTT people are interested in, that's one thing. But can we at least agree it does not have a ton of relevance to the questions people have traditionally considered in foundational work? (This is almost by definition if we set it up so that it is mutually interpretable with ZFC.)
    - throwaway81523 5y ago
      > going back to Gödel (at least) See, that is the basic misunderstanding here. Foundations now is a wider topic area than it was in Gödel's day. It's like saying that automobiles run on internal combustion engines in a productive vein of manufacturing going back to Henry Ford (at least). Since those days though, there is this guy Elon who you might like to meet...
      - spekcular 5y ago
        I absolutely agree that it's a wider, more sophisticated topic today. This doesn't mean that its main concerns have fundamentally changed. The Maddy article linked in a comment above is extremely clear explanation of this.
        throwaway81523 5y ago
        I don't see the Maddy link, but anyway try for something written in the current century.
        spekcular 5y ago
        Here, from three years ago: http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want%20-%20final http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want...
- Twisol 5y ago
  I think Mike Shulman's side of the discussion in that thread is also very worth reading, and it's somewhat unfair to (perhaps unintentionally) characterize Lurie as the representative of mathematicians trying to talk sense into the homotopy type theorists. They have a very balanced discussion where each respectfully tries to understand where the other is coming from. I'm desperately trying to find a lovely philosophical writeup on the different purposes to which a "foundation" is put, and why different foundationalists want those foundations for distinct purposes. I can't seem to hunt it down (Google has become steadily less helpful over time). But the thrust is, I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, as Lurie exhibits throughout, maybe it's worth it to keep using the entirely viable tools you have!
  - spekcular 5y ago
    You write: "I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, maybe it's worth it to keep using the entirely viable tools you have!" My claim is that "capturing [...] some pervasive intuitions" is not what ZFC is trying to do, or what people in foundations are interested in. Lurie puts the point well when he says a foundation "mean[s] a small number of concepts and assumptions from which the rest of mathematics can be derived." The purposes here are first, to figure out what exactly one must assume to get the rest of mainstream mathematics, and second, to provide a convenient base for doing metamathematics (since the fewer elementary operations/objects you have to reason with, the easier it is to write proofs). Capturing intuitions is completely orthogonal to this endeavor; no one is claiming that set-theoretic translations of everyday mathematical arguments capture the intuitive content of those arguments, because no one one intended ZFC to ever do that in the first place. Similarly, no one is claiming that handing someone a Turing machine that performs quicksort is a great way to capture the intuition behind quicksort, or explain the algorithm in an understandable way. Turing machines exist as a special-purpose construct to probe the limits of computation, not to reproduce or communicate high-level algoritmhic reasoning. ZFC is like a Turing machine for (meta)math.

spekcular 5y ago

First, I'm not a set theorist. Second, one of the major motivations for introducing type theory in mathematics was to assist with computer-aided formalization efforts, which has had some success and has a promising future (e.g. the stuff the Lean community has been doing lately). This is great! I'm not complaining at all. But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century. Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-299 https://mathematicswithoutapologies.wordpress.com/2015/05/13... (And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")

Ericson2314 5y ago
> evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics This is still gatekeeping who gets to use the word "foundations". I will go read https://mathematicswithoutapologies.wordpress.com/2015/05/13 https://mathematicswithoutapologies.wordpress.com/2015/05/13 but my hopes are not high for a sudden breakthrough.
- spekcular 5y ago
  I'm sorry, but this is not gatekeeping; that term has an established meaning and mathematical history, and corresponds to a productive vein of research going back to Gödel (at least). If you'd like to argue that the study of foundations should be expanded to include the things that HoTT people are interested in, that's one thing. But can we at least agree it does not have a ton of relevance to the questions people have traditionally considered in foundational work? (This is almost by definition if we set it up so that it is mutually interpretable with ZFC.)
  - throwaway81523 5y ago
    > going back to Gödel (at least) See, that is the basic misunderstanding here. Foundations now is a wider topic area than it was in Gödel's day. It's like saying that automobiles run on internal combustion engines in a productive vein of manufacturing going back to Henry Ford (at least). Since those days though, there is this guy Elon who you might like to meet...
    - spekcular 5y ago
      I absolutely agree that it's a wider, more sophisticated topic today. This doesn't mean that its main concerns have fundamentally changed. The Maddy article linked in a comment above is extremely clear explanation of this.
      - throwaway81523 5y ago
        I don't see the Maddy link, but anyway try for something written in the current century.
        spekcular 5y ago
        Here, from three years ago: http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want%20-%20final http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want...
Twisol 5y ago
I think Mike Shulman's side of the discussion in that thread is also very worth reading, and it's somewhat unfair to (perhaps unintentionally) characterize Lurie as the representative of mathematicians trying to talk sense into the homotopy type theorists. They have a very balanced discussion where each respectfully tries to understand where the other is coming from. I'm desperately trying to find a lovely philosophical writeup on the different purposes to which a "foundation" is put, and why different foundationalists want those foundations for distinct purposes. I can't seem to hunt it down (Google has become steadily less helpful over time). But the thrust is, I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, as Lurie exhibits throughout, maybe it's worth it to keep using the entirely viable tools you have!
- spekcular 5y ago
  You write: "I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, maybe it's worth it to keep using the entirely viable tools you have!" My claim is that "capturing [...] some pervasive intuitions" is not what ZFC is trying to do, or what people in foundations are interested in. Lurie puts the point well when he says a foundation "mean[s] a small number of concepts and assumptions from which the rest of mathematics can be derived." The purposes here are first, to figure out what exactly one must assume to get the rest of mainstream mathematics, and second, to provide a convenient base for doing metamathematics (since the fewer elementary operations/objects you have to reason with, the easier it is to write proofs). Capturing intuitions is completely orthogonal to this endeavor; no one is claiming that set-theoretic translations of everyday mathematical arguments capture the intuitive content of those arguments, because no one one intended ZFC to ever do that in the first place. Similarly, no one is claiming that handing someone a Turing machine that performs quicksort is a great way to capture the intuition behind quicksort, or explain the algorithm in an understandable way. Turing machines exist as a special-purpose construct to probe the limits of computation, not to reproduce or communicate high-level algoritmhic reasoning. ZFC is like a Turing machine for (meta)math.