12
$\begingroup$

I'd like to write mathematical proofs using some proof assistant. Everything will be written using first order logic (with equality) and natural deduction. The background is set theory (ZF). For example, how could I write the following proof?

Axiom: $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$

Theorem: $\forall x\forall y(\forall z(z\notin x)\land\forall z(z\notin y)\rightarrow x=y)$

That is, the empty set is unique.

It's trivial for me to accomplish that using paper and a pen, but what I really need is a software to help me checking proof for correctness.

Thank you.

Improve this question
$\endgroup$
13
  • 11
    $\begingroup$ First you need to select a proof assistant. Coq is what I use, but there are many others. Some of these are based on first order logic, so will be more suited to your needs. Then you need to commit to learning the proof assistant. Within a few days you ought to be able to encode simple theorems, such as the one above, and prove them. Don't expect that we will do this for you. You'll learn nothing that way. $\endgroup$
    – Dave Clarke
    Commented Feb 24, 2011 at 9:33
  • 5
    $\begingroup$ If you're interested in set theory, not type theory then Isabelle is probably the most straightforward system. Coq will seem strange and confusing. $\endgroup$
    – Mark Reitblatt
    Commented Feb 24, 2011 at 13:45
  • 2
    $\begingroup$ I think the axiom you wrote is not first-order logic, but second-order logic. This is because in the former, variables only range over individuals, while in the latter, variables can range over both individuals and sets. Apparently, in the given axiom, $x$ and $y$ are sets while $z$ is an individual. $\endgroup$
    – Sadeq Dousti
    Commented Feb 24, 2011 at 14:05
  • 10
    $\begingroup$ @Sadeq: In ZF aren't sets the basic elements of the universe anyway? So you should be able to say things like "for all sets" in first order logic, which is what's being done in that axiom. $\endgroup$
    – Robin Kothari
    Commented Feb 24, 2011 at 21:32
  • 10
    $\begingroup$ @Sadeq, what Robin said is correct, $\mathbf{ZF}$ is a first order theory and the axiom written in the question is also first order. In $\mathbf{ZF}$ everything is just a set, there is nothing as individuals vs sets. (As a side note, one does not need to move to second or higher order objects to talk about different kinds of variables, one only needs different sorts, second and higher order logic are quite different from many-sorted logics). $\endgroup$
    – Kaveh
    Commented Feb 25, 2011 at 4:57

6 Answers 6

Reset to default
13
$\begingroup$

Both Coq and Isabelle can do this.

[Coq] Here is a paper discussing how to encode ZFC in CIC, on which Coq is based.

Benjamin Werner: Sets in Types, Types in Sets (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle] There is a library for ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

Improve this answer
$\endgroup$
2
  • 4
    $\begingroup$ While this paper is quite nice, I think that it would be more pragmatic to just add species (type variables) and axioms to directly encode the axiomatic theory of ZF, then do the proofs by direct appeal to these axioms. The encoding is more to show that the theories are related in expressive strength. $\endgroup$
    – cody
    Commented Nov 13, 2012 at 17:41
  • 2
    $\begingroup$ I should add that there is an implementation of these ideas though, by Bruno Barras: lix.polytechnique.fr/~barras/proofs/sets/index.html $\endgroup$
    – cody
    Commented Nov 13, 2012 at 17:42
8
$\begingroup$

There are many mathematics articles written using the proof assistant Mizar: http://mizar.org/fm/

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ What is the tool support for Mizar like? $\endgroup$
    – Dave Clarke
    Commented Feb 24, 2011 at 14:21
  • $\begingroup$ I did not use it. $\endgroup$
    – Radu GRIGore
    Commented Feb 25, 2011 at 10:51
8
$\begingroup$

Moved from comment at Kaveh's suggestion

First you need to select a proof assistant. Coq is what I use, but there are many others. Coq is based on higher-order logic (the so-called Calculus of Inductive Constructions). Other proof assistants are based on first order logic, so may be more suited to your needs (modulo the comments above).

Then you need to commit to learning the proof assistant. The linked document is a tutorial for getting of the ground with Coq. Becoming a Coq expert requires years of dedication and practice, but simple theorems can be proven in an afternoon. The key to learning Coq or any other proof assistant is to do proofs, such as the ones in the linked paper. Just reading the paper will help very little, because the whole experience of interacting with the proof assistant cannot be conveyed well on paper.

Within a few days you ought to be able to encode simple theorems, such as the one above, and prove them. Don't expect that we will do this for you. You'll learn nothing that way.

When you do succeed in proving these theorems, feel free to post your answers here and maybe leave a few comments about your experiences.

Are you up for the challenge?

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ Coq is a reasonable choice; however, if xddz5 really wants to work in ZF set theory rather than type theory, then perhaps Mizar is more suitable. $\endgroup$
    – Timothy Chow
    Commented Feb 25, 2011 at 16:22
6
$\begingroup$

Dave Clarke suggests Coq, but really Isabelle seems like a much better idea, seeing as it has A library for ZF. Isabelle is also very mature and includes a wide variety of tactics and extensions.

I haven't personally used Mizar, but it may well be good as well.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Link broken, my man $\endgroup$
    – Daniel Donnelly
    Commented May 17, 2023 at 22:23
2
$\begingroup$

how could I write the following proof?

In Isabelle/ZF you can write something like this 

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

As you can see Isabelle proves this automatically. Of course you can write a more detailed proof if you really want.

Improve this answer
$\endgroup$
2
$\begingroup$

This very theorem is a worked example (see Example 11) in the tutorial included with my DC Proof 2.0 software. Download it free of charge at my website http://www.dcproof.com

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ This is a little sell-ish for this site. Could you present some information in an even-handed way to say in what way your software is well-suited to the problem? Perhaps a link to a video or a screenshot of this derivation being carried out? $\endgroup$
    – Charles Stewart
    Commented Nov 18, 2012 at 18:45
  • 1
    $\begingroup$ Here is the proof: dcproof.com/EmptySetUnique.htm There is a video at my website showing how the system works. $\endgroup$
    – Dan Christensen
    Commented Dec 10, 2012 at 15:39

Your Answer

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