Appendix A — Equality

In most mathematical theories, equality is taken as a primitive undefined relation. In order to use the equality relation it suffices to postulate the following properties1:

Here \(\mathscr{A}(x,x)\) stands for any formula in the given theory and \(\mathscr{A}(x,y)\) results from \(\mathscr{A}(x,x)\) by replacing some, but not necessarily all, ocurrences of \(x\) by \(y\). Moreover \(\mathscr{A}(x,x)\) may contain other variables in addition to \(x\).

Theorem A.1 (Symmetry) \(x = y \Longrightarrow y = x\)

Proof. Let \(\mathscr{A}(x,x)\) be \(x = x\) and \(\mathscr{A}(x,y)\) be \(y = x\) then \(x = y \Longrightarrow (x = x \Longrightarrow y = x)\). Because \(x = x\) and \(x = y \Longrightarrow (x = x \Longrightarrow y = x)\) by Exercise 1.8 \(x = y \Longrightarrow y = x\).

Theorem A.2 (Transitivity) \((x = y \land y = z) \Longrightarrow x = z\)

Proof. Let \(\mathscr{A}(y,y)\) be \(y = z\) and \(\mathscr{A}(y,x)\) be \(x = z\) then \(y = x \Longrightarrow (y = z \Longrightarrow x = z)\).

Also we have that \(x = y\) so by Theorem A.1 \(x = y \Longrightarrow y = x\). Because \(x = y \Longrightarrow y = x\) and \(y = x \Longrightarrow (y = z \Longrightarrow x = z)\) by Example 1.2 \(x = y \Longrightarrow (y = z \Longrightarrow x = z)\).

Finally by Exercise 1.12 because \(x = y \Longrightarrow (y = z \Longrightarrow x = z)\) then \((x = y \land y = z) \Longrightarrow x = z\).

Theorem A.3  

  • \(x = y \Longrightarrow x + z = y + z\)
  • \(x = y \Longrightarrow z + x = z + y\)

Proof.

  • Let \(\mathscr{A}(x,x)\) be \(x + z = x + z\) and \(\mathscr{A}(x,y)\) be \(x + z = y + z\) then \(x = y \Longrightarrow (x + z = x + z \Longrightarrow x + z = y + z)\). Because \(x + z = x + z\) and \(x = y \Longrightarrow (x + z = x + z \Longrightarrow x + z = y + z)\) then by Exercise 1.8 \(x = y \Longrightarrow x + z = y + z\).

  • Let \(\mathscr{A}(x,x)\) be \(z + x = z + x\) and \(\mathscr{A}(x,y)\) be \(z + x = z + y\) then \(x = y \Longrightarrow (z + x = z + x \Longrightarrow z + x = z + y)\). Because \(z + x = z + x\) and \(x = y \Longrightarrow (z + z = z + x \Longrightarrow z + x = z + y)\) then by Exercise 1.8 \(x = y \Longrightarrow z + x = z + y\).


  1. Check out Metamath Proof Explorer - Appendix 2: Traditional Textbook Axioms of Predicate Calculus↩︎