# Introduction to universal algebra and clones

Soichiro Fujii  Research Institute for Mathematical Sciences, Kyoto University
Kyoto 606-8502, Japan<EMAIL_ADDRESS>
###### Abstract.

The purpose of this note is to provide a gentle introduction to basic
universal algebra and (abstract) clones.

###### Key words and phrases:

Universal algebra, equational logic, clones

###### 2010 Mathematics Subject Classification:

03C05, 08B05

The author is supported by ERATO HASUO Metamathematics for Systems Design
Project (No. JPMJER1603), JST

##  1\. Introduction

In almost every field of pure and applied mathematics, _algebras_ (in a broad
sense) arise quite naturally in one way or another. An algebra, typically, is
a set equipped with a family of operations on it. So for example the symmetric
group of degree five $\mathfrak{S}_{5}$ and the ring of integers $\mathbb{Z}$
are both algebras. Structural similarities between important algebras have led
to the introduction and study of various _types of algebras_ , such as
monoids, groups, rings, vector spaces over a field, lattices, Boolean
algebras, and Heyting algebras. A type of algebras is normally specified by a
family of operations and a family of equational axioms. We shall call such a
specification of a type of algebras an _algebraic theory_.

Subsequently, various authors have set out to develop a background theory, or
a metatheory for a certain type of algebraic theories. The most famous
classical example is Birkhoff’s _universal algebra_ [Bir35].111Other examples
of metatheories include those of non-symmetric and symmetric operads [May72],
PROs and PROPs [ML65], generalised operads [Bur71, Kel92, Her00, Lei04], and
monads [EM65, Lin66]; cf. [Fuj18, Fuj19]. By working at this level of
generality, one can prove theorems for various types of algebras once and for
all; for instance, the homomorphism theorems in universal algebra (see e.g.,
[BS81, Section II.6]) generalise the homomorphism theorems for groups to
monoids, rings, lattices, etc. A metatheory also provides a method to relate
different types of algebras, by means of morphisms between algebraic theories.

In this note, we explain the basics of universal algebra. We shall confine
ourselves to the most basic definitions; we focus on _presentations of
equational theories_ , the type of algebraic theories universal algebra deals
with. We then describe a presentation independent version of them, namely
_(abstract) clones_. This note is based on Sections 2.1 and 2.2 of the
author’s thesis [Fuj18].

##  2\. Universal algebra

Universal algebra [Bir35] deals with types of algebras defined by finitary
operations and equations between them. As a running example, let us consider
_groups_. A group may be defined as a set $G$ equipped with an element
$e^{G}\in G$ (the unit), and two functions $i^{G}\colon G\longrightarrow G$
(the inverse) and $m^{G}\colon G\times G\longrightarrow G$ (the
multiplication), satisfying the following axioms:

  * •

for all $g_{1}\in G$, $m^{G}(g_{1},e^{G})=g_{1}$ (the right unit axiom);

  * •

for all $g_{1}\in G$, $m^{G}(g_{1},i^{G}(g_{1}))=e^{G}$ (the right inverse
axiom);

  * •

for all $g_{1},g_{2},g_{3}\in G$,
$m^{G}(m^{G}(g_{1},g_{2}),g_{3})=m^{G}(g_{1},m^{G}(g_{2},g_{3}))$ (the
associativity axiom).222From these three axioms it follows that for all
$g_{1}\in G$, $m^{G}(e^{G},g_{1})=g_{1}$ (the left unit axiom) and
$m^{G}(i^{G}(g_{1}),g_{1})=e^{G}$ (the left inverse axiom) hold.

This definition of group turns out to be an instance of the notion of
_presentation of an equational theory_ , one of the most fundamental notions
in universal algebra.

First we introduce the notion of _graded set_ , which provides a convenient
language for our exposition.

######  Definition 2.1.

  1. (1)

An ($\mathbb{N}$-)graded set $\Gamma$ is a family
$\Gamma=(\Gamma_{n})_{n\in\mathbb{N}}$ of sets indexed by natural numbers
$\mathbb{N}=\\{0,1,2,\dots\\}$. By an element of $\Gamma$ we mean an element
of the set $\coprod_{n\in\mathbb{N}}\Gamma_{n}=\\{\,(n,\gamma)\mid
n\in\mathbb{N},\gamma\in\Gamma_{n}\,\\}$. We write $x\in\Gamma$ iff $x$ is an
element of $\Gamma$.

  2. (2)

If $\Gamma=(\Gamma_{n})_{n\in\mathbb{N}}$ and
$\Gamma^{\prime}=(\Gamma^{\prime}_{n})_{n\in\mathbb{N}}$ are graded sets, then
a morphism of graded sets $f\colon\Gamma\longrightarrow\Gamma^{\prime}$ is a
family of functions
$f=(f_{n}\colon\Gamma_{n}\longrightarrow\Gamma^{\prime}_{n})_{n\in\mathbb{N}}$.

We can routinely extend the basic notions of set theory to graded sets. For
example, we say that a graded set $\Gamma^{\prime}$ is a graded subset of a
graded set $\Gamma$ (written as $\Gamma^{\prime}\subseteq\Gamma$) iff for each
$n\in\mathbb{N}$, $\Gamma^{\prime}_{n}$ is a subset of $\Gamma_{n}$. Given
arbitrary graded sets $\Gamma$ and $\Gamma^{\prime}$, their cartesian product
(written as $\Gamma\times\Gamma^{\prime}$) is defined by
$(\Gamma\times\Gamma^{\prime})_{n}=\Gamma_{n}\times\Gamma^{\prime}_{n}$ for
each $n\in\mathbb{N}$. An equivalence relation on a graded set $\Gamma$ is a
graded subset $R\subseteq\Gamma\times\Gamma$ such that each
$R_{n}\subseteq\Gamma_{n}\times\Gamma_{n}$ is an equivalence relation on the
set $\Gamma_{n}$. Given such an equivalence relation $R$ on $\Gamma$, we can
form the quotient graded set $\Gamma/R$ by setting
$(\Gamma/R)_{n}=\Gamma_{n}/R_{n}$, the quotient set of $\Gamma_{n}$ with
respect to $R_{n}$. These notions will be used below.

A graded set can be seen as a _(functional) signature_. That is, we can regard
a graded set $\Sigma$ as the signature whose set of $n$-ary functional symbols
is given by $\Sigma_{n}$ for each $n\in\mathbb{N}$. We often use the symbol
$\Sigma$ to denote a graded set when we want to emphasise this aspect of
graded sets, as in the following definition.

######  Definition 2.2.

Let $\Sigma$ be a graded set.

  1. (1)

A $\Sigma$-algebra $\mathbf{A}$ is a set $A$ equipped with, for each
$n\in\mathbb{N}$ and $\sigma\in\Sigma_{n}$, a function
${[\\![\sigma]\\!]}^{\mathbf{A}}\colon A^{n}\longrightarrow A$ called the
interpretation of $\sigma$.333Note that we allow the set $A$ to be empty. In
traditional universal algebra the underlying set of a $\Sigma$-algebra is
usually required to be nonempty. We write such a $\Sigma$-algebra
$\mathbf{A}=(A,({[\\![\sigma]\\!]}^{\mathbf{A}})_{n\in\mathbb{N},\sigma\in\Sigma_{n}})$
simply as $(A,{[\\![-]\\!]}^{\mathbf{A}})$. We sometimes omit the superscript
in ${[\\![-]\\!]}^{\mathbf{A}}$.

  2. (2)

If $\mathbf{A}=(A,{[\\![-]\\!]}^{\mathbf{A}})$ and
$\mathbf{B}=(B,{[\\![-]\\!]}^{\mathbf{B}})$ are $\Sigma$-algebras, then a
$\Sigma$-homomorphism from $\mathbf{A}$ to $\mathbf{B}$ is a function $f\colon
A\longrightarrow B$ such that for any $n\in\mathbb{N}$, $\sigma\in\Sigma_{n}$
and $a_{1},\dots,a_{n}\in A$,

$f({[\\![\sigma]\\!]}^{\mathbf{A}}(a_{1},\dots,a_{n}))={[\\![\sigma]\\!]}^{\mathbf{B}}(f(a_{1}),\dots,f(a_{n}))$

holds (that is, the diagram

$A^{n}$$B^{n}$$A$$B$$f^{n}$${[\\![\sigma]\\!]}^{\mathbf{B}}$${[\\![\sigma]\\!]}^{\mathbf{A}}$$f$

commutes).

