Is reflexivity of equality an axiom or a theorem?

Question

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.

Answer 1

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.

Answer 2

I would just like to point out that the usual properties of equality relation, including reflexivity, follow from a single two-way proof rule by Lawvere (expressed in natural-deduction style):

$$\frac{\Theta \vdash \phi[x/y]}{\Theta, x=y \vdash \phi}$$

This should be read as a two-way rule (I don't know how to produce a double horizontal line), i.e., from the top we may infer the bottom and vice versa. The rule has the form of an adjunction between functors, or a Galois connection if you will (equality is left adjoint to contraction is what the rule says). I personally find this more illuminating that wondering whether equality is axiomatized or derived.

For example, reflexivity follows when we take $\phi$ to be the formula $x = y$ and we read the rule bottom-up: because $x = y \vdash x = y$ it is also the case that $\vdash x = x$.

Reference: Bart Jacobs, "Categorical logic and type theory", Lemma 4.1.7, page 229, available in Google books.

Answer 3

I think it is important to consider. The axiom of extensionality is provided as a means of defining equality between sets. Roughly stated we say "A set X is equal to set Y if and only if they both have exactly the same elements." A more precise statement, taking into account that we'd like to quantify over domains that we can define, is this:

1) $X=Y\leftrightarrow \ \forall x \in X\ (x\in Y) \ \wedge \ \forall y \in Y\ (y\in X).$

This is just defining an equality relation for sets, and reflexivity comes from the definition rather than having to be be put forth as an axiom. For example taking X=X,

$\forall x \in X\ (x\in X) \ \wedge \ \forall x \in X\ (x\in X),$

is pretty true.

We can say that reflexivity is a theorem here. It's one of the properties of an Equivalence Relation, which must obey reflexivity, symmetry, and transitivity. Our 'equals' relation on sets happily obeys these rules. I like to consider equality as a possible relation we can define about objects, with some properties that we want it to hold. If we were coming at things from the perspective of logic we might make these properties axioms and prove the existence of such relations as theorems. I'm not completely sure on this. But from the perspective of axiomatized set theory, the extensionality axiom implies the rest of the equality properties very concretely.

Answer 4

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.

Answer 5

For what it's worth (it's been a while), the treatments I have seen take the fundamental properties of equality (reflexivity, symmetry, and transitivity, plus axioms stating that you cannot tell the difference between equal objects) as axioms, though not really as axioms of logic. Rather, there are first order theories, and among them are first order theories with equality, meaning they have a binary relation “=” and associated axioms. Then one spends just a page or two working out the consequences of this, and later, set theory is just another example of a first order theory with equality.

I wonder, though: If you drop equality and the axiom of extensionality, treating equality just as an abbreviation as you suggest, how do you prove that, if every member of x is equal to a member of y and vise versa, then x=_y_?