Everybody knows that equality is reflexive: $\forall(x)(x=x)$. But should reflexivity of equality be taken as an axiom of logic or as a theorem of set theory?
If you choose the former then you probably need the axiom of extensionality: $\forall(x)\forall(y)(x=y\leftrightarrow\forall(z)(z\in x\leftrightarrow z\in y))$.
If you choose the latter then probably $x=y$ is just an abbreviation for $\forall(z)(z\in x\leftrightarrow z\in y)$.
What I'm trying to do is to write down proofs for basic facts about set theory, but I'm not so sure which logical axioms and rules of inference should I take for granted.
Thanks.
Best Answer
We all want reflexivity to be provable in any first order theory, not just set theory. So this question has nothing particularly to do with set theory or with extensionality. Surely we want x=x in all groups, all rings, all graphs, and so on in any mathematical context.
So the answer is that either we add it as an axiom, or we make sure to have other logical axioms that can prove it. What you seem to want or need are the explicit details of your formal proof system. You may choose among many logical systems out there (see the Wikipedia page on proof theory http://en.wikipedia.org/wiki/Proof_theory). In particular, the Hilbert calculus includes reflexivity explicitly as a logical axiom.
Ultimately, it is an irrelevant choice whether you have it as an axiom or as a theorem, unless you are proof theorist, who is studying the proofs themselves as mathematical objects, rather than using proof to understand its mathematical content, as you seem to be doing.