As an example, let us consider the graded set $\Sigma^{\mathrm{Grp}}$ defined
as $\Sigma^{\mathrm{Grp}}_{0}=\\{e\\}$, $\Sigma^{\mathrm{Grp}}_{1}=\\{i\\}$,
$\Sigma^{\mathrm{Grp}}_{2}=\\{m\\}$ and $\Sigma^{\mathrm{Grp}}_{n}=\emptyset$
for all $n\geq 3$. Then the structure of a group is given by that of a
$\Sigma^{\mathrm{Grp}}$-algebra. Note that to give an element $e^{G}\in G$ is
equivalent to give a function ${[\\![e]\\!]}\colon 1\longrightarrow G$ where
$1$ is a singleton set, and that for any set $G$, $G^{0}$ is a singleton set.
Also, between groups, the notions of group homomorphism and
$\Sigma^{\mathrm{Grp}}$-homomorphism coincide.

However, not all $\Sigma^{\mathrm{Grp}}$-algebras are groups; for a
$\Sigma^{\mathrm{Grp}}$-algebra to be a group, the interpretations must
satisfy the group axioms. Notice that all group axioms are equations between
certain expressions built from variables and operations. This is the
fundamental feature shared by all types of algebras expressible in universal
algebra. The following notion of $\Sigma$-term defines “expressions built from
variables and operations” relative to arbitrary graded sets $\Sigma$.

######  Definition 2.3.

Let $\Sigma$ be a graded set. The graded set
$T(\Sigma)=(T(\Sigma)_{n})_{n\in\mathbb{N}}$ of $\Sigma$-terms is defined
inductively as follows.

  1. (1)

For each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$,

$x_{i}^{(n)}\in T(\Sigma)_{n}.$

We sometimes omit the superscript and write $x_{i}$ for $x_{i}^{(n)}$.

  2. (2)

For each $n,k\in\mathbb{N}$, $\sigma\in\Sigma_{k}$ and $t_{1},\dots,t_{k}\in
T(\Sigma)_{n}$,

$\sigma(t_{1},\dots,t_{k})\in T(\Sigma)_{n}.$

When $k=0$, we usually omit the parentheses in $\sigma()$ and write instead as
$\sigma$.

An immediate application of the inductive nature of the above definition of
$\Sigma$-terms is the canonical extension of the interpretation function
${[\\![-]\\!]}$ of a $\Sigma$-algebra from $\Sigma$ to $T(\Sigma)$.

######  Definition 2.4.

Let $\Sigma$ be a graded set and $\mathbf{A}=(A,{[\\![-]\\!]}^{\mathbf{A}})$
be a $\Sigma$-algebra. We define the interpretation
${[\\![-]\\!]^{\prime}}^{\mathbf{A}}$ of $\Sigma$-terms recursively as
follows.

  1. (1)

For each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$,

${[\\![x^{(n)}_{i}]\\!]^{\prime}}^{\mathbf{A}}\colon A^{n}\longrightarrow A$

is the $i$-th projection $(a_{1},\dots,a_{n})\longmapsto a_{i}$.

  2. (2)

For each $n,k\in\mathbb{N}$, $\sigma\in\Sigma_{k}$ and $t_{1}\dots,t_{k}\in
T(\Sigma)_{n}$,

${[\\![\sigma(t_{1},\dots,t_{k})]\\!]^{\prime}}^{\mathbf{A}}\colon
A^{n}\longrightarrow A$

maps $(a_{1},\dots,a_{n})\in A^{n}$ to
${[\\![\sigma]\\!]}^{\mathbf{A}}({[\\![t_{1}]\\!]^{\prime}}^{\mathbf{A}}(a_{1},\dots,a_{n}),\dots,{[\\![t_{k}]\\!]^{\prime}}^{\mathbf{A}}(a_{1},\dots,a_{n}))$;
that is, the function
${[\\![\sigma(t_{1},\dots,t_{k})]\\!]^{\prime}}^{\mathbf{A}}$ is the following
composite:

$A^{n}$$A^{k}$$A.$$\langle{[\\![t_{1}]\\!]^{\prime}}^{\mathbf{A}},\dots,{[\\![t_{k}]\\!]^{\prime}}^{\mathbf{A}}\rangle$${[\\![\sigma]\\!]}^{\mathbf{A}}$

Note that for any $n\in\mathbb{N}$ and $\sigma\in\Sigma_{n}$,
${[\\![\sigma]\\!]}^{\mathbf{A}}={[\\![\sigma(x^{(n)}_{1},\dots,x^{(n)}_{n})]\\!]^{\prime}}^{\mathbf{A}}$.
Henceforth, for any $\Sigma$-term $t$ we simply write
${[\\![t]\\!]}^{\mathbf{A}}$ for ${[\\![t]\\!]^{\prime}}^{\mathbf{A}}$ defined
above.

######  Definition 2.5.

Let $\Sigma$ be a graded set. An element of the graded set $T(\Sigma)\times
T(\Sigma)$ is called a $\Sigma$-equation. We write a $\Sigma$-equation
$(n,(t,s))\in T(\Sigma)\times T(\Sigma)$ (that is, $n\in\mathbb{N}$ and
$t,s\in T(\Sigma)_{n}$) as $t\approx_{n}s$ or $t\approx s$.

######  Definition 2.6.

A presentation of an equational theory ${{\langle\,\Sigma\,|\,E\,\rangle}}$ is
a pair consisting of:

  * •

a graded set $\Sigma$ of basic operations, and

  * •

a graded set $E\subseteq T(\Sigma)\times T(\Sigma)$ of equational axioms.

######  Definition 2.7.

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory.

  1. (1)

A model of ${{\langle\,\Sigma\,|\,E\,\rangle}}$, or a
${{\langle\,\Sigma\,|\,E\,\rangle}}$-model, is a $\Sigma$-algebra $\mathbf{A}$
such that for any $t\approx_{n}s\in E$,
${[\\![t]\\!]}^{\mathbf{A}}={[\\![s]\\!]}^{\mathbf{A}}$ holds.

  2. (2)

A homomorphism between models of ${{\langle\,\Sigma\,|\,E\,\rangle}}$ is just
a $\Sigma$-homomorphism between the corresponding $\Sigma$-algebras.

Consider the presentation of an equational theory
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$, where

$E^{\mathrm{Grp}}_{1}=\\{\,m(x^{(1)}_{1},e)\approx x^{(1)}_{1},\quad
m(x^{(1)}_{1},i(x^{(1)}_{1}))\approx e\,\\},$
$E^{\mathrm{Grp}}_{3}=\\{\,m(m(x^{(3)}_{1},x^{(3)}_{2}),x^{(3)}_{3})\approx
m(x^{(3)}_{1},m(x^{(3)}_{2},x^{(3)}_{3}))\,\\}$

and $E^{\mathrm{Grp}}_{n}=\emptyset$ for all
$n\in\mathbb{N}\setminus\\{1,3\\}$. Clearly, groups are the same as models of
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$. Many other
types of algebras—indeed all examples we have mentioned in the first paragraph
of the introduction—can be written as models of
${{\langle\,\Sigma\,|\,E\,\rangle}}$ for a suitable choice of the presentation
of an equational theory ${{\langle\,\Sigma\,|\,E\,\rangle}}$ (see e.g.,
[BS81]).

We now describe the machinery of _equational logic_ , which enables us to
investigate consequences of equational axioms without referring to their
models. We assume that the reader is familiar with the basics of mathematical
logic, such as substitution of a term $t$ for a variable $x$ in a term $s$
(written as $s[x\mapsto t]$), simultaneous substitution (written as
$s[x_{1}\mapsto t_{1},\dots,x_{k}\mapsto t_{k}]$), and the notion of proof
(tree) and its definition by inference rules.

######  Definition 2.8.

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory.

  1. (1)

Define the set of ${{\langle\,\Sigma\,|\,E\,\rangle}}$-proofs inductively by
the following inference rules. Every
${{\langle\,\Sigma\,|\,E\,\rangle}}$-proof is a finite rooted tree whose
vertices are labelled by $\Sigma$-equations.

(Ax)  (if $t\approx_{n}s\in E$) $t\approx_{n}s$

(Refl)  $t\approx_{n}t$ $t\approx_{n}s$ (Sym)  $s\approx_{n}t$ $t\approx_{n}s$
$s\approx_{n}u$ (Trans)  $t\approx_{n}u$

