4 ms·

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%20wan

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.
- spekcular 5y ago
  I have no objections to claiming success in formalizing mathematics! As I've said, Lean is a big win for type theory. But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.). You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations. And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.
  - deleted 5y ago
    [deleted]
  - zozbot234 5y ago
    Large cardinals are closely related to what type theorists call "universes". Again, there's a huge amount of equiconsistency and relative consistency results linking type- and set theories. To keep suggesting and implying that type theory cannot possibly be a language for talking about these things is so incredibly careless and obtuse that some people might call it actively misleading.
    - spekcular 5y ago
      I'm not sure how that comment is responsive to my post. Sure, type theorists talk about universes, and sure, there are relative consistency results linking type and set theories. My claim is just that large cardinals (or some equivalent concept) are essentially necessary to order theories in consistency strength, so is hard to take a response of the form "it doesn't matter whether HoTT can talk about large cardinals" seriously.

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.

spekcular 5y ago
I have no objections to claiming success in formalizing mathematics! As I've said, Lean is a big win for type theory. But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.). You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations. And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.
- deleted 5y ago
  [deleted]
- zozbot234 5y ago
  Large cardinals are closely related to what type theorists call "universes". Again, there's a huge amount of equiconsistency and relative consistency results linking type- and set theories. To keep suggesting and implying that type theory cannot possibly be a language for talking about these things is so incredibly careless and obtuse that some people might call it actively misleading.
  - spekcular 5y ago
    I'm not sure how that comment is responsive to my post. Sure, type theorists talk about universes, and sure, there are relative consistency results linking type and set theories. My claim is just that large cardinals (or some equivalent concept) are essentially necessary to order theories in consistency strength, so is hard to take a response of the form "it doesn't matter whether HoTT can talk about large cardinals" seriously.