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.



Is reflexivity of equality an axiom or a theorem?
I managed to write down a proof for the reflexivity of equality using only the definition of equality in terms of membership and the rules of natural deduction.


1. Premise: $\forall x\_0\forall x\_1\left(\left(x\_0=x\_1\right)\leftrightarrow\forall x\_2\left(\left(x\_2\in x\_0\right)\leftrightarrow\left(x\_2\in x\_1\right)\right)\right)$
2. Assumption (1): $\forall x\_0\forall x\_1\left(\left(x\_0=x\_1\right)\leftrightarrow\forall x\_2\left(\left(x\_2\in x\_0\right)\leftrightarrow\left(x\_2\in x\_1\right)\right)\right)$
3. Universal elimination (2): $\forall x\_1\left(\left(k\_0=x\_1\right)\leftrightarrow\forall x\_2\left(\left(x\_2\in k\_0\right)\leftrightarrow\left(x\_2\in x\_1\right)\right)\right)$
4. Universal elimination (3): $\left(\left(k\_0=k\_0\right)\leftrightarrow\forall x\_2\left(\left(x\_2\in k\_0\right)\leftrightarrow\left(x\_2\in k\_0\right)\right)\right)$
5. (Subproof 1) Premise: $\left(k\_2\in k\_0\right)$
6. (Subproof 1) Assumption (5): $\left(k\_2\in k\_0\right)$
7. (Subproof 2) Premise: $\left(k\_2\in k\_0\right)$
8. (Subproof 2) Assumption (7): $\left(k\_2\in k\_0\right)$
9. Biconditional introduction (5, 6, 7, 8): $\left(\left(k\_2\in k\_0\right)\leftrightarrow\left(k\_2\in k\_0\right)\right)$
10. Universal introduction (9): $\forall x\_2\left(\left(x\_2\in k\_0\right)\leftrightarrow\left(x\_2\in k\_0\right)\right)$
11. Biconditional elimination (4, 10): $\left(k\_0=k\_0\right)$
12. Universal introduction (11): $\forall x\left(x=x\right)$


In a similar way I also wrote down the proof for the symmetry and for the transitivity of equality.