$s\approx_{k}s^{\prime}$ $t_{1}\approx_{n}t^{\prime}_{1}$ $\cdots$
$t_{k}\approx_{n}t^{\prime}_{k}$ (Cong)  $s[x^{(k)}_{1}\mapsto
t_{1},\dots,x^{(k)}_{k}\mapsto t_{k}]\approx_{n}s^{\prime}[x^{(k)}_{1}\mapsto
t^{\prime}_{1},\dots,x^{(k)}_{k}\mapsto t^{\prime}_{k}]$

  2. (2)

A $\Sigma$-equation $t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$ is called an
equational theorem of ${{\langle\,\Sigma\,|\,E\,\rangle}}$ iff there exists a
${{\langle\,\Sigma\,|\,E\,\rangle}}$-proof whose root is labelled by
$t\approx_{n}s$. We write

${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$

to mean that $t\approx_{n}s$ is an equational theorem of
${{\langle\,\Sigma\,|\,E\,\rangle}}$, and denote by $\overline{E}\subseteq
T(\Sigma)\times T(\Sigma)$ the graded set of all equational theorems of
${{\langle\,\Sigma\,|\,E\,\rangle}}$.

The assertion ${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx s$ says that
the $\Sigma$-equation $t\approx s$ is a _syntactic_ consequence of the
equational axioms ${E}$. Its counterpart is the _semantic_ consequence
relation $\vDash$, defined as follows.

######  Definition 2.9.

  1. (1)

Let $\Sigma$ be a graded set and $\mathbf{A}$ be a $\Sigma$-algebra. For any
$\Sigma$-equation $t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$, we write

$\mathbf{A}\vDash t\approx_{n}s$

to mean ${[\\![t]\\!]}^{\mathbf{A}}={[\\![s]\\!]}^{\mathbf{A}}$.

  2. (2)

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory. For any $\Sigma$-equation $t\approx_{n}s\in T(\Sigma)\times
T(\Sigma)$, we write

${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash t\approx_{n}s$

to mean that for any ${{\langle\,\Sigma\,|\,E\,\rangle}}$-model $\mathbf{A}$,
$\mathbf{A}\vDash t\approx_{n}s$.

Equational logic is known to be both _sound_ and _complete_ , meaning that the
two relations $\vdash$ and $\vDash$ coincide.

######  Theorem 2.10.

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory.

  1. (1)

(Soundness) Let $t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$. If
${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$ then
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash t\approx_{n}s$.

  2. (2)

(Completeness) Let $t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$. If
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash t\approx_{n}s$ then
${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$.

###### Proof.

The soundness theorem can be shown by a straightforward induction over
${{\langle\,\Sigma\,|\,E\,\rangle}}$-proofs.

To prove the completeness theorem, first observe that the graded set
$\overline{E}\subseteq T(\Sigma)\times T(\Sigma)$ of all equational theorems
of ${{\langle\,\Sigma\,|\,E\,\rangle}}$ (Definition 2.8) is an equivalece
relation on $T(\Sigma)$, thanks to the rules (Refl), (Sym) and (Trans). Hence
we can consider the quotient graded set $T(\Sigma)/\overline{E}$. We claim
that for each $n\in\mathbb{N}$, the set
$T^{{{\langle\,\Sigma\,|\,E\,\rangle}}}_{n}=(T(\Sigma)/\overline{E})_{n}$ has
a natural structure of ${{\langle\,\Sigma\,|\,E\,\rangle}}$-model.

We start with endowing a $\Sigma$-algebra structure on the set
$T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$; that is, we define for each
$k\in\mathbb{N}$ and each $\sigma\in\Sigma_{k}$, its interpretation
${[\\![\sigma]\\!]}\colon(T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n})^{k}\longrightarrow
T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$. This is defined as

${[\\![\sigma]\\!]}([t_{1}]_{\overline{E}},\dots,[t_{k}]_{\overline{E}})=[\sigma(t_{1},\dots,t_{k})]_{\overline{E}}$

for each $t_{1},\dots,t_{k}\in T(\Sigma)_{n}$. To see that it is indeed well-
defined, consider the instances of the (Cong) rule where
$s=s^{\prime}=\sigma(x^{(k)}_{1},\dots,x^{(k)}_{k})$. Observe that in this
$\Sigma$-algebra, the interpretation of a $\Sigma$-term $s\in T(\Sigma)_{k}$
is given by

${[\\![s]\\!]}([t_{1}]_{\overline{E}},\dots,[t_{k}]_{\overline{E}})=[s[x^{(k)}_{1}\mapsto
t_{1},\dots,x^{(k)}_{k}\mapsto t_{k}]]_{\overline{E}}.$

The $\Sigma$-algebra
$\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}=(T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n},{[\\![-]\\!]})$
satisfies all equational axioms of ${{\langle\,\Sigma\,|\,E\,\rangle}}$. To
see this, notice that if $s\approx_{k}s^{\prime}\in E$, then for each
$t_{1},\dots,t_{k}\in T(\Sigma)_{n}$, the $\Sigma$-equation
$s[x^{(k)}_{1}\mapsto t_{1},\dots,x^{(k)}_{k}\mapsto
t_{k}]\approx_{n}s^{\prime}[x^{(k)}_{1}\mapsto t_{1},\dots,x^{(k)}_{k}\mapsto
t_{k}]$ is an equational theorem of ${{\langle\,\Sigma\,|\,E\,\rangle}}$, by
the rules (Ax), (Refl) and (Cong). Hence
${[\\![s]\\!]}={[\\![s^{\prime}]\\!]}$ holds in
$\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$.

Now suppose that for a $\Sigma$-equation $t\approx_{n}s$ we have
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash t\approx_{n}s$. Then in particular
$\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}\vDash t\approx_{n}s$, and
in particular the images of
$[x^{(n)}_{1}]_{\overline{E}},\dots,[x^{(n)}_{n}]_{\overline{E}}\in
T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$ under the functions ${[\\![t]\\!]}$
and ${[\\![s]\\!]}$ agree. Hence we have

$\displaystyle[t]_{\overline{E}}$ $\displaystyle=[t[x^{(n)}_{1}\mapsto
x^{(n)}_{1},\dots,x^{(n)}_{n}\mapsto x^{(n)}_{n}]]_{\overline{E}}$
$\displaystyle={[\\![t]\\!]}([x^{(n)}_{1}]_{\overline{E}},\dots,[x^{(n)}_{n}]_{\overline{E}})$
$\displaystyle={[\\![s]\\!]}([x^{(n)}_{1}]_{\overline{E}},\dots,[x^{(n)}_{n}]_{\overline{E}})$
$\displaystyle=[s[x^{(n)}_{1}\mapsto x^{(n)}_{1},\dots,x^{(n)}_{n}\mapsto
x^{(n)}_{n}]]_{\overline{E}}$ $\displaystyle=[s]_{\overline{E}},$

namely ${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$. ∎

Before closing this section, we remark that the
${{\langle\,\Sigma\,|\,E\,\rangle}}$-model
$\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$ used in the above proof is
in fact the _free ${{\langle\,\Sigma\,|\,E\,\rangle}}$-model generated by the
$n$-element set $X_{n}=\\{x^{(n)}_{1},\dots,x^{(n)}_{n}\\}$_, in the following
sense.

######  Proposition 2.11.

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory and $n$ be a natural number. Define the function $\eta_{X_{n}}\colon
X_{n}\longrightarrow T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$ by
$\eta_{X_{n}}(x^{(n)}_{i})=[x^{(n)}_{i}]_{\overline{E}}$ for each
$i\in\\{1,\dots,n\\}$. Given any ${{\langle\,\Sigma\,|\,E\,\rangle}}$-model
$\mathbf{A}=(A,{[\\![-]\\!]})$ and any function $f\colon X_{n}\longrightarrow
A$, there exists a unique homomorphism of
${{\langle\,\Sigma\,|\,E\,\rangle}}$-models
$g\colon\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}\longrightarrow\mathbf{A}$
such that $g\circ\eta_{X_{n}}=f$.

$X_{n}$$T^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$$A$(sets)$\eta_{X_{n}}$$g$$f$
$\mathbf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}_{n}$$\mathbf{A}$(${{\langle\,\Sigma\,|\,E\,\rangle}}$-models)$g$

###### Proof.

The required homomorphism $g$ can be defined from $f$ by recursion; the
details are omitted. ∎

##  3\. Clones

