# Universal Algebra 4: Equations, Congruences, Completeness

It may be a good idea to skip this lecture first and to go directly to the chapter on [term rewriting systems]() and to come back here for definitions as needed.

For this course, the current chapter is more background and only essential for those who want to go deeper into universal algebra or term rewriting. Having said this, it leaves a gap when ignored.

## Introduction

As we have seen, both solving equations in algebra and program execution in an ARS are special cases of equational reasoning. This leads to the following

**Question:** What precisely do we mean when we say that an equation $t\approx t'$ follows from a set of equations $E$?

We have also seen that equations can or cannot hold in an algebra. For example, in the term-algebra $\mathcal L$ for the signature $\{1,+,*\}$, the equation $\;1*1\approx 1\;$ is false, but in the natural numbers the equation $\;1*1\approx 1\;$ is true.

**Question:** What precisely do we mean when we say that an equation $t\approx t'$ holds in an algebra $A$?

Can we always derive all equations that are true in all algebras (possibly satisfying some axioms)? In other words:

**Question:** Are the rules of equational logic complete?

In this lecture we will answer some of these questions and more.

## What are equations?

We can profit from our understanding of free algebras/term algebras in order to understand equations precisely.

**Definition:** Let $\Sigma$ be a signature and $X$ a set of variables. An equation is a pair
$$(t,t')\in Term_\Sigma(X)\times Term_\Sigma(X)$$

Instead of $(t,t')$ we usually write $t\approx t'$.

**Reminder:** When we write $t=t'$ we mean equality in an algebra, when we write $t\approx t'$ we mean the pair $(t,t')$ in $Term_\Sigma(X)$.

**Remark:** Let $E$ be a set of equations $Term_\Sigma(X)$. We will see below how to use the notion of *congruence relation* in order to construct an algebra $Term_\Sigma(X)/E$ in which each equation $t\approx t'$ is turned into an equality.

## Congruence relations

#### Introduction

Conceptually, we have already seen the importance of [equivalence relations](https://hackmd.io/s/B1gOX4lO7#Equivalence-Relations) in many examples. We have also seen the importance of [structure preserving maps](https://hackmd.io/s/HkYir7AiQ). In this section we study congruence relations, which are *structure preserving equivalence relations*.

What is the idea of a structure preserving equivalence relation?

The reason why equivalence relations are so important is that they allow us to take quotients of sets. More precisely, whenever we have an equivalence relation $\equiv$ on a set $A$, then we can from the quotient (=set of equivalence classes) $A/{\equiv}$. Moreover, we get a function, sometimes also called the quotient,
$$A\to A/{\equiv}$$

mapping an element of $A$ to its equivalence class.

But what if $A$ is not a mere set, but carries some structure?

What to we need to add to the notion of equivalence relation in order to make sure that $A\to A/{\equiv}$ is a structure preserving map?

If the structure in question is algebraic, as given by a signature, then the answer is that we need the equivalence relation to be a congruence relation.

#### Example

The clock is a homomorphism
$$h:\mathbb Z\to Clock$$

As every function, $h$ gives rise to an equivalence relation
$$n\equiv m \ \stackrel{def}{\Leftrightarrow} h(n)=h(m)$$

The same equivalence relation can defined purely in terms of $\mathbb Z$ by
$$n\equiv m \ \stackrel{def}{\Leftrightarrow} \exists k\in \mathbb Z\,.\, n-m = 12k.$$

Moreover, the second definition allows us to get back $h$ as
\begin{align}
\mathbb Z & \to \mathbb Z/{\equiv}\\
n & \mapsto n\ \textrm{mod}\ 12
\end{align}
since $Clock$ is ismorphic to $\mathbb Z/{\equiv}$.

One question remains. We know that $h$ is not only a function but a homomorphism. Accordingly, $\equiv$ is not only an equivalence relation.

Which property of $\equiv$ guarantees that $\;\mathbb Z \to \mathbb Z/{\equiv}\;$ is not only a function but also a homomorphism?

The property that $h$ is structure preserving can be phrased intuitively as:

The Clock is neither fast nor slow but measures time the same everyday.

More precisely, if on two different days the clock shows the same time, and on both days I wait $n$ hours, then the clock also shows the same time on both days after my wait.

Even more precisely, in symbolic notation:

$$\frac{t\equiv t'}{t+n\equiv t'+n}$$

We arrived at the definition of a congruence relation in case we have one unary operation "$+n$".

#### Congruence relation, defined

More technically, the most important insight about equational logic is that the rules of equational logic capture what it means to be a surjective homomorphism (=structure preserving map).

**Definition:** A ***congruence relation*** on an algebra $A$ is an equivalence relation $\equiv$ closed under congruence, that is, if $f$ is an operation of arity $n$ and
$$t_i\equiv s_i$$

for $1\le i \le n$ then also
$$ f(t_1,\ldots t_n) \equiv f(s_1,\ldots s_n).$$

#### Proposition on congruence relations:

- Let $h:A\to B$ be a homomorphism. Then the so-called kernel $ker(h)=\{(t,s) \mid h(t)=h(s)\}$ is a congruence relation.

- Let $\equiv$ be a congruence relation on $A$. Then $A/{\equiv}$ is an algebra and the function $[-]_\equiv : A\to A/{\equiv}$ mapping $t\mapsto [t]_\equiv$ is a homomorphism.

Moreover, homomorphism and congruences determine each other in the following sense. If $h:A\to B$ is surjective, then $A/{ker(h)}$ is isomorphic to $B$. And if $\equiv$ is a congruence relation then $\equiv$ is the kernel of $[-]_\equiv$.

**Remark:** Notice that this is universal algebra terminology for what we discussed in the lecture on [meaning in syntax](). If $h:Term_\Sigma(X)\to A$ is a homomorphism, we can think of it as a meaning function from syntax to semantics. Then the relation $t\approx t' \ \stackrel{def}{\Leftrightarrow} h(t)=h(t')$ is a congruence relation and, moreover contains enough information to recover $A$ and $h$ up to isomorphism.

#### Remark on completeness

The proposition on congruence relations is essentially a completeness theorem for equational reasoning without variables. For a full explanation of this, we need more mathematical machinery to be developed below. But the basic idea can be exlained now:

Let $E$ be a set of equations without variables and $Term_\Sigma$ the corresponding term algebra. Let $t\approx t'$ be an equation that is true in all algebras $A$ in which the equations $E$ are true. We will show that $t\approx t'$ can be derived from $E$ using the rules of equational logic:

Let $\equiv$ be the smallest congruence relation containing $E$. Using the proposition on congruence relations, we know that $Term_\Sigma/E$, which we define to be $Term_\Sigma/{\equiv}$, is an algebra. Moreover, $Term_\Sigma/E$ is an algebra that satisfies, by its definition, all equations in $E$. So we know that $Term_\Sigma/E$ also satisfies $t\approx t'$. But this means that $t\approx t'$ is in the congruence $\equiv$ generated by $E$, which in turn means that there is a proof in equational logic deriving $t\approx t'$ from axioms in $E$.

## Syntactical consequence

In the lecture on [induction](), we have seen that, given a set of equations $E$ the rules of equational reasoning amount to an inductive definition of the smallest set $\approx_E$ of equations closed under the rules of equational logic and containing $E$ (the set of "axioms").

So to say that the equation $t\approx t'$ can be derived from a set of equations $E$ is equivalent to say that $t\approx t'$ is an element of $\approx_E$. In logic this is usually written as
$$E\vdash t\approx t'$$

## Semantical consequence

There is another take on consequence. We write
$$E\models t\approx t'$$

to mean that whenever an algebra $A$ satsifies "the axioms" $E$, it also satisfies $t\approx t'$. In symbols, $E\models t\approx t'$ if and only if for all algebras $A$
$$A\models E \ \Longrightarrow \ A\models t\approx t'$$

This leaves us with the task to explain what it means for an equation to hold for an algebra $A$. Intuitively an equation $t\approx t'$ should hold in $A$ if both sides are equal in $A$ for all substitutions of variables. This means (recall ...) that all homomorphisms
$$h:Term_\Sigma(X)\to A$$ we have $h(t)=h(t')$.

**Definition:** Let $\Sigma$ be a signature and $X$ a set of variables. Let $t\approx t'$ be an equation and $A$ and algebra.
We say that $t\approx t'$ holds in $A$, and write
$$A\models t\approx t'$$

if for all homomorphisms
$$h:Term_\Sigma(X)\to A$$

we have $h(t)=h(t')$. We write
$$A\models E$$

to say $A\models t\approx t'$ for all $t\approx t'$ in $E$.

## Soundness and Completeness of Equational Logic

An important theorem, called the soundness and completeness theorem of equational logic states that these two notions of consequence are equivalent.

**Theorem:** $\;E\vdash t\approx t'\;$ if and only if $\;E\models t\approx t'\;$.

*Proof:* (Sketch) *Soundness* is the direction from left to right. By induction on the definition of $\approx_E$, we have to show for each rule of equational logic that if the assumptions of the rule hold in $A$, then so does the conclusion. By definition, $A\models t\approx t'$ means that $h(t)=h(t')$. Since equality is reflexive, transitive and symmetric, the corresponding rules of equational logic are sound. The soundness of substitution comes from the definition of $A\models t\approx t'$ quantifying over all homomorphisms $h:Term_\Sigma(X)\to A$. The soundness of the congruence rule stems from homomorphisms preserving the operations.
$\quad$ *Completeness* is the converse. Among all the algebras in which $E$ holds is the termalgebra quotiented by the smallest congruence relation generated by $E$, which we denote by $Term_\Sigma(X)/E$. Let $h:Term_\Sigma(X)\to Term_\Sigma(X)/E$ be the homomorphism mapping each term to its equivalence class modulo $E$. Now assume $\;E\models t\approx t'\;$. It follows $h(t)=h(t')$. And by definition of $Term_\Sigma(X)/E$ this means that the equation $t\approx t'$ is in $\approx_E$.

**Remark:** This sketch does has some gaps. Most importantly, that the term algebra quotiented by $\approx_E$ is an algebra in which the equations $E$ hold. We have seen the importance of this in the variable free situation in the [Remark on completeness](https://hackmd.io/s/HyMesfK3Q#Remark-on-completeness). We fill this gap in the next section on fully invariant congruence relations, which extends the variable-free [congruence relations](https://hackmd.io/s/HyMesfK3Q#Congruence-relations) to the situation of equations with variables.

## Fully invariant congruence relations

In the section on [congruence relations](https://hackmd.io/s/HyMesfK3Q#Congruence-relations), and in the [remark on completeness](https://hackmd.io/s/HyMesfK3Q#Remark-on-completeness) in particular, we argued that the [proposition on congruence relations]() is a completeness theorem of equational logic without variables.

More precisely, a completeness theorem of equational logic in which variables are treated like constants in the sense that the rule of substitution is not admitted. For example, it would not be possible to deduce from $x+y=y+x$ that $2+3=3+2$ because this requires a substitution $[x\mapsto 2, y\mapsto 3]$.

It is our aim to extend congruence relations to the case with variables. For this we need to consider special congruences. The basic idea is clear, once we remember the rules of equational logic:

Equivalence relations are reflexive, transitive and symmetric.

Congruence relations add the congruence rule.

Fully invariant congruence relations add the substitution rule.

This is done in the following way. Recall that [substitutions on the term algebra are exactly the homomorphisms](https://hackmd.io/s/By3OtPAsQ#Substitution-as-a-homomorphism). The next definition is based on this idea and just that it replaces the term algebra by an arbitrary algebra $A$.

**Definition:** A ***fully invariant congruence relation*** on an algebra $A$ is a congruence relation $\approx$ closed under substitution, that is, if $h:A\to A$ is a homomorphism and $(t,t')$ in $\approx$, then $(h(t),h(t'))$ is also in $\approx$.

**Proposition on fully invariant congruence relations:**

...