A Congruence Closure Theorem

Recall that we convert all relation symbols into function symbols (to simplify the Axioms for Equality).

Theorem Let $E$ be a set of ground equalities and disequalities ( $E := \bigwedge_{i = 0}^m t_i = t_i^\prime \wedge \bigwedge_{i = m+1}^n t_i \neq t_i^\prime$ ). Then the following are equivalent:

$E$ is satisfiable
there exists a congruence on ground terms in which $E$ is true
$E$ is true in the least congruence $r_*$ containing $r_0 = \{(t_1,t_2) \mid (t_1=t_2) \in E \}$
for the least congruence $r_*$ containing $r_0 = \{(t_1,t_2) \mid (t_1=t_2) \in E \}$ we have $(t_1 \neq t_2) \in E$ implies $(t_1,t_2) \notin r_*$

Proof:

The equivalence of first two statements follows from the construction of Herbrand Universe for Equality. We also directly show this special case.

The equivalence of last two statements follows by definition.

We show equivalence of second and third statement.

Third statement trivially implies second.

Consider any congruence $r$ in which $E$ is true.

Then $r_0 \subseteq r$ .

Therefore $r_* \subseteq r$ .

Therefore $E$ is true in $r_*$ as well.

Proof End.