4 ms·

Formal proof is so much important, since currently maths is built on set theory, I wonder how the set theory axioms are written in some of the formal solvers.

robinzfc 2y ago
No need to wonder for long, just have a look. Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms https://us.metamath.org/mpeuni/mmset.html#axioms Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
gaogao 2y ago
You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.
- JonChesterfield 2y ago
  The C part of ZFC is a challenge for constructive theories
  - sylware 2y ago
    I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics. So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
    - JonChesterfield 2y ago
      The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC. I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.
luma 2y ago
Check out mathlib for LEAN, the pace of proofs being added here is breathtaking: https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4
staunton 2y ago
> currently maths is built on set theory most mathematicians will eventually agree with that when pressed. However, almost none of them know the axioms of ZFC by heart (because they don't need them). You can swap out ZFC for something else and nobody will care very much as long as "the same" (does a lot of work here) theorems, which they know and use it their work, remain true. This is what many theorem provers do. Many aren't based on set theory, for example, but instead on type theory. (You can still do set theory in a framework based on type theory, and vice versa, but the foundations are "different").
UltraSane 2y ago
Can't current math be be built equally well on set theory, type theory, or category theory? Coq, Agda, and Lean use Type Theory.
- sylware 2y ago
  As far as I can recall set theory axioms are really basic, dunno if the type theory axioms are really basic too.

robinzfc 2y ago

No need to wonder for long, just have a look. Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms https://us.metamath.org/mpeuni/mmset.html#axioms Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html

gaogao 2y ago

You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.

JonChesterfield 2y ago
The C part of ZFC is a challenge for constructive theories
- sylware 2y ago
  I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics. So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
  - JonChesterfield 2y ago
    The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC. I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.

luma 2y ago

Check out mathlib for LEAN, the pace of proofs being added here is breathtaking: https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4

staunton 2y ago

> currently maths is built on set theory most mathematicians will eventually agree with that when pressed. However, almost none of them know the axioms of ZFC by heart (because they don't need them). You can swap out ZFC for something else and nobody will care very much as long as "the same" (does a lot of work here) theorems, which they know and use it their work, remain true. This is what many theorem provers do. Many aren't based on set theory, for example, but instead on type theory. (You can still do set theory in a framework based on type theory, and vice versa, but the foundations are "different").

UltraSane 2y ago

Can't current math be be built equally well on set theory, type theory, or category theory? Coq, Agda, and Lean use Type Theory.

sylware 2y ago
As far as I can recall set theory axioms are really basic, dunno if the type theory axioms are really basic too.