# Precise axiomatic definition for the equality "=" as a binary relation

Question: What is a simple yet precise definition for "=" as a binary relation?

My try: I find two definitions for "equality relation" which seems to be contradictory.

The first one I learnt in school is that equality is what is called an equivalence relation, that is, it satisfies three axioms: Reflexivity, Symmetry, Transitivity.

The second definition contains an axiom of extensionality.

The third definition I heard contains this additional axiom: $$x=y$$ implies $$P(x)=P(y)$$

Thanks to the comments, I also learnt a definition using first-order logics:

These equality axioms are:

1. Reflexivity.
2. Substitution for functions.
3. Substitution for formulas.

This is close to the things I am looking for. However, this definition looks weird as the second axiom is a special case of the third. Axiomatic system usually don't use redundant axioms.

• The first two aren't definitions of equality: there are equivalence relations other than $=$ (consider "has the same parity as"), and the axiom of extensionality is a characterization of equality rather than a definition of it (okay, I suppose one could view $\in$ as more primitive than $=$ and then take extensionality as a definition of $=$ in terms of $\in$, but I personally don't buy that - if only because non-extensional set theories are also interesting). Feb 12 at 2:36
• Recently there was a similar query, my anser there applies here also Feb 12 at 3:35
• You are right that equality is an equivalence relation, but it is not the only one of course.
– Alex
Feb 12 at 3:46
• in my experience, in logic, $=$ is often used to denote the identity relation, that is, $a=b$ iff $a$ and $b$ are the very same object. In turn, this implies every predicate possessed by $a$ is also possessed by $b$ and vice versa. The identity relation is an example (or instance) of an equivalence relation, but there are equivalence relations that are not identity relations. Feb 12 at 6:06
• equality is a basic concept of human language and thought. In mathematics, it can be formalized using predicate logic. Feb 12 at 6:28

Yes, the two basic axioms for equality are reflexivity: $$x=x$$, and substitution for formulas: $$s = t \to (\varphi [s/z] \to \varphi [t/z])$$.

Note that, using Universal instantiation, we have that reflexivity holds for terms whatever: $$t=t$$.

Now, if $$f$$ is a function symbol (assuming for simplicity that it is a unary function symbol) from reflexivity we have $$f(x)=f(x)$$.

Thus, having that $$f(x)=f(x)$$ is $$(z=f(x))[f(x)/z]$$ and $$f(y)=f(x)$$ is $$(z=f(x))[f(y)/z]$$ we can use susbstitution to get:

$$x=y \to f(x)=f(y)$$.

The substitution property is crucial for equality: if the binary relation has reflexivity, symmetry and transitivity but lacks the substitution property its is an equivalence relation.

• Many thanks! So there are two equivalent definitions: The first one is reflexivity+substitution for formulas. The other one is reflexivity+symmetry+transitivity+substitution for functions?
– dodo
Feb 13 at 4:37
• How is substitution for function relates to substitution for predicates ($x=y\implies P(x)=P(y)$)?
– dodo
Feb 13 at 4:38
• @dodo - subst for predicate is a case of subst for formulas: $x=y \to (P(x) \to P(y))$. If $P$ is a predicate symbol, $P(x)=P(y)$ is wrong. Feb 13 at 6:43
• Oh, I didn't know this before. Good point!
– dodo
Feb 13 at 18:22