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
.
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