4 ms·

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 Luri

by 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.
- Twisol 5y ago
  Yes, hence my desperate desire to relocate the article on what purposes a foundation may be put to. I say this as neutrally as possible, but I don't think "foundation" has such a singular meaning, and misattributing one "foundation's" goals to be those of another's is probably near the root of your frustration. (It would help my case to find the article; at present I can only relay the ghost of what I took from it.) HoTT/UF share some purposes of a foundation with ZFC, and not others. Each has purposes the other does not. That's about the safest thing I can say with any faith that I'm doing it justice.
  - spekcular 5y ago
    I understand this desire but I think people who believe this should develop a new word or description for what you're attempting to do. See my comment here: https://news.ycombinator.com/item?id=30817964 https://news.ycombinator.com/item?id=30817964 I want to emphasize I'm not policing semantics just for the sake of being ornery. My reaction is approximately the same as it would be to someone who sends me a graph theory paper and calls it number theory. These distinctions are useful.
    - Twisol 5y ago
      Yes, I don't especially disagree; I also think words are most useful when they mean something consistent and precise. Nonetheless, I think it's worth separating the merely terminological disagreement from the deeper semantic disagreement. Please do see the article I found(!) in a cousin comment, by Penelope Maddy. I think it provides a very enlightening perspective on the ways in which ZFC and HoTT/UF both purport to be "foundations" and yet seek to perform different duties.
      - spekcular 5y ago
        Thanks. I enjoyed the article you linked. I think the description on page 16 is a good summary of what most people working in foundations take the purpose of foundations to be.
    - 5y ago
zozbot234 5y ago
There's a well-known line of research into the equiconsistency of set-theoretical and type-theoretical foundations, with many compelling results. So you actually can do "reverse mathematics" of type-theoretical foundations. You aren't losing anything.

by Twisol 5y ago

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.

Twisol 5y ago
Yes, hence my desperate desire to relocate the article on what purposes a foundation may be put to. I say this as neutrally as possible, but I don't think "foundation" has such a singular meaning, and misattributing one "foundation's" goals to be those of another's is probably near the root of your frustration. (It would help my case to find the article; at present I can only relay the ghost of what I took from it.) HoTT/UF share some purposes of a foundation with ZFC, and not others. Each has purposes the other does not. That's about the safest thing I can say with any faith that I'm doing it justice.
- spekcular 5y ago
  I understand this desire but I think people who believe this should develop a new word or description for what you're attempting to do. See my comment here: https://news.ycombinator.com/item?id=30817964 https://news.ycombinator.com/item?id=30817964 I want to emphasize I'm not policing semantics just for the sake of being ornery. My reaction is approximately the same as it would be to someone who sends me a graph theory paper and calls it number theory. These distinctions are useful.
  - Twisol 5y ago
    Yes, I don't especially disagree; I also think words are most useful when they mean something consistent and precise. Nonetheless, I think it's worth separating the merely terminological disagreement from the deeper semantic disagreement. Please do see the article I found(!) in a cousin comment, by Penelope Maddy. I think it provides a very enlightening perspective on the ways in which ZFC and HoTT/UF both purport to be "foundations" and yet seek to perform different duties.
    - spekcular 5y ago
      Thanks. I enjoyed the article you linked. I think the description on page 16 is a good summary of what most people working in foundations take the purpose of foundations to be.
  - 5y ago

zozbot234 5y ago

There's a well-known line of research into the equiconsistency of set-theoretical and type-theoretical foundations, with many compelling results. So you actually can do "reverse mathematics" of type-theoretical foundations. You aren't losing anything.