Quotient of an Interpretation under a Congruence
Example: quotient on pairs of natural numbers
Let . Consider a structure with domain , with functions (plus and minus):
Relation defined by
is a congruence with respect to operations and . Indded, we can check that, for example, if and then
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:
Note: this construction can be applied whenever we have an associative and commutative operation satisfying the cancelation law . It allows us to construct a structure where operation has an inverse. What do we obtain if we apply this construction to multiplication of strictly positive integers?
Definition of Quotient of an Interpretation
(Recall notation in First-Order Logic Semantics.)
Let be an interpretation of language with for which Axioms for Equality hold, that is, is a congruence relation for . We will construct a new model .
For each element , define
The constructed model will be where
In particular, when is we have
Functions are special case of relations:
Interpretation of variables is analogous to interpretation of constants:
Lemma 0: For all ,
Lemma 1: For each function symbol with , the relation is a total function and for all ,
Lemma 2: For each term we have .
Theorem: For each formula that contains no '=' symbol, we have where is result of replacing 'eq' with '=' in .