\[\begin{prooftree}
\AXC{$t = t$}
\end{prooftree}
\quad \quad
\begin{prooftree}
\AXC{$s = t$}
\UIC{$t = s$}
\end{prooftree}
\quad \quad
\begin{prooftree}
\AXC{$r = s$}
\AXC{$s = t$}
\BIC{$r = t$}
\end{prooftree}
\quad\quad
\begin{prooftree}
\AXC{$s_1 = t_1$}
\AXC{$\ldots$}
\AXC{$s_n = t_n$}
\TIC{$f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)$}
\end{prooftree}
\]

.. raw:: latex
\begin{center}
\AXC{$t = t$}
\DP
\quad \quad
\AXC{$s = t$}
\UIC{$t = s$}
\DP
\quad \quad
\AXC{$r = s$}
\AXC{$s = t$}
\BIC{$r = s$}
\DP
\quad \quad
\AXC{$s_1 = t_1$}
\AXC{$\ldots$}
\AXC{$s_n = t_n$}
\TIC{$f(s_1, \ldots, s_n) = f(t_1, \ldots, t_n)$}
\DP
\end{center}
The first three rules express the reflexivity, symmmetry, and transitivity of equality,
respectively.
The last rule is called the *congruence* rule.
You should convince yourself that using these rules we can derive
.. raw:: html
\[\begin{prooftree}
\AXC{$r = s$}
\UIC{$t[r/x] = t[s/x]$}
\end{prooftree}
\]

.. raw:: latex
\begin{center}
\AXC{$r = s$}
\UIC{$t[r/x] = t[s/x]$}
\DP
\end{center}
for any terms :math:`r`, :math:`s`, and :math:`t` and variable :math:`x`. If we add relation symbols
and atomic formulas, we would add the following rule:
.. raw:: html
\[
\begin{prooftree}
\AXC{$s_1 = t_1$}
\AXC{$\ldots$}
\AXC{$s_n = t_n$}
\AXC{$R(s_1, \ldots, s_n)$}
\QuaternaryInfC{$R(t_1, \ldots, t_n)$}
\end{prooftree}
\]

