When we define an equality ($=$) of things, for example of vectors in $\mathbb{R}^n$ or of sets in ZF by the Axiom of Extensionality, are there properties that we need to check in order for $=$ to be a "consistent equality notion"? For example, if I defined $v=u$ by $1=-8$ then this would be inconsistent... The Reflexivity axiom for first-order logic with equality would not be verified. So, for example, what do I need to check in order to be sure that the definition $$ (a,b)=(c,d)\iff a=c\text{ and }b=d $$ of equality in $\mathbb{R}^2$ is correct, that is, that it can be taken as an equality in the way we want equality to behave?


The basic laws of equality (or identity) are :

I.1 $∀x \ (x = x)$

I.2 $∀x∀y \ (x = y → y = x)$

I.3 $∀x∀y∀z \ (x = y ∧ y = z → x = z)$

I.4 $∀x_1 \ldots x_n y_1 \ldots y_n \ (x_1 = y_1 \land \ldots \land x_n = y_n → t(x_1, \ldots ,x_n) = t(y_1,\ldots, y_n))$,

$ \ \ \ \ \ ∀x_1 \ldots x_n y_1 \ldots y_n \ (x_1 = y_1 \land \ldots \land x_n = y_n → \varphi(x_1, \ldots ,x_n) \to \varphi(y_1,\ldots, y_n))$.

The first three formulae express : reflexivity, symmetry and transitivity, respectively, of equality.

The last one is a schema that must be "applied" to e.g. any functional symbol of the language.

Considering the language of arithmetic with the function symbol $+$ for sum, in this case I.4 will be :

$∀x_1 x_2 y_1 y_2 \ (x_1 = y_1 \land x_2 = y_2 → (x_1 + x_2) = (y_1 + y_2))$.

Tho prove the above properties, the following axioms are sufficient [see Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112] :

1) $x = x$

2) $x = y → (\alpha → \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing some (but not necessarily all) occurrences of $x$ by $y$.

Regarding set theory, if we want to read the Axiom of Extensionality as a definition for $=$ :

$$A=B \leftrightarrow \forall x \ (x \in A \leftrightarrow x \in B)$$

this is not enough.

It is straightforward to verify that the first three identity laws above are satisfied :

I.1. $A=A$ : $x \in A \leftrightarrow x \in A$ : tautology; thus : $\forall x (x \in A \leftrightarrow x \in A)$, by generalization.

I.2. $A=B \to B=A$ : $(x \in A \leftrightarrow x \in B)$; thus : $(x \in B \leftrightarrow x \in A)$, by tautological consequence.

I.3. Exercise.

For the fourth one, we have that in f-o set theory, there is only one (binary) predicate symbol : $\in$ (and no function symbols).

Thus, we have to verify that :

$∀x_1 y_1 z \ (x_1 = y_1 → (z \in x_1) \to (z \in y_1))$


$∀x_1 y_1 z \ (x_1 = y_1 → (x_1 \in z) \to (y_1 \in z))$

For the first part, we have that $x_1 = y_1 \leftrightarrow \forall z (z \in x_1 \leftrightarrow z \in y_1)$.

But for the second one, we have to postulate it.

  • 1
    $\begingroup$ $\color{#c00}{(a)}$ Aren't I.2 and I.3 consequences of I.1 and I.4 in any first order system? (Proposition 5.4 in Hamilton's Logic for Mathematicians) $\color{#c00}{(b)}$ We give axioms for equality, but then we define equality, for example in ZF by the Axiom of Extensionality. So, my concern is: shouldn't we verify that our definition of equality is consistent with the axioms for equality? That is to say, shouldn't we check that I.1 and I.4 are verified in that case? I've never seen this done after an introduction of the Axiom of Extensionality, for example. $\endgroup$ – Guest Nov 26 '15 at 15:32
  • $\begingroup$ @Guest - 1st comment : Hamilton consider equality ($=$) as an "interpretable" (binary) prdicate symbol $A_1^2$. I'll prefer to consider it a "logical" symbol not to be interpreted. If so, we can have a math theory with no extra-logical symbols ("pure" f-o theory of equality) without predicate and function symbols; in this case axiom schema I.4 has no instances. $\endgroup$ – Mauro ALLEGRANZA Nov 26 '15 at 15:43
  • $\begingroup$ @Guest - but see Hamilton, page 117 : "The first order language which is appropriate for ZF contains variables, punctuation,.connectives and quantifier as usual, and the predicate symbols $=$ and $A_2^2$ (no function letters or individual constants). $A_2^2$ is intended to be interpreted as , the relation of membership ($\in$)." Thus, (ZF1) is not intended as a definition of equality $\endgroup$ – Mauro ALLEGRANZA Nov 26 '15 at 16:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.