Timeline for Book that shows a construction of ZFC with Calculus of Constructions
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 7, 2023 at 13:52 | comment | added | Timothy Chow | @rfloc Isabelle may be a better choice if you want to formalize things set-theoretically. There's Isabelle/ZF as well as auto2. | |
| Apr 6, 2023 at 13:48 | comment | added | Peter LeFanu Lumsdaine | [cont’d] It will teach you a lot about assembly language interpreters, but it’s not an efficient way to implement programs. Type theory is a higher-level language than set theory in the first place, designed to be closer to mathematical practice — if your main goal is understanding how to formalise mathematical structures, order theory, real analysis, etc, in type theory/proof assistants, then I wouldn’t recommend going via ZFC (and I think few people in the field would). | |
| Apr 6, 2023 at 13:48 | comment | added | Peter LeFanu Lumsdaine | @rfloc: I haven’t seen those books before so this is only based on a quick look, but: On the one hand, in principle, yes I think you could formalise that material inside the HoTT book’s implementation of ZFC. But (depending on your motivations) that seems a rather unnatural thing to do — formalising mathematical topics within ZFC, inside the interpretation of ZFC into type theory. To use a programming analogy, that’s like writing your programs in assembly language, and then writing an assembly language interpreter in C. [cont’d] | |
| Apr 6, 2023 at 13:34 | comment | added | rfloc | With the theory presented in the HoTT book, will I be able to formalize, for example, what are in the books "Classical Set Theory" (by Taras Banakh) and "The Structure of the Real Line" (by Lev Bukovský)? Now I want to learn a Dependent Type Theory similar to those behind theorem prover like Lean and Coq because later I want to rewrite everything using a specific theorem prover (now I just want to prove everything without using any proof assistant). | |
| Apr 6, 2023 at 10:51 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |