First-order Logic - Equality and Its Axioms

Equality and Its Axioms

There are several different conventions for using equality (or identity) in first-order logic. The most common convention, known as first-order logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:

1. Reflexivity. For each variable x, x = x.
2. Substitution for functions. For all variables x and y, and any function symbol f,

   x = y → f(...,x,...) = f(...,y,...).

3. Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then

   x = y → (φ → φ').

These are axiom schemes, each of which specifies an infinite set of axioms. The third scheme is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second scheme, involving the function symbol f, is (equivalent to) a special case of the third scheme, using the formula

x = y → (f(...,x,...) = z → f(...,y,...) = z).

Many other properties of equality are consequences of the axioms above, for example:

1. Symmetry. If x = y then y = x.
2. Transitivity. If x = y and y = z then x = z.