This is an old revision of the document!
Axioms for Equality
For language and a relation symbol , the theory of equality, denoted AxEq, is the following set of formulas:
Reflexivity:
Symmetry:
Transitivity:
Congruence for function symbols: for
function symbol with
,
\[ \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n eq(x_i,y_i)) \rightarrow eq(f(x_1,\ldots,x_n),f(y_1,\ldots,y_n))
\]
Congruence for relation symbols: for
relation symbol with
,
\[ \forall x_1,\ldots,x_n, y_1,\ldots,y_n.\ (\bigwedge_{i=1}^n eq(x_i,y_i)) \rightarrow (R(x_1,\ldots,x_n) \leftrightarrow R(y_1,\ldots,y_n))
\]
Definition: if an interpretation the axioms are true, then we call (the interpretation of eq) a congruence relation for interpretation .
References