# Theory of equality

### From Learning Logic for Computer Science

The theory of equality is the theory of congruence relations.

# The theory of equality

Let $\mathcal S$ be an arbitrary signature. Assume $\text{Eq}/2$ is a symbol which is no element of $\mathcal S$ and let $\mathcal S_\text{Eq}$ be defined by $\mathcal S_\text{Eq} = \mathcal S \cup \{\text{Eq}/2\}$.

The **theory of equality** over $\mathcal S$, denoted $\text{ThE}(\mathcal S)$, is the set of all closed $\mathcal S_\text{Eq}$-formulas without equality which are true in all $\mathcal S_\text{Eq}$ structures $\mathcal A$ where $\text{Eq}^{\mathcal A} = \{\langle a,a \rangle \colon a \in A\}$, that is, where $\text{Eq}$ is interpreted as the equality relation.

# The congruence axioms

Let $\mathcal S$ be a signature and $R/2$ a symbol which is no element of $\mathcal S$. The **congruence axioms** for $R$ over $\mathcal S$ are:
\begin{align}
\tag{reflexivity}
& \forall x_0 R(x_0, x_0)\\
\tag{symmetry}
& \forall x_0 \forall x_1 (R(x_0, x_1) \leftrightarrow R(x_1, x_0))\\
\tag{transitivity}
& \forall x_0 \forall x_1 \forall x_2 (R(x_0, x_1) \wedge R(x_1, x_2) \rightarrow R(x_0, x_2))\\
\tag{cong-$f$}
& \forall x_0 \dots \forall x_{2n-1} (\bigwedge_{i<n} R(x_i, x_{n+i}) \rightarrow R(f(x_0, \dots, x_{n-1}), f(x_n, \dots, x_{2n-1}))) && \text{for $f/\!/n \in \mathcal S$}\\
\tag{cong-$S$}
& \forall x_0 \dots \forall x_{2n-1} (\bigwedge_{i<n} S(x_i, x_{n+i}) \rightarrow (S(x_0, \dots, x_{n-1}) \leftrightarrow S(x_n, \dots, x_{2n-1})) && \text{for $S/n \in \mathcal S$}
\end{align}
The set of these axioms is denoted $\text{Cong}(R, \mathcal S)$.

These axioms state that the relation $R$ is an equivalence relation which is compatible with all functions and relations. Such a relation is typically called a **congruence relation**.

**Lemma**
Let $\mathcal A$ be any $\mathcal S_R$ structure such that $\mathcal A \models \text{Cong}(R, \mathcal S)$. Denote the quotient of $\mathcal A$ modulo $R^\mathcal A$ by $\mathcal A/R^\mathcal A$. Then the following holds:

- $\mathcal A/R^\mathcal A$ is well-defined.
- The interpretation of $R$ in $\mathcal A/R^\mathcal A$ is the equality relation.
- For every $\mathcal S$-formula $\varphi$, \begin{align}\mathcal A \models \varphi \qquad \text{iff} \qquad \mathcal A/R^\mathcal A \models \varphi \enspace.\end{align}

Clearly, the equality relation is a congruence relation and satisfies these axioms:

**Lemma**
The equality relation satisfies these axioms, that is,
\begin{align}
\text{Cong}(\text{Eq}, \mathcal S) \subseteq \text{ThE}(\mathcal S) \enspace.
\end{align}

# Relation between the theory of equality and the congruence axioms

**Theorem**
Let $\mathcal S$ and $\text{Eq}$ be as above. Then, for every closed $\mathcal S_\text{Eq}$ formula $\varphi$ without equality,
\begin{align}
\varphi \in \text{ThE}(\mathcal S) \qquad \text{iff} \qquad \text{Cong}(\text{Eq}, \mathcal S) \models \varphi \enspace.
\end{align}

The direction from right to left follows from the second lemma above. For the direction from left to right, assume $\text{Cong}(\text{Eq}, \mathcal S) \not \models \varphi$. Then there is a structure $\mathcal A$ such that $\mathcal A \models \text{Cong}(\text{Eq}, \mathcal S) \cup \{\neg \varphi\}$. By the first lemma, it follows $\mathcal A/\text{Eq}^\mathcal A \not \models \varphi$, which implies $\varphi \notin \text{ThE}(\mathcal S)$.