3 ms·

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 ba

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...
      - throwaway81523 5y ago
        Thanks, that looks interesting and I'll try to read it. But it appears to mostly be about philosophy, and it doesn't say much about what (mathematical) logicians are doing today.
      - Ericson2314 5y ago
        I did start to read it last night, and finished today. My understanding is that regular MLTT already can do all the bold things Set theory does, and HFTT (and other developments) aims to make "Proof Checker" better realized (no more "setoid hell"). Ultimately what us CS people care about is a unity of theory and practice. What drew us to computers int the first place was trying to make explicit and tangible ideas that previously were only laboriously communicated from one generation of big brains to the next in the ivory tower. In that regards, I would say don't even look HoTT or fancy theory developments. Look at Lean, written by a non-type-theorist, and mathlib, written by a non-constructivist. Lean and Mathilb are plainly plowing a head in ways that no set theory based tool has ever achieved, and covering all the set theory bold points in the process. Perhaps a new more elegant type theory will replace Lean soon, but honestly I am not even worried about that. The important thing is making math much more accessible without loss of rigor with these tools. If better theories can follow rather than lead that methological revolution, that's fine with me, As to Category Theory and essential guidance, I have a simple test :). As mathlib (or its sucesssors) matures, let us see how many proofs are refactored to use category theory! I don't want to poo-poo the deeper connections between type theory and cateogory theory, but merely using lots of category theory "library code" in a type theoretic proof assistant not itself designed with explicit reference to category theory is good enough a success story for me. In conclusion: - Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care) - Regular type theory: *check* - HoTT: *check* - Set theory: *check*, bonus points for more exotic large cardinals - Generous Arena, Shared Standard, Meta- mathematical Corral - Regular type theory: *check* - Set theory: *check* - HoTT: WIP because culture shock of weird equality - Proof Checker: - Set theory: *FAIL* - Regular type theory: *partial support*, full if we discard all constructive side goals (Lean) - HoTT: *check*! (Very recent cubical results - Essential guidance: - Category theory does best, but can use as "library" rather than "language". good enough for now.
Ericson2314 5y ago
Foundations goes back to Cantor and Frege, at least. Set theorists have made a Whig History of sorts where everything leads to ZFC, but that is just their post-hoc reading of the intellectual history. We can write Whig Histories too. See https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf for example. The fact is both narratives are wrong --- intellectual history is always more pluralistic and meandering than partisans want to admit in hindsight. We, as the underdogs, are ready to admit that. Can you all do the same?
- spekcular 5y ago
  That link talks almost entirely about implications for programming and not mathematics. I recommend the Penelope Maddy article linked in a comment above for a more in-depth discussion of the relevant history and aims of the field. She says things much more clearly than I can.
  - Ericson2314 5y ago
    Yes, my point is "functional programming" and "ZFC" are both not predestined as the inevitable conclusion the ideas preceding them would lead up to.

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...
    - throwaway81523 5y ago
      Thanks, that looks interesting and I'll try to read it. But it appears to mostly be about philosophy, and it doesn't say much about what (mathematical) logicians are doing today.
    - Ericson2314 5y ago
      I did start to read it last night, and finished today. My understanding is that regular MLTT already can do all the bold things Set theory does, and HFTT (and other developments) aims to make "Proof Checker" better realized (no more "setoid hell"). Ultimately what us CS people care about is a unity of theory and practice. What drew us to computers int the first place was trying to make explicit and tangible ideas that previously were only laboriously communicated from one generation of big brains to the next in the ivory tower. In that regards, I would say don't even look HoTT or fancy theory developments. Look at Lean, written by a non-type-theorist, and mathlib, written by a non-constructivist. Lean and Mathilb are plainly plowing a head in ways that no set theory based tool has ever achieved, and covering all the set theory bold points in the process. Perhaps a new more elegant type theory will replace Lean soon, but honestly I am not even worried about that. The important thing is making math much more accessible without loss of rigor with these tools. If better theories can follow rather than lead that methological revolution, that's fine with me, As to Category Theory and essential guidance, I have a simple test :). As mathlib (or its sucesssors) matures, let us see how many proofs are refactored to use category theory! I don't want to poo-poo the deeper connections between type theory and cateogory theory, but merely using lots of category theory "library code" in a type theoretic proof assistant not itself designed with explicit reference to category theory is good enough a success story for me. In conclusion: - Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care) - Regular type theory: *check* - HoTT: *check* - Set theory: *check*, bonus points for more exotic large cardinals - Generous Arena, Shared Standard, Meta- mathematical Corral - Regular type theory: *check* - Set theory: *check* - HoTT: WIP because culture shock of weird equality - Proof Checker: - Set theory: *FAIL* - Regular type theory: *partial support*, full if we discard all constructive side goals (Lean) - HoTT: *check*! (Very recent cubical results - Essential guidance: - Category theory does best, but can use as "library" rather than "language". good enough for now.

Ericson2314 5y ago

Foundations goes back to Cantor and Frege, at least. Set theorists have made a Whig History of sorts where everything leads to ZFC, but that is just their post-hoc reading of the intellectual history. We can write Whig Histories too. See https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf for example. The fact is both narratives are wrong --- intellectual history is always more pluralistic and meandering than partisans want to admit in hindsight. We, as the underdogs, are ready to admit that. Can you all do the same?

spekcular 5y ago
That link talks almost entirely about implications for programming and not mathematics. I recommend the Penelope Maddy article linked in a comment above for a more in-depth discussion of the relevant history and aims of the field. She says things much more clearly than I can.
- Ericson2314 5y ago
  Yes, my point is "functional programming" and "ZFC" are both not predestined as the inevitable conclusion the ideas preceding them would lead up to.