14
$\begingroup$

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?

$\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$ 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 Rute
    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 Rute
    Jun 15, 2022 at 2:47

4 Answers 4

14
$\begingroup$

How about Isabelle's FOL (PDF version) and ZF? It's a serious tool, people formalized forcing with it, for example.

$\endgroup$
1
10
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.