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 x_i = y_i) \rightarrow 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 x_i = y_i) \rightarrow (R(x_1,\ldots,x_n) \leftrightarrow R(y_1,\ldots,y_n))
\]
References