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 .
A terminological note: in algebra, an interpretation is often called a structure. Instead of using mapping language to interpretation of its symbols, the structure is denoted by a tuple . For example, an interpretation with domain , with one binary operation and one binary relation can be written as a pair . This avoids writing .
Example: quotient on pairs of natural numbers
Let . Consider a structure with domain , with functions \[
p((x_1,y_1),(x_2,y_2)) = (x_1 + x_2, y_1 + y_2)
\] \[
m((x_1,y_1),(x_2,y_2)) = (x_1 + y_2, y_1 + x_2)
\] Relation defined by \[
r = \{((x_1,y_1),(x_2,y_2)) \mid x_1 + y_2 = x_2 + y_1 \}
\] is a congruence with respect to operations and .
Congruence is an equivalence relation. What are equivalence classes for elements:
Whenever we have a congruence in an interpretation, we can shrink the structure to a smaller one by merging elements that are in congruence.
In the resulting structure we define operations and such that the following holds: \[ \begin{array}{l}
I_Q(p)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + x_2, y_1 + y_2)] \\ I_Q(m)( [(x_1,y_1)] , [(x_2,y_2)] ) = [(x_1 + y_2, y_1 + x_2)]
\end{array} \] This construction is an algebraic approach to construct from natural numbers one well-known structure. Which one?
Note: this construction can be applied whenever we have an associative and commutative operation satisfying the cancelation law . It allows us to contruct a structure where operation has an inverse. What do we obtain if we apply this construction to multiplication of strictly positive integers?
References
- Calculus of Computation Textbook, Section 3.1