- English only
Lab for Automated Reasoning and Analysis LARA
We say that a relation is a congruence with respect to a set of functions and relations iff, when we consider a first-order language containing symbols for these functions and relations and interpret ‘eq’ as , the Axioms for Equality hold in the resulting structure .
We next fix as well as functions and relations and consider the set of all congruences on the set with respect to these functions and relations.
We assume no relation symbols other than congruence itself. (We represent a predicate as .)
Theorem: Let be a set of congruences. Then is also a congruence. Note: we define .
We will consider the case of . It case be generalized to arbitrary number of relation, because is associative.
Reflexive: because are congruence. It implies that .
Symmetric: because are congruence. It implies that .
End of Proof.
Theorem: Let be a relation. Let be the set of all congruences such that and let . Then is the least congruence containing , that is
- is a congruence
- if is a congruence such that , then
Let for .
Theorem: is the least congruence containing .
- : is a congruence that contains , thus .
- : by induction on .
- : by definition of
- : all elements introduced by are required to be in by definition of congruence, so if then also
End of Proof.