Theory of equality

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)$.