I'm looking for a proof assistant in order to write formal proofs about basic facts of set theory, such as:
- $a\subseteq a$
- $(a,b)=(c,d)\leftrightarrow a=c\land b=d$
Natural deduction for first-order logic is the only set of rules of inference I'd like to use. Easy to install and easy to use software is preferred over more complicated one. Also, open-source software is preferred over closed-source one. No matter if the software comes with an archive of proofs that have been already formalized: I'd like to start from scratch.
Thanks.
Best Answer
Isabelle supports many different logics, and it has a formulation of first order logic which you may browse here: http://isabelle.in.tum.de/dist/library/FOL/index.html. However, even though proofs are natural deduction in flavor, it does not produce anything a logician would understand as a natural deduction derivation upon shallow inspection.
The automated theorem provers Prover9, E, SPASS and Vampire are all first order systems. They do not produce proofs using natural deduction (they are all typically resolution/paramodulation based systems).
It sounds like ProofWeb is exactly like what you want. It provides a system for displaying the accompanying natural deduction/sequent calculus proof along with a computer assisted formalization. It also has a really nice interactive interface for students, and provides the possibility of assigning exercises. On the other hand, I know that it has been largely developed for Coq, which is way, way more expressive than first order logic. And even though I know that there is a development of set theory within Coq, I suspect modifying the system for basic set theory would be a nontrivial exercise.