.. raw:: latex
\begin{center}
\AXC{$s_1 = t_1$}
\AXC{$\ldots$}
\AXC{$s_n = t_n$}
\AXC{$R(s_1, \ldots, s_n)$}
\QuaternaryInfC{$R(t_1, \ldots, t_n)$}
\DP
\end{center}
Returning to our proof plan, we want to show that if applying these rules successively
does not result in a contradiction, then there is a model in which the original equations
and disequations are all true.
But a problem arises: what if the original set contains an equation :math:`a = f(a)`?
Then our algorithm falls into an infinite loop, deriving
:math:`a = f(a) = f(f(a)) = f(f(f(a))) = \ldots`.
The solution is to restrict attention to *subterms* of terms appearing in the original
equations and disequations.
The theorem follows from the following lemma.
.. admonition:: Lemma
Let :math:`\Gamma` consist of a set of equations and disequations.
Let :math:`S` be the set of subterms of all the terms occurring in :math:`\Gamma`.
Let :math:`\Gamma'` be the set of al equations between elements of :math:`S`
that can be derived from the equations in :math:`\Gamma` using the rules above.
Then :math:`\Gamma` is satisfiable if and only if no disequation in :math:`\Gamma`
is the negation of an equation in :math:`\Gamma'`.
The algorithm implicit in this lemma is called *congruence closure*.
We will see that it can be implemented efficiently (and *is* implemented efficiently in SMT
solvers) using *union-find* data structures.
.. admonition:: Proof
One direction of the lemma is easy. Since the equational rules preserve truth in any
model, if we can derive a contradiction from the equations and disequations in :math:`\Gamma`,
then :math:`\Gamma` is unsatisfiable. The other direction is harder.
Since there are only finitely many pairs of terms in :math:`S`, the algorithm necessarily
terminates.
We need to show that if it terminates without deriving a contradiction, then there is a model
that satisfies :math:`\Gamma`.
Say two elements :math:`s` and :math:`t` are *equivalent*, written :math:`s \equiv t`,
if they are proved equal from the
equations in :math:`\Gamma`. The rules guarantee that this is an *equivalence relation*, which is
to say, it is reflexive, symmetric, and transitive. It is also a *congruence*, which means that
applying a function symbol to equivalent terms results in equivalent terms.
To each element :math:`t`, we associate its *equivalence class* :math:`[t]`, defined by
.. math::
[t] = \{ s \in S \mid s \equiv t \}.
In words, :math:`[t]` is the set of terms equivalent to :math:`t`.
Assuming the algorithm terminates without a contradiction, define a model :math:`\mdl M`
whose universe consists of all the equivalence classes of elements of :math:`S`
together with a new element, :math:`\star`. For elements :math:`t_1, \ldots t_n` in :math:`S`,
interpret each :math:`n`-ary function symbol :math:`f` by function
.. math::
f^{\mdl M}([t_1], \ldots, [t_n]) = \begin{cases}
[f(t_1, \ldots, t_n)] & \text{if $f(t_1, \ldots, t_n)$ is in $S$} \\
\star & \text{otherwise}
\end{cases}
In other words, what :math:`f^{\mdl M}` does to each equivalence class is determined by what
:math:`f` does to each of the elements.
The fact that :math:`\equiv` is a congruence ensures that this makes sense.
This is just a truncated version of the term model, in which provably equal terms
are all glued together.
It is not hard to show that for every term :math:`t` in :math:`S`,
:math:`\tval{t}_{\mdl M}` is equal to :math:`[t]`.
But this is what we need. For every equation :math:`s = t` in :math:`\Gamma`, :math:`s` and :math:`t` are in the
same equivalence class, so they are equal in the model.
And if :math:`s` and :math:`t` are not provably equal, then :math:`[s]` and :math:`[t]` are not the same, so
every disequation :math:`s \ne t` in :math:`\Gamma` is true in :math:`\mdl M` as well.
For examples of the algorithm in action, first let us show that the set
.. math::
f^3(a) = a, \, f^5(a) = a, \, f(a) \ne a
is unsatisfiable, where :math:`f^n(a)` abbreviates :math:`n`-fold application :math:`f(f(\cdots f(a)))`.
The set of all subterms is
.. math::
a, \, f(a), \, f^2(a), \, f^3(a), \, f^4(a), \, f^5(a).
We start with the equivalence classes :math:`\{ a, f^3(a) \}` and :math:`\{ a, f^5(a)\}`
as well as all the others subterms in singleton sets.
From :math:`a = f^3(a)` we derive :math:`f(a) = f^4(a)` by congruence, giving rise to the set
:math:`\{ f(a), f^4(a) \}`. Applying congruence again gives rise to the set :math:`\{ f^2(a), f^5(a) \}`,
which is merged with :math:`\{ a, f^5(a)\}` to yield :math:`\{ a, f^2(a), f^5(a) \}`.
Applying congruence again yields :math:`\{ f(a), f^3(a) \}`. (We ignore the term :math:`f^6(a)`.)
This is merged with the set :math:`\{ a, f^3(a) \}` to yield :math:`\{ a, f(a), f^3(a)\}`.
Applying congruence again yields :math:`\{ f(a), f^2(a), f^4(a)\}`, which is merged with
:math:`\{ a, f(a), f^3(a) \}` and :math:`\{ f^2(a), f^5(a) \}` to yield
:math:`\{ a, f(a), f^2(a), f^3(a), f^5(a) \}`.
At this point, we have derived :math:`f(a) = a`, contradicting the disequality in the original set.
So the set is unsatisfiable.
Suppose we start instead with the set
.. math::
f^2(a) = a, \, f^4(a) = a, \, f(a) \ne a, \, f(a) \ne b
You can check that in this case, the algorithm terminates with the following three
equivalence classes:
- :math:`[a] = \{ a, f^2(a), f^4(a)\}`
- :math:`[f(a)] = \{ f(a), f^3(a) \}`
- :math:`[b] = \{ b \}`.
We now construct a model :math:`\mdl M` with these elements and an additional element :math:`\star`, with
.. math::
f^{\mdl M}([a]) & = [f(a)] \\
f^{\mdl M}([f(a)]) & = [a] \\
f^{\mdl M}([b]) & = \star \\
f^{\mdl M}(\star) & = \star
You can check that this satisfies the original set of equations and disequations.
Suppose we allow atomic formulas :math:`R(t_1, \ldots, t_n)` and negated atomic formulas in :math:`\Gamma`.
To test satisfiability, we do not have to change much.
Using the congruence rule for relations, whenever we have derived :math:`R(s_1, \ldots, s_n)`
and :math:`s_i = t_i` for every :math:`i`, we can conclude :math:`R(t_1, \ldots, t_n)`.
The algorithm terminates when we contradict a disequality or another negated atomic formula.
If the algorithm terminates without a contradiction, we build a model as before,
where we simply declare that :math:`R^{\mdl M}([t_1], \ldots, [t_n])` holds if and only if
we have determined that :math:`R(t_1, \ldots, t_n)` in a consequence of the original set.
Now suppose we are given an existential sentence :math:`\ex {x_1, \ldots, x_n} A`
where :math:`A` is quantifier-free, and suppose we want to determine whether it is satisfiable.
Replace :math:`x_1, \ldots, x_n` in :math:`A` with new constants :math:`c_1, \ldots, c_n`.
The resulting quantifier-free sentence is satisfiable if and only if the existential one is.
Put that sentence in DNF, and use the fact :math:`A_1 \lor \cdots \lor A_n` is satisfiable
if and only if one of the sentences :math:`A_i` is.
That reduces the task to determining whether a conjunction of literals is satisfiable,
and we have just explained how to do that.
Since a sentence is valid if and only if its negation is satisfiable, and since the negation
of a universal sentence is an existential sentence, we have shown the following.
.. admonition:: Theorem
The satisfiability of an existential sentence in first-order logic is decidable.
Equivalently, the validity of a universal sentence is decidable.
.. TODO: In the exercises, show the convexity of equational logic.