Patrick Nicodemus (Apr 26 2023 at 17:59): Patrick Nicodemus (Apr 26 2023 at 17:59):Lawrence Paulson has axiomatized a ZFC universe type in HOL. There has been a category theory development on top of this. If I want to do category theory in ZFC using this development i am curious what HOL buys you. Both in practical and theoretical terms, in expressiveness and convenience, what would be the difference between doing math in ZFC in FOL vs doing math in HOL where all the mathematical objects are terms of V? what are some ways that isabelle's rich type system could improve your quality of life here?
Lukas Stevens (Apr 27 2023 at 13:25):You can read about the motivation for ZFC_in_HOL here. In short, Isabelle/ZF doesn't even have real numbers. Results about those could be re-used from the outer logic, Isabelle/HOL. In general, Isabelle/HOL is the most mature logic in terms of automation and tooling.
Patrick Nicodemus (Apr 27 2023 at 13:29):Lukas Stevens said:
You can read about the motivation for
ZFC_in_HOLhere. In short, Isabelle/ZF doesn't even have real numbers. Results about those could be re-used from the outer logic, Isabelle/HOL. In general, Isabelle/HOL is the most mature logic in terms of automation and tooling.
Thank you!
Lukas Stevens (Apr 27 2023 at 13:30):One prominent example is sledgehammer, which only exists in Isabelle/HOL IRC.
Last updated: Apr 27 2024 at 16:16 UTC