The central notion we have introduced in the previous section is that of
_presentation of an equational theory_ (Definition 2.6), whose main purpose is
to define its _models_ (Definition 2.7). It can happen, however, that two
different presentations of equational theories define the “same” models,
sometimes in a quite superficial manner.

For example, consider the following presentation of an equational theory
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime}}\,|\,E^{\mathrm{Grp}^{\prime}}\,\rangle}}$:

$\Sigma^{\mathrm{Grp}^{\prime}}=\Sigma^{\mathrm{Grp}},$
$E^{\mathrm{Grp}^{\prime}}_{1}=\\{\,m(x^{(1)}_{1},e)\approx x^{(1)}_{1},\quad
m(e,x^{(1)}_{1})\approx x^{(1)}_{1},\\\ m(x^{(1)}_{1},i(x^{(1)}_{1}))\approx
e,\quad m(i(x^{(1)}_{1}),x^{(1)}_{1})\approx e\,\\},$
$E^{\mathrm{Grp}^{\prime}}_{n}=E^{\mathrm{Grp}}_{n}\quad\text{ for all
}n\in\mathbb{N}\setminus\\{1\\}.$

It is a classical fact that a group can be defined either as a model of
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$ or as a
model of
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime}}\,|\,E^{\mathrm{Grp}^{\prime}}\,\rangle}}$.
Indeed, we may add arbitrary equational theorems of
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$, such as
$i(i(x_{1}))\approx x_{1}$, $i(m(x_{1},x_{2}))\approx m(i(x_{2}),i(x_{1}))$
and $x_{1}\approx x_{1}$, as additional equational axioms and still obtain the
groups as the models.

As another example, let us consider the presentation of an equational theory
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime\prime}}\,|\,E^{\mathrm{Grp}^{\prime\prime}}\,\rangle}}$
defined as:

$\Sigma^{\mathrm{Grp}^{\prime\prime}}_{0}=\\{e,e^{\prime}\\},\quad\Sigma^{\mathrm{Grp}^{\prime\prime}}_{n}=\Sigma^{\mathrm{Grp}}_{n}\quad\text{
for all }n\in\mathbb{N}\setminus\\{0\\},$
$E^{\mathrm{Grp}^{\prime\prime}}_{0}=\\{e\approx e^{\prime}\\},\quad
E^{\mathrm{Grp}^{\prime\prime}}_{n}=E^{\mathrm{Grp}}_{n}\quad\text{ for all
}n\in\mathbb{N}\setminus\\{0\\}.$

To make a set $A$ into a model of
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime\prime}}\,|\,E^{\mathrm{Grp}^{\prime\prime}}\,\rangle}}$,
formally we have to specify two elements ${[\\![e]\\!]}$ and
${[\\![e^{\prime}]\\!]}$ of $A$, albeit they are forced to be equal and play
the role of unit with respect to the group structure determined by
${[\\![m]\\!]}$. We cannot quite say that models of
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime\prime}}\,|\,E^{\mathrm{Grp}^{\prime\prime}}\,\rangle}}$
are _equal_ to models of
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$, since
their data differ; however, it should be intuitively clear that there is no
point in distinguishing them.444In precise mathematical terms, our claim of
the “sameness” amounts to the existence of an isomorphism of categories
between the categories of
${{\langle\,\Sigma^{\mathrm{Grp}}\,|\,E^{\mathrm{Grp}}\,\rangle}}$-models and
of
${{\langle\,\Sigma^{\mathrm{Grp}^{\prime\prime}}\,|\,E^{\mathrm{Grp}^{\prime\prime}}\,\rangle}}$-models
preserving the underlying sets of models, i.e., commuting with the forgetful
functors into the category $\mathbf{Set}$ of sets.

A presentation of an equational theory has much freedom in choices both of
basic operations and of equational axioms. It is really a _presentation_. In
fact, there is a notion which may be thought of as an _equational theory_
itself, something that a presentation of an equational theory presents; it is
called an _(abstract) clone_ (see e.g., [Tay93]).

######  Definition 3.1.

A clone $\mathsf{T}$ consists of:

(CD1):

a graded set $T=(T_{n})_{n\in\mathbb{N}}$;555In traditional universal algebra,
people often omit $T_{0}$.

(CD2):

for each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$, an element

$p^{(n)}_{i}\in T_{n};$

(CD3):

for each $k,n\in\mathbb{N}$, a function

$\circ^{(n)}_{k}\colon T_{k}\times(T_{n})^{k}\longrightarrow T_{n}$

whose action on an element $(\phi,\theta_{1},\dots,\theta_{k})\in
T_{k}\times(T_{n})^{k}$ we write as
$\phi\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k})$ or simply as
$\phi\circ(\theta_{1},\dots,\theta_{k})$;

satisfying the following equations:

(CA1):

for each $k,n\in\mathbb{N}$, $j\in\\{1,\dots,k\\}$ and
$\theta_{1},\dots,\theta_{k}\in T_{n}$,

$p^{(k)}_{j}\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k})=\theta_{j};$

(CA2):

for each $n\in\mathbb{N}$, $\theta\in T_{n}$,

$\theta\circ^{(n)}_{n}(p^{(n)}_{1},\dots,p^{(n)}_{n})=\theta;$

(CA3):

for each $l,k,n\in\mathbb{N}$, $\psi\in T_{l}$, $\phi_{1},\dots,\phi_{l}\in
T_{k}$, $\theta_{1},\dots,\theta_{k}\in T_{n}$,

$\psi\circ^{(k)}_{l}\big{(}\phi_{1}\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k}),\
\dots,\ \phi_{l}\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k})\big{)}\\\
=\big{(}\psi\circ^{(k)}_{l}(\phi_{1},\dots,\phi_{l})\big{)}\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k}).$

Such a clone is written as
$\mathsf{T}=(T,(p^{(i)}_{n})_{n\in\mathbb{N},i\in\\{1,\dots,n\\}},(\circ^{(n)}_{k})_{k,n\in\mathbb{N}})$
or simply $(T,p,\circ)$.

To understand the definition of clone, it is helpful to look at some pictures
known as _string diagrams_ (cf. [Cur12, Lei04]). Given a clone
$\mathsf{T}=(T,p,\circ)$, let us draw an element $\theta$ of $T_{n}$ as a
triangle with $n$ “input wires” and a single “output wire”:

$\theta$ . . . $n$ (1)

The element $p^{(n)}_{i}$ in (CD2) may also be denoted by

. . . . . . $(i\text{-th})$$n$

and $\phi\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k})$ in (CD3) by

