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?
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.
Lukas Stevens said:
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.
Thank you!
One prominent example is sledgehammer, which only exists in Isabelle/HOL IRC.
Last updated: Dec 21 2024 at 16:20 UTC