Equality axioms

Axioms regularizing the use of the equality relation in mathematical proofs. These axioms assert the reflexivity of the equality relation and the possibility of substituting equals for equals. Symbolically the equality axioms are written:

$$ x = x , $$

$$ x = y \wedge \phi ( y | v) \Rightarrow \phi ( x | v), $$

$$ x = y \Rightarrow t ( y | v) = t ( x | v), $$

where $ \phi $ is a formula and $ t $ is a term in the language in question, $ x $, $ y $ and $ v $ are variables having the same non-empty domain of variation, and expressions of the form $ \phi ( x \mid v) $ and $ t ( x \mid v) $ denote the result of replacing all free occurrences of $ v $ in $ \phi $ or $ t $ by $ x $.

Using equality axioms, the symmetry and transitivity of the equality relation can be proved. To do this take $ \phi $ to be the formula $ y = v $ in the first case and the formula $ v = z $ in the second.

If the formulas and terms of the language in question are constructed from atomic formulas and terms using logical connectives and superposition, then the reduced equality axioms can be derived from their particular cases when $ \phi $ and $ t $ are atomic formulas and terms. Symbolically:

$$ x _ {i} = y _ {i} \wedge P ( x _ {1} \dots x _ {i} \dots x _ {n} ) \Rightarrow \ P ( x _ {1} \dots y _ {i} \dots x _ {n} ), $$

$$ x _ {i} = y _ {i} \Rightarrow f ( x _ {1} \dots x _ {i} \dots x _ {n} ) = f ( x _ {1} \dots y _ {i} \dots x _ {n} ), $$

where $ P $ and $ f $ are $ n $- place predicate and function symbols.

References

[a1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1950) pp. Chapt. XIV