$\leavevmode\hbox to202.36pt{\vbox
to134.95pt{\pgfpicture\makeatletter\hbox{\hskip
142.00714pt\lower-67.47623pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}
{}{}{{}} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{42.67914pt}\pgfsys@lineto{0.0pt}{-42.67914pt}\pgfsys@lineto{42.67914pt}{0.0pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.24721pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\phi$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}{}}{{}}{}
{{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{42.67914pt}\pgfsys@moveto{0.0pt}{34.14323pt}\pgfsys@lineto{-17.07182pt}{34.14323pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.20256pt}{-30.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vbox{
\kern-1.0pt\hbox{.}\hbox{.}\hbox{.} }$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}{{}}{}{{}{}}{{}}{} {{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-42.67914pt}\pgfsys@moveto{0.0pt}{-34.14323pt}\pgfsys@lineto{-17.07182pt}{-34.14323pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{}}{}{{}}{}
{{}{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{42.67914pt}{0.0pt}\pgfsys@lineto{59.75096pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}
{}{}{{}} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-59.75096pt}{56.9055pt}\pgfsys@lineto{-59.75096pt}{11.38094pt}\pgfsys@lineto{-17.07182pt}{34.14322pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-49.2718pt}{31.57323pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\theta_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-47.19124pt}{-30.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vbox{
\kern-1.0pt\hbox{.}\hbox{.}\hbox{.} }$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-69.95352pt}{4.14322pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vbox{
\kern-1.0pt\hbox{.}\hbox{.}\hbox{.} }$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}{}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{{}}
{}{}{{}} {}{} {}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-59.75096pt}{-11.38094pt}\pgfsys@lineto{-59.75096pt}{-56.9055pt}\pgfsys@lineto{-17.07182pt}{-34.14322pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-49.41763pt}{-36.64322pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\theta_{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-69.95352pt}{-64.14322pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vbox{
\kern-1.0pt\hbox{.}\hbox{.}\hbox{.} }$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{-94.61829pt}{14.22638pt}\pgfsys@curveto{-94.61829pt}{15.39796pt}{-95.56804pt}{16.34772pt}{-96.73962pt}{16.34772pt}\pgfsys@curveto{-97.91121pt}{16.34772pt}{-98.86096pt}{15.39796pt}{-98.86096pt}{14.22638pt}\pgfsys@curveto{-98.86096pt}{13.0548pt}{-97.91121pt}{12.10504pt}{-96.73962pt}{12.10504pt}\pgfsys@curveto{-95.56804pt}{12.10504pt}{-94.61829pt}{13.0548pt}{-94.61829pt}{14.22638pt}\pgfsys@closepath\pgfsys@moveto{-96.73962pt}{14.22638pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-96.73962pt}{14.22638pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{-94.61829pt}{-14.22638pt}\pgfsys@curveto{-94.61829pt}{-13.0548pt}{-95.56804pt}{-12.10504pt}{-96.73962pt}{-12.10504pt}\pgfsys@curveto{-97.91121pt}{-12.10504pt}{-98.86096pt}{-13.0548pt}{-98.86096pt}{-14.22638pt}\pgfsys@curveto{-98.86096pt}{-15.39796pt}{-97.91121pt}{-16.34772pt}{-96.73962pt}{-16.34772pt}\pgfsys@curveto{-95.56804pt}{-16.34772pt}{-94.61829pt}{-15.39796pt}{-94.61829pt}{-14.22638pt}\pgfsys@closepath\pgfsys@moveto{-96.73962pt}{-14.22638pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-96.73962pt}{-14.22638pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-116.65648pt}{14.22638pt}\pgfsys@lineto{-99.58464pt}{14.22638pt}\pgfsys@curveto{-88.20372pt}{14.22638pt}{-85.35826pt}{48.3696pt}{-76.82278pt}{48.3696pt}\pgfsys@lineto{-59.75096pt}{48.3696pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-116.65648pt}{14.22638pt}\pgfsys@lineto{-99.58464pt}{14.22638pt}\pgfsys@curveto{-88.20372pt}{14.22638pt}{-85.35826pt}{-19.91684pt}{-76.82278pt}{-19.91684pt}\pgfsys@lineto{-59.75096pt}{-19.91684pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-116.65648pt}{-14.22638pt}\pgfsys@lineto{-99.58464pt}{-14.22638pt}\pgfsys@curveto{-88.20372pt}{-14.22638pt}{-85.35826pt}{19.91684pt}{-76.82278pt}{19.91684pt}\pgfsys@lineto{-59.75096pt}{19.91684pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-116.65648pt}{-14.22638pt}\pgfsys@lineto{-99.58464pt}{-14.22638pt}\pgfsys@curveto{-88.20372pt}{-14.22638pt}{-85.35826pt}{-48.3696pt}{-76.82278pt}{-48.3696pt}\pgfsys@lineto{-59.75096pt}{-48.3696pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-109.78722pt}{-30.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\vbox{
\kern-1.0pt\hbox{.}\hbox{.}\hbox{.} }$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{} {}{}{}{}{{{}{}}}{{}} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}}
}}{{}} {} {}{}{} { {{}} {} {}{}{} {}{}{} } { {{}} {} {}{}{} }
}{{}{}}{{}{}}{{{{}{}{{}} }}{{}}}
{}\pgfsys@moveto{-122.34694pt}{-19.91684pt}\pgfsys@moveto{-122.34694pt}{-19.91684pt}\pgfsys@curveto{-123.84695pt}{-19.16687pt}{-124.84694pt}{-17.41684pt}{-124.84694pt}{-14.91684pt}\pgfsys@lineto{-124.84694pt}{-5.0pt}\pgfsys@curveto{-124.84694pt}{-2.5pt}{-125.84692pt}{-0.74997pt}{-127.34694pt}{0.0pt}\pgfsys@curveto{-125.84692pt}{0.74997pt}{-124.84694pt}{2.5pt}{-124.84694pt}{5.0pt}\pgfsys@lineto{-124.84694pt}{14.91684pt}\pgfsys@curveto{-124.84694pt}{17.41684pt}{-123.84695pt}{19.16687pt}{-122.34694pt}{19.91684pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-138.67413pt}{-1.50694pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\scriptsize{$n$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ .$

Then the axioms (CA1)–(CA3) simply assert obvious equations between the
resulting “circuits”. For instance, (CA2) for $n=3$ reads:

$\leavevmode\hbox to191.83pt{\vbox
to86.56pt{\pgfpicture\makeatletter\hbox{\hskip 0.59999pt\lower-43.27913pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}{{}}{}{{}}{}{}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{8.5359pt}\pgfsys@lineto{17.07182pt}{8.5359pt}\pgfsys@curveto{25.6073pt}{8.5359pt}{34.14322pt}{42.67914pt}{42.67914pt}{42.67914pt}\pgfsys@lineto{88.20372pt}{42.67914pt}\pgfsys@curveto{96.7392pt}{42.67914pt}{105.27512pt}{8.5359pt}{113.81104pt}{8.5359pt}\pgfsys@lineto{130.88286pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{17.07182pt}{0.0pt}\pgfsys@curveto{25.6073pt}{0.0pt}{34.14322pt}{34.14322pt}{42.67914pt}{34.14322pt}\pgfsys@lineto{56.90552pt}{34.14322pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-8.5359pt}\pgfsys@lineto{17.07182pt}{-8.5359pt}\pgfsys@curveto{25.6073pt}{-8.5359pt}{34.14322pt}{25.6073pt}{42.67914pt}{25.6073pt}\pgfsys@lineto{56.90552pt}{25.6073pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{8.5359pt}\pgfsys@lineto{56.90552pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{130.88286pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-8.5359pt}\pgfsys@lineto{56.90552pt}{-8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}{{}}{}{{}}{}{}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-8.5359pt}\pgfsys@lineto{17.07182pt}{-8.5359pt}\pgfsys@curveto{25.6073pt}{-8.5359pt}{34.14322pt}{-42.67914pt}{42.67914pt}{-42.67914pt}\pgfsys@lineto{88.20372pt}{-42.67914pt}\pgfsys@curveto{96.7392pt}{-42.67914pt}{105.27512pt}{-8.5359pt}{113.81104pt}{-8.5359pt}\pgfsys@lineto{130.88286pt}{-8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{17.07182pt}{0.0pt}\pgfsys@curveto{25.6073pt}{0.0pt}{34.14322pt}{-34.14322pt}{42.67914pt}{-34.14322pt}\pgfsys@lineto{56.90552pt}{-34.14322pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}{{}}{}{{}}{}{}{} {}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{8.5359pt}\pgfsys@lineto{17.07182pt}{8.5359pt}\pgfsys@curveto{25.6073pt}{8.5359pt}{34.14322pt}{-25.6073pt}{42.67914pt}{-25.6073pt}\pgfsys@lineto{56.90552pt}{-25.6073pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{34.14322pt}\pgfsys@curveto{59.02686pt}{35.3148pt}{58.0771pt}{36.26456pt}{56.90552pt}{36.26456pt}\pgfsys@curveto{55.73393pt}{36.26456pt}{54.78418pt}{35.3148pt}{54.78418pt}{34.14322pt}\pgfsys@curveto{54.78418pt}{32.97163pt}{55.73393pt}{32.02188pt}{56.90552pt}{32.02188pt}\pgfsys@curveto{58.0771pt}{32.02188pt}{59.02686pt}{32.97163pt}{59.02686pt}{34.14322pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{34.14322pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{34.14322pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{25.6073pt}\pgfsys@curveto{59.02686pt}{26.77888pt}{58.0771pt}{27.72864pt}{56.90552pt}{27.72864pt}\pgfsys@curveto{55.73393pt}{27.72864pt}{54.78418pt}{26.77888pt}{54.78418pt}{25.6073pt}\pgfsys@curveto{54.78418pt}{24.43571pt}{55.73393pt}{23.48596pt}{56.90552pt}{23.48596pt}\pgfsys@curveto{58.0771pt}{23.48596pt}{59.02686pt}{24.43571pt}{59.02686pt}{25.6073pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{25.6073pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{25.6073pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{8.5359pt}\pgfsys@curveto{59.02686pt}{9.70749pt}{58.0771pt}{10.65724pt}{56.90552pt}{10.65724pt}\pgfsys@curveto{55.73393pt}{10.65724pt}{54.78418pt}{9.70749pt}{54.78418pt}{8.5359pt}\pgfsys@curveto{54.78418pt}{7.36432pt}{55.73393pt}{6.41457pt}{56.90552pt}{6.41457pt}\pgfsys@curveto{58.0771pt}{6.41457pt}{59.02686pt}{7.36432pt}{59.02686pt}{8.5359pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{8.5359pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{8.5359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{-8.5359pt}\pgfsys@curveto{59.02686pt}{-7.36432pt}{58.0771pt}{-6.41457pt}{56.90552pt}{-6.41457pt}\pgfsys@curveto{55.73393pt}{-6.41457pt}{54.78418pt}{-7.36432pt}{54.78418pt}{-8.5359pt}\pgfsys@curveto{54.78418pt}{-9.70749pt}{55.73393pt}{-10.65724pt}{56.90552pt}{-10.65724pt}\pgfsys@curveto{58.0771pt}{-10.65724pt}{59.02686pt}{-9.70749pt}{59.02686pt}{-8.5359pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{-8.5359pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{-8.5359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{-25.6073pt}\pgfsys@curveto{59.02686pt}{-24.43571pt}{58.0771pt}{-23.48596pt}{56.90552pt}{-23.48596pt}\pgfsys@curveto{55.73393pt}{-23.48596pt}{54.78418pt}{-24.43571pt}{54.78418pt}{-25.6073pt}\pgfsys@curveto{54.78418pt}{-26.77888pt}{55.73393pt}{-27.72864pt}{56.90552pt}{-27.72864pt}\pgfsys@curveto{58.0771pt}{-27.72864pt}{59.02686pt}{-26.77888pt}{59.02686pt}{-25.6073pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{-25.6073pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{-25.6073pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{59.02686pt}{-34.14322pt}\pgfsys@curveto{59.02686pt}{-32.97163pt}{58.0771pt}{-32.02188pt}{56.90552pt}{-32.02188pt}\pgfsys@curveto{55.73393pt}{-32.02188pt}{54.78418pt}{-32.97163pt}{54.78418pt}{-34.14322pt}\pgfsys@curveto{54.78418pt}{-35.3148pt}{55.73393pt}{-36.26456pt}{56.90552pt}{-36.26456pt}\pgfsys@curveto{58.0771pt}{-36.26456pt}{59.02686pt}{-35.3148pt}{59.02686pt}{-34.14322pt}\pgfsys@closepath\pgfsys@moveto{56.90552pt}{-34.14322pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{56.90552pt}{-34.14322pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{22.03818pt}{8.5359pt}\pgfsys@curveto{22.03818pt}{9.70749pt}{21.08842pt}{10.65724pt}{19.91684pt}{10.65724pt}\pgfsys@curveto{18.74525pt}{10.65724pt}{17.7955pt}{9.70749pt}{17.7955pt}{8.5359pt}\pgfsys@curveto{17.7955pt}{7.36432pt}{18.74525pt}{6.41457pt}{19.91684pt}{6.41457pt}\pgfsys@curveto{21.08842pt}{6.41457pt}{22.03818pt}{7.36432pt}{22.03818pt}{8.5359pt}\pgfsys@closepath\pgfsys@moveto{19.91684pt}{8.5359pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91684pt}{8.5359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{22.03818pt}{0.0pt}\pgfsys@curveto{22.03818pt}{1.17159pt}{21.08842pt}{2.12134pt}{19.91684pt}{2.12134pt}\pgfsys@curveto{18.74525pt}{2.12134pt}{17.7955pt}{1.17159pt}{17.7955pt}{0.0pt}\pgfsys@curveto{17.7955pt}{-1.17159pt}{18.74525pt}{-2.12134pt}{19.91684pt}{-2.12134pt}\pgfsys@curveto{21.08842pt}{-2.12134pt}{22.03818pt}{-1.17159pt}{22.03818pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{19.91684pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91684pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{22.03818pt}{-8.5359pt}\pgfsys@curveto{22.03818pt}{-7.36432pt}{21.08842pt}{-6.41457pt}{19.91684pt}{-6.41457pt}\pgfsys@curveto{18.74525pt}{-6.41457pt}{17.7955pt}{-7.36432pt}{17.7955pt}{-8.5359pt}\pgfsys@curveto{17.7955pt}{-9.70749pt}{18.74525pt}{-10.65724pt}{19.91684pt}{-10.65724pt}\pgfsys@curveto{21.08842pt}{-10.65724pt}{22.03818pt}{-9.70749pt}{22.03818pt}{-8.5359pt}\pgfsys@closepath\pgfsys@moveto{19.91684pt}{-8.5359pt}\pgfsys@fillstroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.91684pt}{-8.5359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{130.88286pt}{19.91684pt}\pgfsys@lineto{130.88286pt}{-19.91684pt}\pgfsys@lineto{173.562pt}{0.0pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{142.76202pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\theta$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{173.562pt}{0.0pt}\pgfsys@lineto{190.63339pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ =\ \leavevmode\hbox
to78.02pt{\vbox to41.03pt{\pgfpicture\makeatletter\hbox{\hskip
0.59999pt\lower-20.51683pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{8.5359pt}\pgfsys@lineto{17.07182pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{17.07182pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{-8.5359pt}\pgfsys@lineto{17.07182pt}{-8.5359pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\par{}{{}}{} {}{} {}{}
{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{19.91684pt}\pgfsys@lineto{17.07182pt}{-19.91684pt}\pgfsys@lineto{59.75096pt}{0.0pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{28.95099pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\theta$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{1.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{59.75096pt}{0.0pt}\pgfsys@lineto{76.82236pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\ .$

Next we define models of a clone. We first need a few preliminary definitions.

######  Definition 3.2.

Let $A$ be a set. Define the clone $\mathsf{End}(A)=({\langle
A,A\rangle},p,\circ)$ as follows:

(CD1):

for each $n\in\mathbb{N}$, let ${\langle A,A\rangle}_{n}$ be the set of all
functions from $A^{n}$ to $A$;

(CD2):

for each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$, let $p^{(n)}_{i}$ be the
$i$-th projection $A^{n}\longrightarrow A$, $(a_{1},\dots,a_{n})\longmapsto
a_{i}$;

(CD3):

for each $k,n\in\mathbb{N}$, $g\colon A^{k}\longrightarrow A$ and
$f_{1},\dots,f_{k}\colon A^{n}\longrightarrow A$, let
$g\circ^{(n)}_{k}(f_{1},\dots,f_{k})$ be the function
$(a_{1},\dots,a_{n})\longmapsto
g(f_{1}(a_{1},\dots,a_{n}),\dots,f_{k}(a_{1},\dots,a_{n}))$, that is, the
following composite:

$A^{n}$$A^{k}$$A.$$\langle f_{1},\dots,f_{k}\rangle$$g$

It is straightforward to check the axioms (CA1)–(CA3).

######  Definition 3.3.

Let $\mathsf{T}=(T,p,\circ)$ and
$\mathsf{T^{\prime}}=(T^{\prime},p^{\prime},\circ^{\prime})$ be clones. A
clone homomorphism from $\mathsf{T}$ to $\mathsf{T^{\prime}}$ is a morphism of
graded sets (Definition 2.1) $h\colon T\longrightarrow T^{\prime}$ which
preserves the structure of clones; precisely,

  * •

for each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$,
$h_{n}(p^{(n)}_{i})=p^{\prime(n)}_{i}$;

  * •

for each $k,n\in\mathbb{N}$, $\phi\in T_{k}$ and
$\theta_{1},\dots,\theta_{k}\in T_{n}$,

$h_{n}\big{(}\phi\circ^{(n)}_{k}(\theta_{1},\dots,\theta_{k})\big{)}=h_{k}(\phi)\circ^{\prime(n)}_{k}\big{(}h_{n}(\theta_{1}),\dots,h_{n}(\theta_{k})\big{)}.$

######  Definition 3.4.

Let $\mathsf{T}$ be a clone. A model of $\mathsf{T}$ is a pair
$\mathbf{A}=(A,\alpha)$ consisting of a set $A$ and a clone homomorphism
$\alpha\colon\mathsf{T}\longrightarrow\mathsf{End}(A)$.

Let us then define the notion of homomorphism between models. First we extend
the definition of the graded set ${\langle A,A\rangle}$ introduced in
Definition 3.2.

######  Definition 3.5.

  1. (1)

Let $A$ and $B$ be sets. The graded set ${\langle A,B\rangle}$ is defined by
setting, for each $n\in\mathbb{N}$, ${\langle A,B\rangle}_{n}$ be the set of
all functions from $A^{n}$ to $B$.

  2. (2)

Let $A,A^{\prime}$ and $B$ be sets and $f\colon A^{\prime}\longrightarrow A$
be a function. The morphism of graded sets ${\langle f,B\rangle}\colon{\langle
A,B\rangle}\longrightarrow{\langle A^{\prime},B\rangle}$ is defined by
setting, for each $n\in\mathbb{N}$, ${\langle f,B\rangle}_{n}\colon{\langle
A,B\rangle}_{n}\longrightarrow{\langle A^{\prime},B\rangle}_{n}$ be the
precomposition by $f^{n}\colon(A^{\prime})^{n}\longrightarrow A^{n}$; that is,
$h\longmapsto h\circ f^{n}$.

  3. (3)

Let $A,B$ and $B^{\prime}$ be sets and $g\colon B\longrightarrow B^{\prime}$
be a function. The morphism of graded sets ${\langle A,g\rangle}\colon{\langle
A,B\rangle}\longrightarrow{\langle A,B^{\prime}\rangle}$ is defined by
setting, for each $n\in\mathbb{N}$, ${\langle A,g\rangle}_{n}\colon{\langle
A,B\rangle}_{n}\longrightarrow{\langle A,B^{\prime}\rangle}_{n}$ be the
postcomposition by $g\colon B\longrightarrow B^{\prime}$; that is,
$h\longmapsto g\circ h$.

######  Definition 3.6.

Let $\mathsf{T}$ be a clone, and $\mathbf{A}=(A,\alpha)$ and
$\mathbf{B}=(B,\beta)$ be models of $\mathsf{T}$. A homomorphism from
$\mathbf{A}$ to $\mathbf{B}$ is a function $f\colon A\longrightarrow B$ making
the following diagram of morphisms of graded sets commute:

$T$${\langle A,A\rangle}$${\langle B,B\rangle}$${\langle
A,B\rangle}.$$\alpha$${\langle A,f\rangle}$$\beta$${\langle f,B\rangle}$

Now let us turn to the relation between presentations of equational theories
(Definition 2.6) and clones. We start with the observation that the graded set
$T(\Sigma)$ of $\Sigma$-terms (Definition 2.3) has a canonical clone
structure, given as follows:

(CD2):

for each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$, let $p^{(n)}_{i}$ be
$x^{(n)}_{i}\in T(\Sigma)_{n}$;

(CD3):

for each $k,n\in\mathbb{N}$, $s\in T(\Sigma)_{k}$ and $t_{1},\dots,t_{k}\in
T(\Sigma)_{n}$, let $s\circ^{(n)}_{k}(t_{1},\dots,t_{k})$ be
$s[x^{(k)}_{1}\mapsto t_{1},\dots,x^{(k)}_{k}\mapsto t_{k}]\in T(\Sigma)_{n}$.

We denote the resulting clone by $\mathsf{T}(\Sigma)$. In fact, this clone is
characterised as the _free clone generated by $\Sigma$_, in the following
sense.

######  Proposition 3.7.

Let $\Sigma$ be a graded set, and let
$\eta_{\Sigma}\colon\Sigma\longrightarrow T(\Sigma)$ be the morphism of graded
sets defined by
$(\eta_{\Sigma})_{n}(\sigma)=\sigma(x^{(n)}_{1},\dots,x^{(n)}_{n})$ for each
$n\in\mathbb{N}$ and $\sigma\in\Sigma_{n}$. Given any clone
$\mathsf{S}=(S,p,\circ)$ and any morphism of graded sets
$f\colon\Sigma\longrightarrow S$, there exists a unique clone homomorphism
$g\colon\mathsf{T}(\Sigma)\longrightarrow\mathsf{S}$ such that
$g\circ\eta_{\Sigma}=f$.

$\Sigma$${T}(\Sigma)$$S$(graded sets)$\eta_{\Sigma}$$g$$f$
$\mathsf{T}(\Sigma)$$\mathsf{S}$(clones)$g$

###### Proof.

The clone homomorphism $g$ may be defined by recursion (recall that
$T(\Sigma)$ was defined inductively) as follows:

  1. (1)

for each $n\in\mathbb{N}$ and $i\in\\{1,\dots,n\\}$, let

$g_{n}(x^{(n)}_{i})=p^{(n)}_{i};$

  2. (2)

for each $k,n\in\mathbb{N}$, $\sigma\in\Sigma_{k}$ and $t_{1},\dots,t_{k}\in
T(\Sigma)_{n}$, let

$g_{n}(\sigma(t_{1},\dots,t_{k}))=f_{k}(\sigma)\circ^{(n)}_{k}(g_{n}(t_{1}),\dots,g_{n}(t_{k})).$

To check that $g$ is indeed a clone homomorphism, it suffices to show for each
$s\in T(\Sigma)_{k}$ and $t_{1},\dots,t_{k}\in T(\Sigma)_{n}$,

$g_{n}(s[x^{(k)}_{1}\mapsto t_{1},\dots,x^{(k)}_{k}\mapsto
t_{k}])=g_{k}(s)\circ^{(n)}_{k}(g_{n}(t_{1}),\dots,g_{n}(t_{k}));$

this can be shown by induction on $s$. The uniqueness of $g$ is clear. ∎

The construction given in Definition 2.4 is a special case of the above; let
$\mathsf{S}$ be $\mathsf{End}(A)$.

Recall from Definition 2.8 the graded set $\overline{E}\subseteq
T(\Sigma)\times T(\Sigma)$ of equational theorems of a presentation of an
equational theory ${{\langle\,\Sigma\,|\,E\,\rangle}}$. The graded set
$\overline{E}$ is an equivalence relation on $T(\Sigma)$, and hence we may
consider the quotient graded set $T(\Sigma)/\overline{E}$ (as we did in the
proof of Theorem 2.10). By the rule (Cong), the clone operations on
$T(\Sigma)$ induce well-defined operations on $T(\Sigma)/\overline{E}$; that
is, $\overline{E}$ is not only an equivalence relation on the graded set
$T(\Sigma)$, but it is also a congruence relation on the clone
$\mathsf{T}(\Sigma)$. In particular, we can define $\circ^{(n)}_{k}$ on
$T(\Sigma)/\overline{E}$ by

$[\phi]_{\overline{E}}\circ^{(n)}_{k}([\theta_{1}]_{\overline{E}},\dots,[\theta_{k}]_{\overline{E}})=[\phi(\theta_{1},\dots,\theta_{k})]_{\overline{E}}.$

This makes the graded set $T(\Sigma)/\overline{E}$ into a clone; the clone
axioms for $T(\Sigma)/{\overline{E}}$ may be immediately checked from the
existence of a surjective morphism of graded sets $q\colon
T(\Sigma)\longrightarrow T(\Sigma)/\overline{E}$ (given by
$\theta\longmapsto[\theta]_{\overline{E}}$) preserving the clone operations.
The resulting clone is denoted by
$\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$; in words, it is the clone
consisting of _$\Sigma$ -terms modulo equational theorems of
${{\langle\,\Sigma\,|\,E\,\rangle}}$_. It is also characterised by a universal
property.

######  Proposition 3.8.

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory, and let
$q\colon\mathsf{T}(\Sigma)\longrightarrow\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$
be the clone homomorphism defined by $q_{n}(\theta)=[\theta]_{\overline{E}}$
for each $n\in\mathbb{N}$ and $\theta\in T(\Sigma)_{n}$. Given any clone
$\mathsf{S}=(S,p,\circ)$ and a clone homomorphism
$g\colon\mathsf{T}(\Sigma)\longrightarrow\mathsf{S}$ such that for any
$t\approx_{n}s\in E$, $g_{n}(t)=g_{n}(s)$ holds, there exists a unique clone
homomorphism
$h\colon\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}\longrightarrow\mathsf{S}$
such that $h\circ q=g$.

$\mathsf{T}(\Sigma)$$\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$$\mathsf{S}$$q$$h$$g$

###### Proof.

The clone homomorphism $h$ is given by
$h_{n}([\theta]_{\overline{E}})=g_{n}(\theta)$; this is shown to be well-
defined by induction on ${{\langle\,\Sigma\,|\,E\,\rangle}}$-proofs (see
Definition 2.8). The uniqueness of $h$ is immediate from the surjectivity of
$q$. ∎

We can now show that for any presentation of an equational theory
${{\langle\,\Sigma\,|\,E\,\rangle}}$, to give a model of
${{\langle\,\Sigma\,|\,E\,\rangle}}$ is equivalent to give a model of the
clone $\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$. A model of the clone
$\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$ (Definition 3.4) can be—by
Proposition 3.8—equivalently given as a suitable clone homomorphism out of
$\mathsf{T}(\Sigma)$; this in turn is—by Proposition 3.7—equivalently given as
a suitable morphism of graded sets out of $\Sigma$, which is nothing but a
model of the presentation of an equational theory
${{\langle\,\Sigma\,|\,E\,\rangle}}$ (Definition 2.7).

We also remark that every clone is isomorphic to a clone of the form
$\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$ for some presentation of an
equational theory ${{\langle\,\Sigma\,|\,E\,\rangle}}$. Indeed, given any
clone $\mathsf{S}=(S,p,\circ)$ we can consider its underlying graded set $S$
as a graded set of basic operations, and obtain the surjective clone
homomorphism
$\varepsilon_{\mathsf{S}}\colon\mathsf{T}(S)\longrightarrow\mathsf{S}$
extending the identity morphism on $S$ by Proposition 3.7. Define
$E_{\mathsf{S}}\subseteq T(S)\times T(S)$ to be the kernel of
$\varepsilon_{\mathsf{S}}$, i.e., the graded set of all pairs of elements of
$T(S)$ whose images under $\varepsilon_{\mathsf{S}}$ agree. Then we have
$\mathsf{S}\cong\mathsf{T}^{{\langle\,S\,|\,E_{\mathsf{S}}\,\rangle}}$.

The inference rules of equational logic we have given in Definition 2.8 can be
understood as the inductive definition of the congruence relation
$\overline{E}\subseteq T(\Sigma)\times T(\Sigma)$ on the clone
$\mathsf{T}(\Sigma)$ generated by $E\subseteq T(\Sigma)\times T(\Sigma)$. The
notion of clone therefore provides conceptual understanding of equational
logic.

We can also shed new light on the soundness and completeness theorem (Theorem
2.10) for equational logic. First we define a variant of the semantical
consequence relation $\vDash$ (Definition 2.9) via the “clone-valued
semantics”.

######  Definition 3.9.

  1. (1)

Let $\Sigma$ be a graded set, $\mathsf{S}=(S,p,\circ)$ be a clone and
$f\colon\Sigma\longrightarrow S$ be a morphism of graded set. For any
$\Sigma$-equation $t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$, we write

$(\mathsf{S},f)\vDash_{\mathrm{Clo}}t\approx_{n}s$

iff $g(t)=g(s)$, where $g\colon\mathsf{T}(\Sigma)\longrightarrow\mathsf{S}$ is
the clone homomorphism extending $f$ via Proposition 3.7.

  2. (2)

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory. For any $\Sigma$-equation $t\approx_{n}s\in T(\Sigma)\times
T(\Sigma)$, we write

${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash_{\mathrm{Clo}}t\approx_{n}s$

iff for any clone $\mathsf{S}=(S,p,\circ)$ and a morphism of graded set
$f\colon\Sigma\longrightarrow S$ such that
$(\mathsf{S},f)\vDash_{\mathrm{Clo}}t^{\prime}\approx_{n^{\prime}}s^{\prime}$
for all $t^{\prime}\approx_{n^{\prime}}s^{\prime}\in E$,
$(\mathsf{S},f)\vDash_{\mathrm{Clo}}t\approx_{n}s$.

######  Theorem 3.10 (cf. Theorem 2.10).

Let ${{\langle\,\Sigma\,|\,E\,\rangle}}$ be a presentation of an equational
theory.

  1. (1)

(Soundness with respect to the clone-valued semantics) Let $t\approx_{n}s\in
T(\Sigma)\times T(\Sigma)$. If ${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash
t\approx_{n}s$ then
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash_{\mathrm{Clo}}t\approx_{n}s$.

  2. (2)

(Completeness with respect to the clone-valued semantics) Let
$t\approx_{n}s\in T(\Sigma)\times T(\Sigma)$. If
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash_{\mathrm{Clo}}t\approx_{n}s$ then
${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$.

###### Proof.

The soundness theorem with respect to the clone-valued semantics follows from
Proposition 3.8. For the completeness theorem with respect to the clone-valued
semantics, consider the clone $\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}}$
and the morphism of graded set

$\Sigma$$T(\Sigma)$$T(\Sigma)/\overline{E}$$\eta_{\Sigma}$$q$

(see Proposition 3.7 for the definition of $\eta_{\Sigma}$ and Proposition 3.8
for $q$); then
$(\mathsf{T}^{{\langle\,\Sigma\,|\,E\,\rangle}},q\circ\eta_{\Sigma})\vDash_{\mathrm{Clo}}t\approx_{n}s$
iff ${{\langle\,\Sigma\,|\,E\,\rangle}}\vdash t\approx_{n}s$. ∎

Clearly,
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash_{\mathrm{Clo}}t\approx_{n}s$ implies
${{\langle\,\Sigma\,|\,E\,\rangle}}\vDash t\approx_{n}s$; the latter amounts
to restricting the clone $\mathsf{S}$ in Definition 3.9 to those of the form
$\mathsf{End}(A)$ for some set $A$. Hence the (original) soundness theorem
follows from the soundness theorem with respect to the clone-valued semantics,
but observe that the completeness theorem is not an immediate consequence of
the completeness theorem with respect to the clone-valued
semantics.666However, one can combine the completeness theorem with respect to
the clone-valued semantics with an _embedding theorem for clones_ , which
claims that every clone $\mathsf{S}$ can be embedded into a product of clones
of the form $\mathsf{End}(A)$, to obtain the completeness theorem. Such an
embedding may be obtained, for example, by canonically mapping an arbitrary
clone $\mathsf{S}=(S,p,\circ)$ into
$\prod_{i=0}^{\infty}\mathsf{End}{(S_{n})}$, whose injectivity can be checked
by an argument similar to our proof of the completeness theorem (Theorem
2.10).

## References

  * [Bir35] Garrett Birkhoff.  On the structure of abstract algebras.  In Mathematical proceedings of the Cambridge philosophical society, volume 31, pages 433–454. Cambridge University Press, 1935.
  * [BS81] S. Burris and H.P. Sankappanavar.  A course in universal algebra, volume 78 of Graduate Texts in Mathematics.  Springer, 1981.  The Millenium Edition available at http://www.math.uwaterloo.ca/~snburris/htdocs/ualg.html, 2000 and 2012.
  * [Bur71] Albert Burroni.  $T$-catégories (catégories dans un triple).  Cahiers de topologie et géométrie différentielle catégoriques, 12:215–321, 1971.
  * [Cur12] Pierre-Louis Curien.  Operads, clones, and distributive laws.  In Operads and Universal Algebra, volume 9 of Nankai Series in Pure, Applied Mathematics and Theoretical Physics, pages 25–49, 2012\.
  * [EM65] Samuel Eilenberg and John C. Moore.  Adjoint functors and triples.  Illinois Journal of Mathematics, 9(3):381–398, 1965.
  * [Fuj18] Soichiro Fujii.  Foundations of Algebraic Theories and Higher Dimensional Categories.  PhD thesis, University of Tokyo, 2018.
  * [Fuj19] Soichiro Fujii.  A unified framework for notions of algebraic theory.  arXiv preprint, 2019.
  * [Her00] Claudio Hermida.  Representable multicategories.  Advances in Mathematics, 151(2):164–225, 2000.
  * [Kel92] G.M. Kelly.  On clubs and data-type constructors.  Applications of Categories in Computer Science, 177:163–190, 1992\.
  * [Lei04] Tom Leinster.  Higher operads, higher categories, volume 298 of London Mathematical Society Lecture Note Series.  Cambridge University Press, 2004.
  * [Lin66] Fred E.J. Linton.  Some aspects of equational categories.  In Proceedings of the Conference on Categorical Algebra, pages 84–94. Springer, 1966.
  * [May72] J. Peter May.  The geometry of iterated loop spaces, volume 271 of Lecture Notes in Mathematics.  Springer, 1972.
  * [ML65] Saunders Mac Lane.  Categorical algebra.  Bulletin of the American Mathematical Society, 71(1):40–106, 1965\.
  * [Tay93] Walter Taylor.  Abstract clone theory.  In Algebras and orders, pages 507–530. Springer, 1993.