I have been trying to find open source proof assistants for first order logic with equality and set theory. To date, the closest that I have found is Metamath (http://us.metamath.org/index.html) and Mizar (http://mizar.org/). Mizar does not appear to be open source. Are there any others?
$\begingroup$
$\endgroup$
3
-
6$\begingroup$ It's worth noting Isabelle is a generic framework you can extend to set theory or other theories cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf . Might be a little helpful. $\endgroup$– Ms. Molly Stewart-GallusCommented Jun 15, 2022 at 2:15
-
1$\begingroup$ Mizar and Metamath are the two I’m aware of. I think the Mizar folks like to state that Mizar came before open source software and they developed their own procedures. So while it isn’t technically open source, it is freely available to use and you can see the source code if you write a Mizar article. $\endgroup$– Jason RuteCommented Jun 15, 2022 at 2:43
-
1$\begingroup$ Oh, also there is Mario Carneiro’s Metamath Zero which is different from Metamath but can compile the Metamath set.mm library. It’s more of a research project however. $\endgroup$– Jason RuteCommented Jun 15, 2022 at 2:47
Add a comment
|
4 Answers
$\begingroup$
$\endgroup$
1
How about Isabelle's FOL (PDF version) and ZF? It's a serious tool, people formalized forcing with it, for example.
-
3$\begingroup$ Not just that – even the independence of the Continuum Hypothesis! isa-afp.org/entries/Independence_CH.html $\endgroup$ Commented Jun 15, 2022 at 9:38
$\begingroup$
$\endgroup$
We have been working on a deep embedding of first-order logic in Coq for quite a while now, which could be relevant depending on what you plan to do. For instance, in a project on undecidability and incompleteness we consider various axiomatisations of ZF set theory and its finitary fragments.
So at least if you want to do some meta-theory of set theory, this setting could be helpful. However, if you want to do proofs inside of set theory, working with such a deep embedding is probably less convenient than Metamath, Mizar, or Isabelle/ZF.
$\begingroup$
$\endgroup$
Mizar is now open source, and the code is available at https://github.com/MizarProject/system under a GPLv3 license. Further, there is also an ongoing project to reimplement Mizar in Rust.
answered Feb 27, 2023 at 23:59
$\begingroup$
$\endgroup$
You may want to look at LISA https://github.com/epfl-lara/lisa
It is a new proof assistant based on First Order Logic with schematic symbols, equality and set theory. Its kernel is based on a proof checker for Sequent Calculus, and a LCF-style system for development of theorems and definitions.
It is a new proof assistant, fully open source, still under development, in Scala. The kernel is fully functional, but there is for now little automation.
