Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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.

share|improve this question
11  
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. –  Dave Clarke Feb 24 '11 at 9:33
5  
If you're interested in set theory, not type theory then Isabelle is probably the most straightforward system. Coq will seem strange and confusing. –  Mark Reitblatt Feb 24 '11 at 13:45
2  
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. –  Sadeq Dousti Feb 24 '11 at 14:05
7  
@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. –  Robin Kothari Feb 24 '11 at 21:32
7  
@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). –  Kaveh Feb 25 '11 at 4:57

6 Answers 6

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

share|improve this answer
1  
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. –  cody Nov 13 '12 at 17:41
1  
I should add that there is an implementation of these ideas though, by Bruno Barras: lix.polytechnique.fr/~barras/proofs/sets/index.html –  cody Nov 13 '12 at 17:42

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?

share|improve this answer
4  
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. –  Timothy Chow Feb 25 '11 at 16:22

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

share|improve this answer
2  
What is the tool support for Mizar like? –  Dave Clarke Feb 24 '11 at 14:21
    
I did not use it. –  Radu GRIGore Feb 25 '11 at 10:51

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.

share|improve this answer

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.

share|improve this answer

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

share|improve this answer
1  
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? –  Charles Stewart Nov 18 '12 at 18:45
1  
Here is the proof: dcproof.com/EmptySetUnique.htm There is a video at my website showing how the system works. –  Dan Christensen Dec 10 '12 at 15:39

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.