Equational theories

3 General implications

In this chapter we record some general implications between equational laws.

Theorem 3.1 Singleton law implies all other laws

The singleton law (Definition 2.2) implies all other laws.

Proof

This is clear from substitution.

Theorem 3.2 All laws imply the trivial law

All laws imply the trivial law (Definition 2.1).

Proof

Trivial.

Every law \(E\) has a dual \(E^{\mathrm{op}}\), formed by replacing the magma operation \(\circ \) with its opposite \(\circ ^{\mathrm{op}}:(x,y) \mapsto y \circ x\). For instance, the opposite of the law \(x \circ y = x \circ z\) is \(y \circ x = z \circ x\). A list of equations and their duals can be found here. Of the 4694 equations under consideration, 84 are self-dual, leaving 2305 pairs of dual equations.

The implication graph has a duality symmetry:

Theorem 3.3 Duality

If \(E,F\) are equational laws, then \(E\) implies \(F\) if and only if \(E^{\mathrm{op}}\) implies \(F^{\mathrm{op}}\).

Proof

This is because a magma \(M\) obeys a law \(E\) if and only if the opposite magma \(M^{\mathrm{op}}\) obeys \(E^{\mathrm{op}}\).

Some equational laws can be “diagonalized”:

Theorem 3.4 Diagonalization

An equational law of the form

\begin{equation} \label{prediag} F(x_1,\dots ,x_n) = G(y_1,\dots ,y_m), \end{equation}
1

where \(x_1,\dots ,x_n\) and \(y_1,\dots ,y_m\) are distinct indeterminates, implies the diagonalized law

\[ F(x_1,\dots ,x_n) = F(x'_1,\dots ,x'_n). \]

In particular, if \(G(y_1,\dots ,y_m)\) can be viewed as a specialization of \(F(x'_1,\dots ,x'_n)\), then these two laws are equivalent.

Proof

From two applications of 1 one has

\[ F(x_1,\dots ,x_n) = G(y_1,\dots ,y_m) \]

and

\[ F(x'_1,\dots ,x'_n) = G(y_1,\dots ,y_m) \]

whence the claim.

Thus for instance, Definition 2.7 is equivalent to Definition 2.2.