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:
Definition: if an interpretation the axioms are true, then we call (the interpretation of eq) a congruence relation for interpretation .
Remark: Functions are a special case of relations. However, the condition above for function symbols is weaker than the condition for relation symbols. If is a function, then the relation does not satisfy the congruence condition because it only has one result, namely , and not all the results that are in relation eq with .
References
- Calculus of Computation Textbook, Section 3.1