MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

## Is reflexivity of equality an axiom or a theorem?

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.

-

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.

-

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.

-
 I find these proof-theoretic considerations to cast the most light: the stremgth of proof theory is showing how elementary the concepts we are looking at really are. – Charles Stewart Jan 30 2010 at 9:55 Of course, I very much doubt that in this particular case Lawvere was going after proof-theoretic analysis of equality. He was expressing the proof rules for equality in a category-theoretic way. This can be done with all logical connectives and the quantifiers: each receives exactly one two-way proof rule which is an adjunction. – Andrej Bauer Jan 31 2010 at 10:02

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.

-
There's one property that cannot be proved from this definition: $2) x = y \wedge x \in z \rightarrow y \in z$ If we take $x=y$ to be an abbreviation for 1), then we must add 2) as an axiom. – robin-adams Jul 21 2010 at 8:00

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?

-
 Let alone proving that if x = y, then x belongs to z if and only if y belongs to z (which I always regarded as the true meaning of the axiom of extensionality). – Andrea Ferretti Jan 29 2010 at 14:40 @Andrea: I am not sure why you consider that statement being the true (or any) meaning of extensionality. To me, it's an equality axiom: The one that says you can't tell the difference between equal objects. Apart from that, I agree with your comment. – Harald Hanche-Olsen Jan 29 2010 at 16:24

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.

-