# Proof assistant for writing mathematics

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.

-
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
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
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
@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
@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

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

-
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
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.

Are you up for the challenge?

-
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/

-
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.

-

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.

-