### Concepts of Sameness (Part 3)

#### Posted by John Baez

Now I’d like to switch to pondering different approaches to equality. (Eventually I’ll have put all these pieces together into a coherent essay, but not yet.)

We tend to think of $x = x$ as a fundamental property of equality, perhaps the most fundamental of all. But what is it actually *used* for? I don’t really know. I sometimes joke that equations of the form $x = x$ are the only really *true* ones — since any other equation says that *different* things are equal — but they’re also completely *useless*.

But maybe I’m wrong. Maybe equations of the form $x = x$ are useful in some way. I can imagine one coming in handy at the end of a proof by contradiction where you show some assumptions imply $x \ne x$. But I don’t remember ever doing such a proof… and I have trouble imagining that you ever *need* to use a proof of this style.

If you’ve used the equation $x = x$ in your own work, please let me know.

To explain my question a bit more precisely, it will help to choose a specific formalism: first-order classical logic with equality. We can get the rules for this system by taking first-order classical logic with function symbols and adding a binary predicate “$=$” together with three axiom schemas:

**1. Reflexivity**: for each variable $x$,

$x = x$

**2. Substitution for functions**: for any variables $x, y$ and any function symbol $f$,

$x = y \; \implies\; f(\dots, x, \dots) = f(\dots, y, \dots)$

**3. Substitution for formulas**: For any variables $x, y$ and any formula $\phi$, if $\phi'$ is obtained by replacing any number of free occurrences of $x$ in $\phi$ with $y$, such that these remain free occurrences of $y$, then

$x = y \;\implies\; (\phi \;\implies\; \phi')$

Where did symmetry and transitivity of equality go? They can actually be derived!

For transitivity, use ‘substitution for formulas’ and take $\phi$ to be $x = z$, so that $\phi'$ is $y = z$. Then we get

$x=y \;\implies\; (x = z \;\implies\; y = z)$

This is *almost* transitivity. From this we can derive

$(x = y \;\&\; x = z) \;\implies\; y = z$

and from this we can derive the usual statement of transitivity

$(x = y\; \& \; y = z) \;\implies\; x = z$

by choosing different names of variables and using symmetry of equality.

But how do we get symmetry? We can derive this using reflexivity and substitution for formulas. Take $\phi$ to be $x = x$ and take $\phi'$ be the result of substituting the first instance of $x$ with $y$: that is, $y = x$. Then we get

$x = y \;\implies \;(x = x \;\implies \;y = x)$

Using $x = x$, we can derive

$x = y \;\implies\; y = x$

This is the only time I remember using $x = x$ to derive something! So maybe this equation *is* good for something. But if proving symmetry and transitivity of equality is the *only* thing it’s good for, I’m not very impressed. I would have been happy to take both of these as axioms, if necessary. After all, people often do.

So, just to get the conversation started, I’ll conjecture that reflexivity of equality is completely useless if we include symmetry of equality in our axioms. Namely:

**Conjecture.** Any theorem in classical first-order logic with equality that does not include a subformula of the form $x = x$ for any variable $x$ can also be derived from a variant where we drop reflexivity, keep substitution for functions and substitution for formulas, and add this axiom schema:

**1’. Symmetry**: for any variables $x$ and $y$,

$x = y \; \implies \; y = x$

Proof theorists: can you show this is true, or find a counterexample? We’ve seen that we can get transitivity from this setup, and then I don’t really see how it hurts to omit $x = x$. I may be forgetting something, though!

## Re: Concepts of Sameness (Part 3)

You definitely want reflexivity in the list of conditions for an equivalence relation. Let $\sim$ be an equivalence relation without reflexivity on $X$. Then, if $x \in X$ is equivalent to anything, we can deduce that $x \sim x$. However, we can’t rule out the possibility that $x$ is equivalent to nothing, not even itself.

Therefore, we don’t get a map from $X$ to $X/\sim$. To me, one of the main purposes of equivalence relations is forming quotients, so this is definitely a problem.