3 ms·

1. ZFC does everything you need it to do. It's a really hard set of axioms for me to justify compared to MLTT, and it's important to me how "obvious" some set o

by creata 6y ago

1. ZFC does everything you need it to do. It's a really hard set of axioms for me to justify compared to MLTT, and it's important to me how "obvious" some set of axioms is. MLTT also has the advantage that it's very easy to use without encoding everything into well-founded, untyped trees, which is nice. 2. What are these "substantive problems"? I don't have any experience in foundations, so I'm genuinely curious. 3. Sure, intuitionistic mathematics has very little popularity, but a lot of that popularity is among computer scientists, for fairly obvious reasons. 4. The HoTT book and the nLab are two of the most out-in-the-open developments in math I've seen --- the HoTT book was even written in a public GitHub repo iirc. Naturally that has a lot of appeal for HN. If you have anything similar (blogs, wikis, etc.) for mainstream foundations, I'd love to read them. 5. Yeah, personally, I'm not really convinced that HoTT is a good idea, but I guess we'll just have to wait and see.

spekcular 6y ago
1. ZFC is fairly "obvious" when taught the right way. Unfortunately, most people do have not the privilege of a good set theory instructor. 2. Whether V equals Ultimate L, for example. There's "pop math" coverage available [1], as well as more technical introductions by Woodin if you Google for them. 3. I'm not sure what reasons you're referring to; can you enlighten me? I can guess, but the ones I'm guessing are not very good, and I'd rather not attribute weak arguments to you or them. 4. The Stacks Project, for one [2]. It covers most of the foundations of modern algebraic geometry, is of extremely high quality, and is regularly cited in research papers. [1]: https://www.quantamagazine.org/to-settle-infinity-question-a-new-law-of-mathematics-20131126/ https://www.quantamagazine.org/to-settle-infinity-question-a... [2]: https://stacks.math.columbia.edu/ https://stacks.math.columbia.edu/
- mkehrt 6y ago
  3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.

by creata 6y ago

spekcular 6y ago

1. ZFC is fairly "obvious" when taught the right way. Unfortunately, most people do have not the privilege of a good set theory instructor. 2. Whether V equals Ultimate L, for example. There's "pop math" coverage available [1], as well as more technical introductions by Woodin if you Google for them. 3. I'm not sure what reasons you're referring to; can you enlighten me? I can guess, but the ones I'm guessing are not very good, and I'd rather not attribute weak arguments to you or them. 4. The Stacks Project, for one [2]. It covers most of the foundations of modern algebraic geometry, is of extremely high quality, and is regularly cited in research papers. [1]: https://www.quantamagazine.org/to-settle-infinity-question-a-new-law-of-mathematics-20131126/ https://www.quantamagazine.org/to-settle-infinity-question-a... [2]: https://stacks.math.columbia.edu/ https://stacks.math.columbia.edu/

mkehrt 6y ago
3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.