# Finite model theory for pseudovarieties and universal algebra: preservation,
definability and complexity.

Lucy Ham  Melbourne Integrative Genomics and MACSYS, School of Biosciences,
University of Melbourne, Victoria 3010 Australia<EMAIL_ADDRESS>and
Marcel Jackson  Department of Mathematical and Physical Sciences, La Trobe
University, Victoria 3086, Australia<EMAIL_ADDRESS>
###### Abstract.

We explore new interactions between finite model theory and a number of
classical streams of universal algebra and semigroup theory. A key result is
an example of a finite algebra whose variety is not finitely axiomatisable in
first order logic, but which has first order definable finite membership
problem. This algebra witnesses the simultaneous failure of the Łos-Tarski
Theorem, the SP-preservation theorem and Birkhoff’s HSP-preservation theorem
at the finite level as well as providing a negative solution to a first order
formulation of the long-standing Eilenberg Schützenberger problem. The example
also shows that a pseudovariety without any finite pseudo-identity basis may
be finitely axiomatisable in first order logic. Other results include the
undecidability of deciding first order definability of the pseudovariety of a
finite algebra and a mapping from any fixed template constraint satisfaction
problem to a first order equivalent variety membership problem, thereby
providing examples of variety membership problems complete in each of the
classes L, NL, $\texttt{Mod}_{p}(\texttt{L})$, P, and infinitely many others
(depending on complexity-theoretic assumptions).

###### 2000 Mathematics Subject Classification:

Primary: 03C13, 08B05; Secondary: 08B26, 68Q15, 68Q19, 08A30, 20M07

##  1\. Introduction

The central themes of finite model theory have primarily concerned relational
signatures, but several facets of reasonably independent lineage have
algebraic origins: amongst others we have in mind for example, tame congruence
theory in universal algebra [23], and the theory of pseudovarieties in
semigroup theory [2, 17], both with very significant development and many deep
and difficult results. The present article aims to develop some stronger
cross-fertilisation between the two genetic lines: relational and algebraic.
On the one hand, the article will provide some initial development of several
classical finite model theoretic ideas in universal algebraic settings. On the
other hand, we aim to explore some classical universal algebraic
considerations in a new light. The article is structured with these dual goals
in mind. The original contributions are sorted into a series of “Toolkit”
sections and of “Result” sections. In the toolkit sections we provide some
initial development of basic finite model theoretic considerations with
applicability to considerations in universal algebra, particularly relating to
variety membership.

  * •

In Section 3 we explore congruence generation and subdirect irreducibility,
solving a problem of Bergman and Slutzki [7] and introducing the notion of
definable completely meet irreducible congruences and first order subdirect
decomposition.

  * •

In Section 4 we provide some preservation theorems that hold at the finite
level in algebraic settings. An example result is Corollary 4.5, which shows
that if a finitely generated pseudovariety is definable by a
$\forall^{*}\exists^{*}$ sentence amongst finite algebras, then it is the
finite part of a finitely based variety, and so definable by a finite set of
equations.

  * •

In Section 5 we explore Ehrenfeucht-Fraïssé games in algebraic signatures,
providing a completeness theorem in uniformly locally finite settings.

The “Result” sections use ideas from the toolkit sections to provide some new
results of finite model theoretic character for universal algebra.

  * •

In Section 6 we provide a finite algebra whose pseudovariety is first order
definable by a $\forall^{*}\exists^{*}\forall^{*}$ sentence, yet not finitely
based in the conventional sense: there is no finite axiomatisation by
pseudoequations. In other words, it provides a negative solution to a first
order logic formulation of the long-standing Eilenberg-Schützenberger problem
[18] (which remains open in original formulation), and witnesses the
simultaneous failure of multiple classical preservation theorems. The example
also provides a tight upper limit to any further extensions of the
aforementioned Corollary 4.5.

  * •

In Section 7, we show how to map the complexity-theoretic landscape of fixed
finite template constraint satisfaction problems precisely into the
pseudovariety membership problem for finite algebras: for every finite
relational structure $\mathbb{S}$ we find a finite algebra ${\bf S}$ such that
the constraint satisfaction problem $\operatorname{CSP}(\mathbb{S})$ for
$\mathbb{S}$ is first order equivalent to the problem of deciding membership
in the variety of $\mathbf{S}$.

  * •

Finally in Section 8 we demonstrate some of the Toolkit developments to
provide a proof that McKenzie’s $A(\mathcal{T})$ construction from [41] yields
the undecidability of the finite model theoretic version of Tarski’s Finite
Basis Problem: the proof bypasses McKenzie’s $F(\mathcal{T})$ construction
[42] as well as Willard’s Finite Basis Theorem [53].

Before we commence the preliminary sections and subsequent development of
original results we provide some deeper contextual background to the
developments and their motivation.

###  1.1. Computational complexity.

A central context for the present work has been the following computational
problem, where by _variety_ we mean the equational class of ${\bf B}$, or
equivalently, the closure under the $\mathsf{HSP}$ class operator (homomorphic
images of subalgebras of direct products).
$\textsf{var-mem}(*,*)$
Instance: two finite algebras ${\bf A}$ and ${\bf B}$ of the same signature
signature.
Question: is ${\bf A}$ in the variety generated by ${\bf B}$?

Typically we are interested in the case where ${\bf B}$ is fixed, and the
input is algebra ${\bf A}$ only; this problem is denoted by $\textsf{var-
mem}(*,{\bf B})$, and we similarly let $\textsf{var-mem}({\bf A},*)$ denote
the dual problem where ${\bf A}$ is fixed. We will also be interested in the
promise restriction of this problem, where the input is required to be
subdirectly irreducible (that is, there is a unique minimum nontrivial
congruence; see Section 3). We denote this by $\textsf{var-si-mem}(*,{\bf
B})$.

The var-mem problem is in general doubly exponential time complete, even in
the restricted $\textsf{var-mem}(*,{\bf B})$ form: Marcin Kozik [36] showed
there is a finite algebra ${\bf B}$, for which $\textsf{var-mem}(*,{\bf B})$
is 2EXPTIME-complete, while a doubly exponential time algorithm solving var-
mem in full generality can be found in Bergman and Slutzki [5]. Overall, it
seems rather hard to determine the complexity of $\textsf{var-mem}(*,{\bf B})$
for given ${\bf B}$, and it has only been over the last couple of decades that
any examples were found for which the problem was not polynomial time
solvable, despite awareness of this problem at least 10 years prior (Problem 1
of [2] or Problem 3.11 of [34] for example). Zoltan Szekely found a flat graph
algebra with NP-complete finite membership in its variety [48]. Monoid and
semigroup examples with NP-hard finite membership were subsequently provided
by the second author and Ralph McKenzie [28], eventually leading to a
6-element example by the second author [26], the minimum possible cardinality
(for a semigroup). A 26-element involuted semigroup whose variety has NP-hard
finite membership was found by the second author and Volkov [32], though this
can be reduced to 10 elements using the developments of [26]; and a
$3$-element semiring with NP-hard membership has been given in [30], the
smallest possible size for any algebra for intractable var-mem problem. Marcin
Kozik found several examples of increasingly harder finite membership (PSPACE-
complete and EXPSPACE complete [35]), eventually leading to the aforementioned
example with 2EXPTIME-complete finite membership problem for its variety [36].

There is a connection here with the finite basis problem, as when ${\bf B}$
has a finite basis for its equational theory, then a particularly transparent
algorithm for solving $\textsf{var-mem}(*,{\bf B})$ emerges: simply test the
equations in the basis on the input ${\bf A}$. Not only is this a polynomial
time solution, it shows that $\textsf{var-mem}(*,{\bf B})$ is first order
definable. This immediately motivates a finite model theoretic consideration:
is this the only way that $\textsf{var-mem}(*,{\bf B})$ can be first order
definable? Thus, an early motivation for the developments in the present
article was a search in the opposite direction to most of the above examples:
algebras ${\bf B}$ for which $\textsf{var-mem}(*,{\bf B})$ is maximally easy.
This is reinforced by the open problems in the next subsection, which also
give rise to tractable instances of $\textsf{var-mem}(*,{\bf B})$; indeed the
first order ES problem is precisely the question just asked.

###  1.2. Universal algebra.

One motivation for examining the finer computational complexity of tractable
variety membership problems is that there are connections with two of the most
famous open problems in universal algebra.

> The Eilenberg-Schützenberger Problem [18, p. 417]. (The ES problem.) Is it
> true that when a finite algebra ${\bf A}$ of finite signature generates a
> variety without a finite equational basis, then the finite part of this
> variety has no finite equational basis?

If ${\bf A}$ were a counterexample to the Eilenberg-Schützenberger Problem,
then the complexity of the finite membership in $\mathsf{HSP}({\bf A})$ is in
FO (the class of first order definable decision problems), even if ${\bf A}$
is NFB. Indeed, in the context of computational complexity the following
variant might seem more pertinent.

> First order ES Problem. Is it true that when a finite algebra ${\bf A}$ of
> finite signature generates a variety without a finite axiomatisation in
> first order logic, then the finite part of this variety has no finite
> axiomatisation in first order logic?

Even though the finite axiomatisability in the premise of this implication is
equivalent to finite axiomatisability by equations, that implication is not
clear at the finite level. We will show that this first order variant of the
Eilenberg-Schützenberger Problem has a negative solution.

The next problem is usually attributed to a spoken speculation by Bjarni
Jónsson at Oberwolfach in 1976 (see [29, pp. 256]) but also appears in the PhD
thesis of Robert E. Park [43] from the same year. (See [54] for detailed
discussion of this problem.)

> The Jónsson-Park Conjecture [43]. (JP conjecture.) Does every finite algebra
> of finite type whose variety has only finitely many subdirectly irreducibles
> also have a finite basis for its equations?

If ${\bf A}$ were a counterexample to the JP conjecture then the complexity of
$\textsf{var-mem}(*,{\bf B})$ is in P, because any instance ${\bf A}$ may be
decomposed in polynomial time to a polynomial number of subdirectly
irreducible quotients [16], and it suffices to check each of these for
membership in the finite list of subdirectly irreducibles in
$\mathsf{HSP}({\bf A})$. We will present a universal algebraic condition that
in some cases enables this decomposition to be performed as a first order
construction. A first order variant of the JP Conjecture seems relevant; we
phrase these as problems rather than as a conjecture.

> First order JP Problem. If a finite algebra of finite type generates a
> variety with only finitely many subdirectly irreducibles, must its
> pseudovariety be definable in first order logic at the finite level?

We do not resolve this problem in the present article, though demonstrate some
of the ideas presented by giving a reasonably straightforward positive
verification of the First Order JP Problem in the case of semilattice-based
algebras (this follows already from the more powerful finite basis theorem for
congruence meet semidistributive varieties due to Ross Willard [53], but our
proof is very different and significantly easier).

###  1.3. Preservation Theorems

The first order ES-problem is related to the programme of classifying which
classical model theoretic preservation theorems hold at the finite level; see
[1] or [47, §2]. We briefly recall some of the classical preservation theorems
of relevance.

The Łos-Tarski Theorem (Preservation Theorem for $\mathsf{S}$-closed classes).

> Let $\mathcal{L}$ be a signature and $\mathscr{K}$ be a hereditary class of
> $\mathcal{L}$-structures (that is, closed under taking isomorphic copies of
> substructures). If $mathscr{K}=\operatorname{Mod}(\Phi)$ for some first
> order sentence $\Phi$, then $\Phi$ is equivalent to a universal sentence.

For the following recall that an existential positive sentence in first order
logic is a sentence of the form $\exists\bar{x}\phi(\bar{x})$ where
$\phi(\bar{x})$ is an open formula built from atomic formulæ using only
conjunction and disjunction (no negation or implication).

Homomorphism Preservation Theorem.

> Let $\mathcal{L}$ be a signature and $\mathscr{K}$ be a class of
> $\mathcal{L}$-structures closed under homomorphisms: whenever ${\bf A}$ and
> ${\bf B}$ are $\mathcal{L}$-structures with a homomorphism from ${\bf A}$
> into ${\bf B}$ and ${\bf A}\in\mathscr{K}$ then ${\bf B}\in\mathscr{K}$
> also. If $\mathscr{K}$ is the class of models of a first order sentence
> $\Phi$, then $\mathscr{K}=\operatorname{Mod}(\Phi)$ for some first order
> sentence $\Phi$, then $\Phi$ is equivalent to an existential positive
> sentence.

A Horn clause is a disjunction of atomic sentences and negated atomic
sentences, where at most on disjunct is not negated. A Horn formula is a
conjunction of Horn clauses, and is universal if it is universally quantified.
Preservation Theorem for $\mathsf{SP}$-classes.

> If $\Phi$ is a sentence defining a class $\mathscr{K}$ of structures closed
> under taking isomorphic copies of substructures and direct products, then
> $\Phi$ is logically equivalent to a universal Horn sentence.

Preservation Theorem for $\mathsf{HSP}$-classes for algebraic signatures
(Birkhoff’s Preservation Theorem).

> If $\Phi$ is a sentence defining a variety $\mathscr{V}$, then $\Phi$ is
> logically equivalent to a universally quantified conjunction of equations.

A failure of Łos-Tarski theorem at the finite level was discovered first by
Tait [49] and then independently by Gurevich and Shelah; see [1] for several
variants of the Gurevich-Shelah example. On the other hand, Rossman [46]
solved Problem 2 of Alechina and Gurevich [1] positively by showing that the
Homomorphism Preservation Theorem holds at the finite level, in relational
signatures. The last two preservation theorems need minor adjustment to be
formulated at the finite level because general direct products produce
infinite objects from finite ones. Thus we restrict to closure under finitary
direct products only: $\mathsf{P}_{\rm fin}$. It turns out that there are many
familiar and failures of the $\mathsf{HSP}_{\rm fin}$-preservation theorem at
the finite level (see Example 2.2 below for instance). For $\mathsf{SP}_{\rm
fin}$-closed classes the situation is far less clear, and the possibility of
the corresponding preservation theorem holding at the finite level is Problem
1 of Alechina and Gurevich [1]. Clark, Davey, Jackson, Pitkethly [13, Theorem
4.2] implicitly resolved this negatively in algebraic signatures: a sentence
is found defining a class of a Boolean topological algebras; but at the finite
level, the class is $\mathsf{SP}_{\rm fin}$-closed, but not definable by any
universal Horn sentence. In the present article we make further amendments to
this example to provide a simultaneous failure of all three of the
$\mathsf{S}$, $\mathsf{SP}_{\rm fin}$ and $\mathsf{HSP}_{\rm
fin}$-Preservation Theorems at the finite level: the class will be closed
under $\mathsf{HSP}_{\rm fin}$, definable by a
$\forall^{*}\exists^{*}\forall^{*}$ sentence, but not definable by any first
order $\forall^{*}\exists^{*}$ sentence. It remains unknown if the
$\mathsf{SP}_{\rm fin}$-preservation theorem holds at the finite level for
relational signatures. Similarly, it is unknown if the Homomorphism
Preservation Theorem holds at the finite level if operations are allowed,
though the first author has shown that it fails when relativised to the class
of lattices [21].

There are many other preservation theorems that we do not address in the
present article. One that does not appear in [1, 47], but which has recently
arisen in the context of variety-like classes of semigroups is the
preservation theorem for quantified conjunctions of equations (“equation
systems”) [22]. These admit a preservation theorem in terms of closure under
taking of elementary embeddings (E), homomorphic images and direct products
(originally asserted by Keisler [33]). We do not know if our example violates
the $\mathsf{E}\mathsf{H}\mathsf{P}$ Preservation Theorem at the finite level.

###  1.4. Pseudovarieties

A substantial impetus for the development of finite model theory has been from
computer science, via descriptive complexity, and in the context of database
theory. Relational structures have the prominent role in these settings. An
important context in which classes of finite _algebraic_ systems have
prominence is in the interaction between finite semigroups and regular
languages. Here, the famous Eilenberg-Schützenberger correspondence [17],
provides a strong impetus for the study of _pseudovarieties_ : classes of
finite algebras closed under homomorphisms, subalgebras and finitary direct
products. The Eilenberg-Schützenberger correspondence provides a dual
isomorphism between the lattice of semigroup pseudovarieties and the lattice
of so-called varieties of regular languages. This also provides a further
motivation for problems such as $\textsf{var-mem}(*,{\bf A})$, as membership
of languages in natural classes of regular languages can be recast as
membership problems of their syntactic semigroup in natural pseudovarieties.

The standard approach to axiomatising pseudovarieties is by way of equations
between pseudowords: equalities between elements of free profinite algebras:
see [2] (and Example 2.2 below). Our counterexample to the first order ES
Problem has no finite axiomatisation by pseudo-equations, despite being
finitely axiomatised in first order logic (without recourse to pseudoterms); a
semigroup example awaits discovery, or a nonexistence proof.

###  1.5. Historical note

Much of the early development of the present article occurred prior to the
first author’s article [21], emerging out of the second author’s 00’s work
[13] and [25] and incorporating project work by the first author under the
support of the Australian Mathematical Sciences Institute during the summer of
2010/2011. Further development occurred within the second author’s funded
project _Algebra in Complexity and Complexity in Algebra_ (Australian Research
Council DP1094578). A number of the ideas were also presented by the second
author in a talk at the ALCFest conference at Charles University Prague 2014,
and more recently at the Workshop on Finite Model Theory and Multi-Valued
Logics, University of Queensland 2022.

##  2\. Preliminaries

###  2.1. Varieties and other algebraic concepts

We direct the reader to a typical universal algebra text such as [4] or [11]
for deeper explanation around the following concepts. A reader familiar with
the area can skip the section entirely.

The algebraic focus of the article is primarily with theory of varieties and
to a lesser extent quasivarieties, and their restriction to finite algebras.
Recall that a _variety_ of algebras is any class $\mathscr{V}$ of algebras of
the same signature that is defined by some set (possibly infinite) of
equations: universally quantified equalities between terms. (Equations are
also often referred to as _identities_.) Equivalently, $\mathscr{V}$ is a
variety if it is closed under the class operators $\mathsf{H}$ (taking
homomorphic images), $\mathsf{S}$ (isomorphic copies of subalgebras) and
$\mathsf{P}$ (direct products). The variety generated by an algebra ${\bf A}$
is $\mathsf{HSP}({\bf A})$.

######  Example 2.1.

The variety of semilattices is the class of algebras with a single binary
operation $\wedge$ defined by idempotence, commutativity and associativity:

$x\wedge x\approx x,\quad x\wedge y\approx y\wedge x,\quad x\wedge(y\wedge
z)\approx(x\wedge y)\wedge z$

(universally quantified). Equivalently, the variety of semilattices is equal
to $\mathsf{HSP}(\mathbf{S}_{\wedge})$, where $\mathbf{S}_{\wedge}$ denotes
the $2$-element semilattice (which can be represented by interpreting $\wedge$
as the usual number-theoretic multiplication on the two-element set
$\\{0,1\\}$).

We will say that an algebra is _semilattice-based_ if its fundamental
operations include a binary operation satisfying the semilattice axioms.

When ${\bf A}$ is finite, then the finite members of $\mathsf{HSP}({\bf A})$
are obtained by taking only finitary direct products $\mathsf{P}_{\rm fin}$;
in other words $\mathsf{HSP}_{\rm fin}({\bf A})$. In general a class of finite
algebras closed under $\mathsf{HSP}_{\rm fin}$ is called a _pseudovariety_.
Pseudovarieties cannot in general be defined by equations (even at the finite
level), and pseudo-equations are the standard approach: using equalities
between limits of sequences of terms rather than between terms.

######  Example 2.2.

The pseudovariety of $\mathscr{J}$-trivial monoids is the class of finite
monoids satisfying

$\forall a\forall b\forall x_{1}\forall y_{1}\forall x_{2}\forall y_{2}\
x_{1}ay_{1}\approx b\And x_{2}by_{2}\approx a\rightarrow a\approx b.$

and can also be axiomatised by pseudoequations $x^{\omega}\approx
x^{\omega+1}$ and $(xy)^{\omega}\approx(yx)^{\omega}$, where $x^{\omega}$
denotes pseudo-operation defined as the limit $\lim_{n\to\infty}x^{n!}$, the
limit of an eventually constant sequence in any finite monoid.

As described in Subsection 1.3, a _universal Horn class_ is a class of
structures (algebras, relational structures, or general structures with both
operations and relations), defined by universally quantified conjunctions of
Horn clauses: disjunctions of atomic and negated atomic formulæ, where at most
one disjunct is non-negative. These may also equivalently be described as
classes closed under taking isomorphic copies induced substructures
($\mathsf{S}$ again), direct products over nonempty sets of models
$\mathsf{P}^{+}$, and ultraproducts $\mathsf{P}_{u}$.

######  Example 2.3.

The class of simple graphs may be considered as symmetric loopless digraphs,
and is the universal Horn class defined by

$\neg(x,x)\in R,\qquad\neg(x,y)\in R\vee(y,x)\in R$

This universal Horn class has no finite generator.

As usual, when a Horn clause has exactly one positive disjunct, then we can
rewrite it as an implication: so $\neg(x,y)\in R\vee(y,x)\in R$ becomes
$(x,y)\in R\rightarrow(y,x)\in R$. _Quasivarieties_ are universal Horn classes
definable by implicative Horn clauses: where precisely one disjunct is
positive, usually written as an implication. The implication in Example 2.2 is
another example quasiequation. Equivalently, quasivarieties are universal Horn
classes closed under taking arbitrary direct products: meaning we allow the
degenerate direct product over the empty set of structures, which returns the
one element total structure (all relations are total on this one point). This
one-element structure is the only difference between a quasivariety and a
universal Horn class, so from a computational and axiomatisability perspective
they are not significantly different.

We make a lot of use of the notion of _uniform local finiteness_ for finitely
generated classes: this means a class of structures in which for all $n$,
there exists $m$ such that the $n$-generated substructures have size at most
$m$. In most cases, what we really use is the less well-known concept
_regularly locally finite_ , which means that there are only finitely many
$n$-generated substructures up to isomorphism, all finite. In finite
signatures however, these concepts are equivalent, see Bezhanishvili [8]
(noting that we have bypassed consideration of whether the class in question
is hereditary by including “substructures” in the definition). All classes of
relational structures are uniformly locally finite, as there is no generation
power. The following easy lemma is folklore.

######  Lemma 2.4.

Let $\mathscr{K}$ be a uniformly locally finite class of algebras of the same
finite signature. Then the pseudovariety generated by $\mathscr{K}$ is also
uniformly locally finite.

The next lemma is usually called Birkhoff’s Finite Basis Theorem after Garrett
Birkhoff [9]; see Theorem 4.2 of Burris and Sankappanavar [11] for example,
where we direct the reader to a proof. (Note that the proof in [11] assumes
that $\mathscr{K}$ is the variety generated by a finite algebra, but in fact
it only uses the idea that the $k$-generated free algebra is finite, and this
requires only that $\mathscr{K}$ is a uniformly locally finite class of
algebras.)

######  Birkhoff’s Finite Basis Theorem 2.5.

Let $\mathscr{K}$ be a uniformly locally finite class of algebras. For any
number $k$, there is a finite set equations

$\Sigma_{\rm BFB}:=\\{s_{i}(x,x_{1},\dots,x_{k})\approx
t_{i}(x,x_{1},\dots,x_{k})\mid i=1,2,\dots,\ell\\}$

such that $\mathscr{K}\models\Sigma_{\rm BFB}$ and for every term
$t(x,x_{1},\dots,x_{k})$ there is an $i\leq\ell$ with $\Sigma_{\rm BFB}\vdash
t(x,x_{1},\dots,x_{k})\approx t_{i}(x,x_{1},\dots,x_{k})$.

The laws provided by this theorem enable us to reduce arbitrary terms in a
fixed finite alphabet to one in some fixed finite set.

###  2.2. Preliminaries: first order reductions

We now recall the definition of a first-order reduction; see [24] or [39] for
a more complete treatment. In the standard definition for computational
complexity we are allowed recourse to a strict linear order $<$ and work
entirely within relational signatures. Every operation of arity $n$ can be
considered as a relation of arity $n+1$ using its graph.

For $n\in{\mathbb{N}}\cup\\{0\\}$, purely relational signatures $\mathcal{R}$
and $\mathcal{S}$ and variables $\vec{x}=x_{0},\dots,x_{n-1}$, a first-order
${\mathcal{R}\cup\\{<\\}}$-formula $\varphi(\vec{x})$ determines a family of
$n$-ary relations on any ${\mathcal{R}\cup\\{<\\}}$-structure $\mathbb{B}$ in
the following way. First, the solution set of $\varphi(\vec{x})$ is an $n$-ary
relation. Second, for any fundamental relation $s\in\mathcal{S}$ of arity $k$,
a $kn$-ary formula $\psi_{s}(\vec{x}_{1},\dots,\vec{x}_{k})$ (where
$\vec{x}_{i}$ denotes $x_{i,0},\dots,x_{i,n-1}$) in the language of
${\mathcal{R}\cup\\{<\\}}$ determines a family of $k$-ary relations on
$n$-tuples: a $k$-ary relation on $B^{n}$. The family

$\\{\varphi(\vec{x})\\}\cup\\{\psi_{s}(\vec{x}_{1},\dots,\vec{x}_{k})\mid
s\in\mathcal{S}\\}$

defines an ${\mathcal{S}}$-structure $\mu(\mathbb{B})$, whose universe $U$ is
the solution set of $\varphi(\vec{x})$, as a subset of $B^{n}$, and where the
relations on $\mu(\mathbb{B})$ are the restriction to $U$ of the solution sets
of $\psi_{s}(\vec{x_{1}},\dots,\vec{x_{k}})$, for each $s\in\mathcal{S}$.
These formulas form an $n$-ary _first order query_.

We will also explore a one-to-many variation of this idea. In this formulation
we have a first order query, as just defined but allow some additional free
variables $y_{1},\dots,y_{k}$ in all formulas. Each evaluation of these
variables in some structure $\mathbb{A}$, say
$(y_{1},\dots,y_{k})\mapsto(a_{1},\dots,a_{k})$, will give rise to a first
order query with parameters $a_{1},\dots,a_{k}$. The intention is that we have
a reduction from problem $\mathcal{P}$ to $\mathcal{Q}$ where structure
$\mathbb{A}$ has a property $\mathcal{P}$ if and only if for every evaluation
$(y_{1},\dots,y_{k})\mapsto(a_{1},\dots,a_{k})$ in the universe $A$ has
property $\mathcal{Q}$. In particular, we observe that if property
$\mathcal{Q}$ is first order, then so also is property $\mathbb{P}$, as we are
simply asserting that the structure defined by the first order query has first
order property $\mathcal{Q}$ for all choices of $a_{1},\dots,a_{k}$.

##  3\. Toolkit: principal congruences and subdirect irreducibility

In this section we observe some facts concerning the precise complexity of
several problems relating to the decomposition into subdirectly irreducible
quotients. Previous contributions due to Bergman and Slutzki [5, 6, 7] give
much of the general picture, though we solve one open problem in their work,
and find improved complexity for a range of important classes of interest.

Recall that an algebra is _subdirectly irreducible_ if there is a pair of
distinct elements $a\neq b$ that is contained in the principal congruence of
all pairs. Equivalently, there is a unique minimum nontrivial congruence: the
_monolith_. As every algebra is a subdirect product of its subdirectly
irreducible quotients, we obtain a reduction from $\textsf{var-mem}(*,{\bf
B})$ to the problem $\textsf{var-si-mem}(*,{\bf B})$. This reduction can be
performed in polynomial time [16], though the authors are unaware of any finer
level classification of the complexity of this process. We explore some ideas
related to this, though present only a particular case where the subdirectly
irreducible quotients may be created as first order queries.

We will be interested in the following computational problems on finite
algebras.

Subdirect irreducibility
Instance: a finite algebra ${\bf A}$ of finite signature.
Question: is ${\bf A}$ subdirectly irreducible?

Principal congruence membership
Instance: a finite algebra ${\bf A}$ of finite signature and two unordered
pairs $\\{a,b\\}$ and $\\{c,d\\}$ taken from $A$.
Question: is $(a,b)$ in the principal congruence of ${\bf A}$ generated by
$(c,d)$?

The principal congruence generated by a pair $(c,d)$ is often denoted
$\operatorname{Cg}(c,d)$, so that the question in principal congruence
membership can be written “is $(a,b)\in\operatorname{Cg}(c,d)$?”

cong-class
Instance: A pair $({\bf A},C)$, where ${\bf A}$ is an algebra and $C\subseteq
A$.
Question: Is there a congruence $\theta$ on ${\bf A}$ in which $C$ is a
congruence class?

The following theorem is mostly due to Bergman and Slutzki, though item 3
solves positively the problem stated at [7, p.598], and therefore negatively
the problem stated at [7, p.603].

######  Theorem 3.1.

In any finite algebraic signature containing an operation of arity at least
$2$:

  1. (1)

([7]) Principal congruence membership is NL-complete.

  2. (2)

([7]) Subdirect irreducibility is NL-complete.

  3. (3)

cong-class is NL-complete.

###### Proof.

All three statements are proved by reduction from the undirected graph
reachability problem. Items 1 and 2 are [7, Theorem 3.5] (which also considers
the problem of recognising simplicity for a finite algebra; we have no use for
this here though). We consider item 3. It is already shown in [7] that cong-
class is in NL. We need to show hardness.

Consider a finite directed graph $G=(V,E)$ with distinguished vertices $u,v$.
Let $a,b,0$ be symbols not in $V$ and construct the graph $G_{a,b}$ on
$V\cup\\{a,b\\}$ with edges consisting of $E$ along with $(a,u)$, $(v,a)$ and
$(v,b)$. Now consider the graph algebra of $G_{a,b}$, with zero element $0$:
the elements are the vertices of $G_{a,b}$ and the product between vertices is
$x\cdot y=y$ if $(x,y)$ is an edge, and $0$ otherwise (all products involving
$0$ are also $0$). We claim that the subset $\\{a,b\\}$ is a congruence class
if and only if $v$ is not reachable from $u$. Clearly $\\{a,b\\}$ is a
congruence class if and only if it is the congruence class of the congruence
$\operatorname{Cg}(a,b)$, thus it suffices to show that $\\{a,b\\}$ is a
congruence class of $\operatorname{Cg}(a,b)$ if and only if $v$ is not
reachable from $u$.

Assume $v$ is reachable from $u$. So $v$ is also reachable from $a$, and then
$b$ is reachable from $a$; let $a=a_{0},u=a_{1},a_{2},\dots,a_{n}=v$ be a
sequence of vertices leading from $a$ to $v$. So $(\dots((aa_{1})a_{2})\dots
a_{n})b=vb=b$ and then $a\equiv b$ implies $b\equiv(\dots((ba_{1})a_{2})\dots
a_{n})b=0$. So $\\{a,b\\}$ is not a congruence class.

Now assume that $v$ is not reachable from $u$. Let $U$ denote the subset of
$V\cup\\{a,b\\}$ reachable by a nontrivial path from $u$, and observe that
$a,b,v\notin U$. It is now routine to show that $\operatorname{Cg}(a,b)$
consists of the following blocks: $\\{a,b\\}$, $U\cup\\{0\\}$ and all
singletons from $V\backslash U$.

This proof concerns only the case where there is a single binary operation,
but the argument can be transformed trivially into any signature containing at
least one operation of arity $\geq 2$ by selecting such an operation, and
making it equal to $\cdot$ above on the first two coordinates (and independent
of any further coordinates if it has arity more than $2$), and letting all
other operations be projections. ∎

As we shortly demonstrate, a wide range of algebraic settings enjoy a weak
congruence condition that improves on Theorem 3.1. Let $T_{x}$ be the set of
all terms in an algebraic signature in variables $\\{x,z_{1},z_{2},\dots\\}$
and let $F$ be a subset of $T_{x}$. For an algebra ${\bf A}$ and $a,b,c,d\in
A$ we write $\\{c,d\\}\looparrowright^{1}_{F}\\{a,b\\}$ if there is a term
$t(x,z_{1},z_{2},\dots)\in F$ and elements $e_{0},e_{1},\dots\in A$ such that

$\\{t^{\bf A}(c,e_{0},e_{1},\dots),t^{\bf
A}(d,e_{0},e_{1},\dots)\\}=\\{a,b\\}.$

Define $\\{c,d\\}\looparrowright^{n}_{F}\\{a,b\\}$ if there is a sequence
$a=a_{0},a_{1},a_{2},\dots,a_{n}=b$ with
$\\{c,d\\}\looparrowright_{F}^{1}\\{a_{i},a_{i+1}\\}$ for each
$i=0,\dots,n-1$. Finally, write $\\{c,d\\}\looparrowright_{F}\\{a,b\\}$ if
$\\{c,d\\}\looparrowright_{F}^{k}\\{a,b\\}$ for some $k$. Maltsev proved that
a pair $(a,b)\in\operatorname{Cg}(c,d)$ if and only if
$\\{a,b\\}\looparrowright_{T_{x}}\\{c,d\\}$. A class has _term finite
principal congruences_ (TFPC) if there a finite set $F\subseteq T_{x}$ such
that $\looparrowright_{T_{x}}$ coincides with $\looparrowright_{F}$. A class
has _definable principal congruences_ (DPC) if there exists $n$ and a finite
subset $F\subseteq T_{x}$ with
${\looparrowright_{T_{x}}}={\looparrowright_{F}^{n}}$. The DPC property is
rather special, but as explained in [12], many familiar classes of algebraic
structures have the TFPC property, including semigroups, groups, rings and
lattices.

The following generalised version of principal congruence membership is useful
before we state and prove the theorem.

Congruence membership
Instance: a finite algebra ${\bf A}$ of finite signature, a subset $S\subseteq
A^{2}$ and an unordered pair $\\{a,b\\}$.
Question: is $(a,b)$ in the congruence of ${\bf A}$ generated by $S$?

######  Theorem 3.2.

Let $\mathscr{V}$ be a variety of finite signature and with TFPC.

  1. (0)

For any finite algebra ${\bf A}$ the congruence membership problem is solvable
in L.

As a consequence, each of the following problems are in L:

  1. (1)

Principal congruence membership;

  2. (2)

Subdirect irreducibility;

  3. (3)

cong-class.

###### Proof of Theorem 3.2..

We first explain why the solvability of (1), (2) and (3) in L follows from the
logspace solvability of (0) almost trivially: in each case we can solve in
logspace using an oracle for (0), and as $\texttt{L}^{\texttt{L}}=\texttt{L}$
we obtain membership in L. Note that space considerations still only concern
the working tape, and not the oracle tape, so that we do not need to concern
ourselves with the size of any constructed $S$ written to the oracle, only
with the working tape required to perform any calculations needed for that
writing; see [10, Section 6.2] for detailed discussion on this.

Item (1) is a specific case of (0), where $S=\\{(c,d)\\}$.

For item (2), subdirect irreducibility can be decided in L by systematically
enumerating (one-by-one, re-using the same piece of work tape) all pairs
$a\neq b$, and in each case systematically enumerating (one-by-one, reusing
some new piece of work tape) all $c\neq d$, testing for satisfaction of
$(a,b)\in\operatorname{Cg}(c,d)$ using the oracle. Subdirect irreducibility
holds if there is a choice of $(a,b)$ such that every pair $c\neq d$ satisfies
$(a,b)\in\operatorname{Cg}(c,d)$.

For item (3), observe that a subset $C\subseteq A$ is a congruence class of a
congruence if and only if it is a congruence class of the congruence
$\operatorname{Cg}(S)$, where $S=C^{2}\subseteq A^{2}$. Because $C$ is
trivially a subset of a congruence class of $\operatorname{Cg}(C^{2})$, we can
decide equality with a congruence class, by selecting an arbitrary $c\in C$,
and then systematically verifying $(d,c)\notin\operatorname{Cg}(C^{2})$ using
the oracle for (0), for each $d\notin C$. Again we have reduced to a special
case of (0), where $S=C^{2}$.

To prove (0), let $F$ be a finite subset of $T_{x}$ that determines principal
congruences in $\mathscr{V}$, let ${\bf A}$ be a finite member of
$\mathscr{V}$ and $S\subseteq A^{2}$. For any given pair $(a,b)\in A^{2}$, if
$a=b$ then $(a,b)\in\operatorname{Cg}(S)$ trivially, so we assume that $a\neq
b$. Then $(a,b)\in\operatorname{Cg}(S)$ if and only if $a$ is reachable from
$b$ in the undirected graph on $A$ whose undirected edges are $\\{\\{u,v\\}\in
A^{2}\mid S\looparrowright^{1}_{F}\\{u,v\\}\\}$. As $F$ is finite, the
relation $\\{c,d\\}\looparrowright^{1}_{F}\\{u,v\\}$ is a first order formula
for each $c\neq d$ with $(c,d)\in S$. The relation
$S\looparrowright^{1}_{F}\\{u,v\\}$ is simply the disjunction of the formulas
$\\{c,d\\}\looparrowright_{F}^{1}\\{u,v\\}$ over all pairs $(c,d)\in S$, and
hence is also a first order formula. Thus the edge relation of this graph is
itself first order definable from the input subset $S$ and algebra ${\bf A}$,
and so can be constructed in logspace. Thus (0) holds because undirected graph
reachability can be solved in L; see [44, 45]. ∎

Theorem 3.2 (2) shows that the promise of subdirect irreducibility in
restricting $\textsf{var-mem}(*,{\bf B})$ to $\textsf{var-si-mem}(*,{\bf B})$
can be verified in logspace. A more useful contribution would be if it gave
rise to a logspace reduction from $\textsf{var-mem}(*,{\bf B})$ to
$\textsf{var-si-mem}(*,{\bf B})$, however it is not clear to the authors if
this is true; even in nondeterministic logspace.

######  Question 3.3.

Is there a reasonably applicable algebraic condition that guarantees the
logspace construction of the subdirectly irreducible quotients of a finite
input algebra ${\bf B}$?

It would be nice if the TFPC condition was sufficient for example. We now
introduce a congruence condition which enables the construction of subdirectly
irreducible quotients in not only logspace, but even as a first order queries,
thereby showing that $\textsf{var-mem}(*,{\bf B})$ and $\textsf{var-si-
mem}(*,{\bf B})$ are in fact first order equivalent. This is only a weak
answer to Question 3.3 however, as it is likely that the property is
reasonably rare, even if we are able to provide at least one broad class in
which it does.

######  Definition 3.4.

Let $\mathscr{K}$ be a class of algebras of the same signature. The class
$\mathscr{K}$ is said to have _definable completely meet irreducible
congruences_ (abbreviated to _definable cmi congruences_) if there is a
formula $\pi(x,y,u,v)$ with four free variables $x,y,u,v$ such that every
${\bf A}\in\mathscr{K}$ and every $a,b\in A$ with $a\neq b$ we have
$\\{(c,d)\in A^{2}\mid{\bf A}\models\pi(a,b,c,d)\\}$ is a congruence
$\theta_{a,b}$ that is maximal with respect to not containing the pair
$(a,b)$.

We remind the reader that the property that a congruence $\theta$ is maximal
with respect to $(a,b)\notin\theta$ for some $a,b$ is equivalent to $\theta$
being completely meet irreducible in the congruence lattice. When $K$ is a
class of finite algebras, then the congruence lattice is finite, so complete
meet irreducibility coincides with meet irreducibility, and so for the
purposes of this paper, either notion would suffice.

In general there may not be a unique maximum congruence separating a pair
$a\neq b$, but Definition 3.4 only requires that $\theta_{a,b}$ be a maximal
congruence separating $a$ from $b$. In Lemma 6.4 we will show that the pointed
semidiscriminator variety (in the sense of [25]) over any finite signature has
definable cmi congruences.

The following gives a one-to-many first order reduction from an algebra with
definable cmi congruences to its subdirectly irreducible quotients. This in
turn provides a one-to-many first order reduction from $\textsf{var-
mem}(*,{\bf B})$ to $\textsf{var-si-mem}(*,{\bf B})$.

######  Theorem 3.5.

If $\mathscr{K}$ is a class of algebras of the same signature, closed under
taking homomorphic images and with definable cmi congruences, then there is a
first order query $\phi(x,y)$ with two free variables $x,y$, such that for
every ${\bf A}\in\mathscr{K}$ and every $a\neq b$ in $A$ we have $\phi(a,b)$
defines a subdirectly irreducible quotient of ${\bf A}$ in which the monolith
is generated by representatives of the congruence classes of $a$ and $b$.

###### Proof.

Let $\pi(x,y,u,v)$ be a formula defining cmi congruences in $K$. For each
${\bf A}\in K$ and each $a\neq b$ in $A$, let $\theta_{a,b}$ denote the cmi
congruence defined by $\pi(x,y,a,b)$. Our one-to-many reduction will use an
implicit linear order $\leq$ on the set $A$ (with $<$ being the corresponding
strict order).

We first observe that we may use $\leq$ to define the set of minimal
representatives of the $\theta_{a,b}$-classes: $\\{z\in A\mid\forall
x(\pi(x,z,a,b)\Rightarrow x\leq z)\\}$. On this set we define each fundamental
$n$-ary operation $f$ as follows:

$(f(c_{1},\dots,c_{n})\approx
d)\leftrightarrow(\pi(f(c_{1},\dots,c_{n}),d,a,b)).$

The operations are well defined because $\theta_{a,b}$ is a congruence
relation, and as we have selected the domain as a transversal of the
congruence classes, the defined algebra is a subdirectly irreducible quotient
of ${\bf A}$ in which the representative members of the congruence classes of
$a$ and $b$ generate the minimal congruence. ∎

######  Corollary 3.6.

If $\mathscr{V}$ has definable cmi congruences, by formula $\pi(x,y,u,v)$,
then $\mathscr{V}_{\rm si}$ is definable within $\mathscr{V}$ by the sentence

$\exists u\exists v\forall x\forall y\ u\neq v\And(x\approx
y\leftrightarrow\pi(x,y,u,v)).$

We mention that subdirectly irreducible algebras are also first order
definable in the presence of definable principle congruences, as subdirect
irreducibility is equivalent to

$\exists u\exists v\forall x\forall y\ x\not\approx
y\rightarrow(u,v)\in\operatorname{Cg}(x,y).$

##  4\. Toolkit: Preservation Theorems

In this section we provide some preservation theorems that hold at the finite
level in algebraic signatures. In the class of relational structures,
$\mathsf{HSP}$-classes are too restrictive to be of much interest. However
there is a rather elementary preservation theorem in universal first order
logic that can be stated for $\mathsf{SP}$-classes for arbitrary finite
structures (relational or algebraic), provided uniform local finiteness is
assumed. To begin with we recall some basic facts concerning classes generated
by classes of finite structures. In the following, $\operatorname{Mod}_{\rm
fin}$ denotes “finite models of” and $\operatorname{Th}_{\rm uH}(\mathscr{K})$
denotes the universal Horn theory of $\mathscr{K}$.

######  Lemma 4.1.

The following hold for any $\mathsf{SP}_{\rm fin}$-closed class $\mathscr{K}$
of finite structures in a finite signature.

  1. (1)

$\mathscr{K}=\operatorname{Mod}_{\rm fin}(\operatorname{Th}_{\rm
uH}(\mathscr{K}))$.

  2. (2)

$\mathscr{K}$ is uniformly locally finite if and only if
$\operatorname{Mod}(\operatorname{Th}_{\rm uH}(\mathscr{K}))$ is uniformly
locally finite.

  3. (3)

$\mathscr{K}$ is uniformly locally finite if and only if the ultraproduct
closure of $\mathscr{K}$ is uniformly locally finite.

  4. (4)

If $\mathscr{K}$ is a uniformly locally finite class of algebras and is also
closed under taking homomorphic images, then $\mathscr{K}$ is the finite part
of $\mathsf{HSP}(\mathscr{K})$.

###### Proof.

The first part is due to Gorbunov [19, Proposition 2.5.12], while the second
part is usually attributed to Maltsev. Part (3) follows from part (2) because
the ultraproduct closure of $\mathscr{K}$ is a subclass of the universal Horn
class generated by $\mathscr{K}$.

For the fourth part, note that every variety is generated by its finitely
generated free algebras, and all finite algebras are quotients of free
algebras. Uniform local finiteness ensures that finitely generated free
algebras in the variety generated by $\mathscr{K}$ are finite, and as
$\mathscr{K}$ is assumed to be closed under quotients, these free algebras,
and their quotients lie in $\mathscr{K}$. In other words, $\mathscr{K}$ is the
finite part of $\mathsf{HSP}(\mathscr{K})$. ∎

The following easy observation gives some form of partial preservation theorem
at the finite level.

######  Theorem 4.2.

Let $\Phi$ be a _universal_ sentence defining a uniformly locally finite class
whose finite models $\mathscr{K}=\operatorname{Mod}_{\rm fin}(\Phi)$ are
$\mathsf{SP}_{\rm fin}$-closed. Then $\operatorname{Mod}(\Phi)$ is a universal
Horn class and $\Phi$ is logically equivalent to a universal Horn sentence,
even amongst structures of possibly infinite size.

###### Proof.

First observe that as $\mathscr{K}\subseteq\operatorname{Mod}(\Phi)$ and
$\operatorname{Mod}(\Phi)$ is locally finite and ultraproduct-closed, it
follows from Lemma 4.1 part (3) that $\mathscr{K}$ is uniformly locally
finite. Then Lemma 4.1 part (2) implies that
$\operatorname{Mod}(\operatorname{Th}_{\rm uH}(\mathscr{K}))$ is locally
finite.

Next observe that two locally finite universal classes agreeing on finite
models coincide. So $\operatorname{Mod}(\operatorname{Th}_{\rm
uH}(\mathscr{K}))=\operatorname{Mod}(\Phi)$, and then the Compactness Theorem
ensures that there is a finite subset of $\operatorname{Th}_{\rm
uH}(\mathscr{K})$ that is equivalent to $\Phi$. ∎

######  Theorem 4.3.

If $\Phi$ is a universal sentence defining a uniformly locally finite
pseudovariety $\mathscr{K}$ of finite algebras then $\Phi$ is logically
equivalent to a finite conjunction of equations, even amongst structures of
possibly infinite size.

###### Proof.

The proof is almost identical to that of Theorem 4.2, using Lemma 4.1(4) in
place of part (3). ∎

The following result is given for function-free signatures in [20, Theorem 3],
where it is attributed to Compton. Recall that a _hereditary class_ means one
that is closed under $\mathsf{S}$.

######  Theorem 4.4.

If $\Phi$ is a $\forall^{*}\exists^{*}$-sentence defining a uniformly locally
finite hereditary class $\mathscr{K}$ of finite structures then $\Phi$ is
equivalent on finite structures to a universal sentence.

###### Proof.

The proof is by way of a sort of “localised Skolemisation” process. Let $\Phi$
be

$\forall x_{1}\forall x_{2}\dots\forall x_{n}\exists y_{1}\exists
y_{2}\dots\exists y_{m}\phi(x_{1},\dots,x_{n},y_{1},\dots,y_{m}).$

We first observe that uniform local finiteness allows us to apply Birkhoff’s
Finite Basis Theorem 2.5 to find a finite set $F$ of terms in variables
$x_{1},\dots,x_{n}$ such that every term $t(x_{1},\dots,x_{n})$ is equivalent
in $\mathscr{K}$ to one from $F$; that is, for every $t(x_{1},\dots,x_{n})$
there exists $s\in F$ with $\mathscr{K}\models s\approx t$.

We claim that $\Phi$ is equivalent to the sentence $\Phi^{\prime}=\forall
x_{1}\dots\forall x_{n}\phi^{\prime}(x_{1},\dots,x_{n})$ where

$\phi^{\prime}(x_{1},\dots,x_{n}):=\bigvee_{(t_{1},\dots,t_{m})\in
F^{m}}\phi(x_{1},\dots,x_{n},t_{1}(x_{1},\dots,x_{n}),\dots,t_{m}(x_{1},\dots,x_{n})).$

It is trivial that $\Phi^{\prime}\vdash\Phi$, so that the finite models of
$\Phi^{\prime}$ are a subclass of $\mathscr{K}$. Now assume that ${\bf
A}\in\mathscr{K}$. Consider any $a_{1},\dots,a_{n}\in A$. Now as
$\mathrm{sg}_{{\bf A}}(a_{1},\dots,a_{n})\models\Phi$, there are
$b_{1},\dots,b_{m}\in\mathrm{sg}_{{\bf A}}(a_{1},\dots,a_{n})$ with
$\mathrm{sg}_{{\bf
A}}(a_{1},\dots,a_{n})\models\phi(a_{1},\dots,a_{n},b_{1},\dots,b_{m})$. As
$b_{1},\dots,b_{m}\in\mathrm{sg}_{{\bf A}}(a_{1},\dots,a_{n})$ there are terms
$t_{1},\dots,t_{m}\in F$ with $b_{i}=t_{i}(a_{1},\dots,a_{n})$ for
$i=1,\dots,m$. Then

$\mathrm{sg}_{{\bf
A}}(a_{1},\dots,a_{n})\models\phi(a_{1},\dots,a_{n},t_{1}(a_{1},\dots,a_{n}),\dots,t_{m}(a_{1},\dots,a_{n})),$

and hence $\mathrm{sg}_{{\bf
A}}(a_{1},\dots,a_{n})\models\phi^{\prime}(a_{1},\dots,a_{n})$. That is, ${\bf
A}\models\phi^{\prime}(a_{1},\dots,a_{n})$. As $a_{1},\dots,a_{n}$ were
arbitrary, it follows that ${\bf A}\models\Phi^{\prime}$. ∎

The following result also holds if “pseudovariety” is replace by
“$\mathsf{SP}_{\rm fin}$-closed class”, and “finite conjunction of equations”
is replaced by “universal Horn sentence”.

######  Corollary 4.5.

If $\Phi$ is a $\forall^{*}\exists^{*}$ sentence defining a uniformly locally
finite pseudovariety $\mathscr{K}$ of finite algebras, then $\Phi$ is
logically equivalent to a finite conjunction of equations, even amongst
structures of possibly infinite size.

###### Proof.

Theorem 4.4 shows that $\Phi$ is equivalent to a universal sentence, and then
Theorem 4.3 shows this is equivalent to a conjunction of equations. ∎

Another way to state Corollary 4.5 is that a uniformly locally finite
pseudovariety $\mathscr{K}$ of finite algebras is either finitely axiomatised
by equations, or cannot be defined by any $\forall^{*}\exists^{*}$-sentence.

We now observe that the assumption of uniform local finiteness here is
necessary (a similar example can be found in [47]).

######  Example 4.6.

The class of finite $\mathcal{J}$-trivial monoids is definable by a universal
Horn sentence, but not by any system of equations. So the Preservation Theorem
for $\mathsf{HSP}$-classes fails at the finite level, even amongst universal
Horn sentences. The example also shows that Theorem 4.3 and Corollary 4.5 do
not hold if the assumption of uniform local finiteness is dropped.

###### Proof.

Our definition of $\mathcal{J}$-triviality in Example 2.2 is by way of a
universal Horn sentence. However as all finite nilpotent monoids are
$\mathcal{J}$-trivial, all equations true of $\mathcal{J}$-trivial monoids are
true of all monoids. So the class of finite $\mathcal{J}$-trivial monoids is
not the set of finite models of any system of equations (and certainly not of
any finite conjunction of equations). ∎

##  5\. Toolkit: Ehrenfeucht Fraïssé games in finite algebras

In this section we consider algebraic Ehrenfeucht-Fraïssé games, proving
completeness of the approach when it comes to establishing failure of first
order definability amongst finite models within uniformly locally finite
classes. While we give basic details, we assume the reader has some
familiarity with Ehrenfeucht-Fraïssé games; details can be almost any text on
model theory, or finite model theory [39].

The board of the game consists two (typically not identical) structures ${\bf
A}$ and ${\bf B}$. In standard formulations the signature is restricted to
relations and constants only, but there is nothing in the definition that
prevents operations of positive arity also. The goal of Spoiler is to reveal
the two structures as distinct; the goal of Duplicator is to hide any
distinction between the two for as long as possible!

The players play a certain number of rounds. Each round consists of the
following rules.

  1. (1)

Spoiler picks a structure; either ${\bf A}$ or ${\bf B}$.

  2. (2)

Spoiler makes a move by selecting an element of that structure; either
$a\in{\mathbf{A}}$ or $b\in{\mathbf{B}}$.

  3. (3)

Duplicator responds by selecting an element in the other structure.

After $n$ rounds of an Ehrenfeucht-Fraïssé game, we have moves
($a_{1},\dots,a_{n}$) and ($b_{1},\dots,b_{n}$). Duplicator wins the $n$-round
game provided the map that sends each $a_{i}$ to $b_{i}$ is an isomorphism
between the substructures of ${\bf A}$ and ${\bf B}$ generated by
$\\{a_{1},\dots,a_{n}\\}$ and $\\{b_{1},\dots,b_{n}\\}$ respectively. If
Duplicator can win the $n$-round game regardless of how Spoiler plays, we say
that Duplicator has _an $n$-round winning strategy_ and we write ${\bf
A}\equiv_{n}{\bf B}$. In the conventional setting, where positive arity
operations are disallowed, there is almost no generation power: it simply
means the usual automatic inclusion of any constants in the signature. Given
that our focus is on algebras, we use standard notation
$\operatorname{Sg}^{\bf A}(s_{1},\dots,s_{k})$ to denote the subalgebra of
${\bf A}$ generated by some elements $s_{1},\dots,s_{k}$, dropping the
superscript ${\bf A}$ if this is implicit.

The _quantifier rank_ $\operatorname{qr}$ of a formula is defined inductively
as follows:

  * •

If $\phi$ is an atomic formula then $\operatorname{qr}(\phi)=0$;

  * •

$\operatorname{qr}(\phi_{1}\vee\phi_{2})=\operatorname{qr}(\phi_{1}\And\phi_{2})=\max\\{\operatorname{qr}(\phi_{1}),\operatorname{qr}(\phi_{2})\\}$;

  * •

$\operatorname{qr}(\neg\phi)=\operatorname{qr}(\phi)$;

  * •

$\operatorname{qr}(\forall x\,\phi)=\operatorname{qr}(\exists
x\,\phi)=\operatorname{qr}(\phi)+1$.

We use the notation $\operatorname{FO}[n]$ for all first order formulæ of
quantifier rank up to $n$, and in general use the abbreviation FO for _first
order_ (noting that FO refers to the class of problems definable in FO, with
linear order).

The first fundamental theorem for Ehrenfeucht-Fraïssé games in finite model
theory is the following; there is no requirement for the signature to be
relational here.

######  Theorem 5.1.

The following are equivalent for two finite structures ${\bf A}$ and ${\bf B}$
of the same type:

  1. (1)

${\bf A}\equiv_{n}{\bf B}$; that is, Duplicator has a winning strategy in an
$n$-round play of our new game.

  2. (2)

${\bf A}$ and ${\bf B}$ agree on $\operatorname{FO}[n]$.

Theorem 5.1 gives rise to a general methodology for proving inexpressibility
results, which we give in the next theorem. The theorem is usually restricted
to relational signatures (no operations of positive arity) where uniform local
finiteness holds always, and so the entire statement can be given as an if and
only if. The proof under uniform local finiteness assumptions is the main new
contribution in the section, though the arguments are mostly almost identical,
but incorporating Birkhoff’s Finite Basis Theorem 2.5.

######  Theorem 5.2.

A property $\mathcal{P}$ is not expressible in FO if for every
$n\in\mathbb{N}$, there exist two finite structures ${\bf A}_{n}$ and ${\bf
B}_{n}$, such that:

  * •

${\bf A}_{n}\equiv_{n}{\bf B}_{n}$.

  * •

${\bf A}_{n}$ has property $\mathcal{P}$, and ${\bf B}_{n}$ does not.

When relativised to any uniformly locally finite class of structures, the
converse also holds: inexpressibility in FO ensures the existence of ${\bf
A}_{n}$ and ${\bf B}_{n}$.

The following example demonstrates the necessity of some caveat for the “only
if” part of Theorem 5.2, and therefore a fundamental difference between
relational signatures and algebraic signatures.

######  Example 5.3.

Consider the signature of unars: unary algebras with a single unary operation
$f$, and consider the property $\mathcal{P}$ that $f^{n}(x)\approx f^{n+1}(x)$
holds for sufficiently large $n$. Then $\mathcal{P}$ is not first order
definable at the finite level, yet unars with property $\mathcal{P}$ can be
distinguished from unars failing $\mathcal{P}$ in a one step algebraic
Ehrenfreucht-Fraïssé game.

###### Proof.

Assume ${\bf A}$ satisfies $\mathcal{P}$ and ${\bf B}$ does not. So there is
$b\in B$ such that $f^{n}(b)$ never coincides with $f^{n+1}(b)$, for any $n$.
Spoiler chooses this $b$, and for any $a\in A$ that duplicator selects we find
that $\mathrm{sg}_{\bf A}(a)\not\cong\mathrm{sg}_{\bf B}(b)$ because for some
$n$ the property $f^{n}(a)=f^{n+1}(a)$ holds. So ${\bf A}\not\equiv_{1}{\bf
B}$.

Now to show that $\mathcal{P}$ is not first order definable at the finite
level. For this it suffices to work in the relational setting, where $f$ is
replaced by its graph: this is because if there is a first order formula
defining $\mathcal{P}$ in the algebraic setting, then it may be translated
into one defining $\mathcal{P}$ in the relational setting. Let
$\mathbb{A}_{k}$ denote the digraph consisting of a path of length $k$ with a
loop as terminal vertex, and let $\mathbb{B}_{k}$ denote the digraph
consisting of the disjoint union of $\mathbb{A}_{k}$ with a $k$-cycle. It is
routine exercise in standard Ehrenfreucht-Fraïssé games to verify that for
sufficiently large $k$, duplicator may survive $n$ rounds of this game; see
Figure 3.4 of Libkin [39] and accompanying text for example. ∎

Define the _height_ of a term as follows: variables are of height $0$. If $f$
is a fundamental operation of arity $n$ and the maximum height amongst some
set of terms $t_{1},\dots,t_{n}$ is $k$, then $f(t_{1},\dots,t_{n})$ is of
height $k+1$. We interpret this as defining the height of nullaries to be $1$.

The following lemma is an algebraic variant of Lemma 3.13 of Libkin [39].

######  Lemma 5.4.

Let $k,m,n$ be natural numbers.

  1. (1)

Every atomic subformula of a rank $k$ formula in $m$ free variables
$x_{0},\dots,x_{m-1}$ involves at most $m+k$ variables.

  2. (2)

Up to logical equivalence there are only finitely many distinct rank $k$
formulæ in the $m$ free variables $x_{0},\dots,x_{m-1}$ whose terms are of
height at most $n$.

###### Proof.

Both statements are proved by induction over $k$ (the number $m$ varies: for
each $k$ we ask the statement be true of any $m$). We omit full details of the
proof as it is essentially identical to as in [39, Lemma 3.13], with the one
difference occurring in the second item, in consideration of the base case of
a rank $0$ formula. However the difference is minor: the bound on height of
terms continues to ensure that there are only finitely many atomic formulæ in
$m$ free variables, and every rank $0$ formula is a Boolean combination of
these, and hence the base statement is true. ∎

######  Definition 5.5.

Let ${\bf A}$ be a finite algebra and $a\in A$. Define the _rank $k$ type_ of
the element $a$, denoted $\operatorname{tp}_{k}({\bf A},a)$, to be the set of
all FO-formulæ $\varphi(x)$ of rank $k$ for which ${\bf A}\models\varphi(a)$.

The set $\operatorname{tp}_{k}({\bf A},a)$ is always infinite because there is
no bound on height of any terms that appear within. The following lemma
contains the primary use of uniform local finiteness.

######  Lemma 5.6.

Let ${\bf A}$ be a finite algebra and $a\in A$. Then the rank $k$ type
$\operatorname{tp}_{k}({\bf A},a)$ of $a$ is logically equivalent to a finite
subset of $\operatorname{tp}_{k}({\bf A},a)$.

###### Proof.

We use the set $\Sigma_{\rm BFB}$ of equations identified in Birkhoff’s Finite
Basis Theorem 2.5 for the pseudovariety generated by ${\bf A}$ (which is
uniformly locally finite as ${\bf A}$ is finite), and use the notation of the
statement there. We also let $F$ be the (finite) set of terms appearing in
$\Sigma_{\rm BFB}$. Now the set $\operatorname{tp}_{k}({\bf A},a)$ contains
$\Sigma_{\rm BFB}$. Let $\Psi(x)$ be a formula in $\operatorname{tp}_{k}({\bf
A},a)$, and let $s(x,x_{1},\dots,x_{m})\approx t(x,x_{1},\dots,x_{m})$ be an
atomic subformula of $\Psi(x)$. By the first statement in Lemma 5.4, we have
that $s(x,x_{1},\dots,x_{m})\approx t(x,x_{1},\dots,x_{m})$ involves at most
$k+1$ distinct variables. Then by Birkhoff’s Finite Basis Theorem 2.5 there
are $s^{\prime},t^{\prime}\in F$ with

$\Sigma_{\rm BFB}\vdash s(x,x_{1},\dots,x_{m})\approx
s^{\prime}(x_{i_{0}},\dots,x_{i_{k}})\And t(x,x_{1},\dots,x_{m})\approx
t^{\prime}(x_{i_{0}},\dots,x_{i_{k}}),$

for some subset
$\\{x_{i_{0}},\dots,x_{i_{k}}\\}\subseteq\\{x,x_{1},\dots,x_{m}\\}$. Thus in
the presence of $\Sigma_{\rm BFB}$, the subformula
$s(x,x_{1},\dots,x_{m})\approx t(x,x_{1},\dots,x_{m})$ is equivalent to the
formula $s^{\prime}(x_{i_{0}},\dots,x_{i_{k}})\approx
t^{\prime}(x_{i_{0}},\dots,x_{i_{k}})$, showing that $\Psi(x)$ is equivalent
to one in which all terms have height at most the maximum height of the terms
in $F$. Thus, by the second part of Lemma 5.4, the set
$\operatorname{tp}_{k}({\bf A},a)$ is logically equivalent to the finite
subset consisting of $\Sigma_{\rm BFB}$ along with all members of
$\operatorname{tp}_{k}({\bf A},a)$ whose terms are of height at most $n$. ∎

The following is essentially Theorem 3.15 of Libkin [39] in the algebraic
setting. As the (easy) proof is unchanged we omit it, though comment that the
sentence $\alpha_{k}(x)$ is of course just the conjunction of the members of
the finite subset of $\operatorname{tp}_{k}({\bf A},a)$ identified as
equivalent to $\operatorname{tp}_{k}({\bf A},a)$ in Lemma 5.6.

######  Lemma 5.7.

For any finite algebra ${\bf A}$ and element $a\in A$ there is a rank $k$
formula $\alpha_{k}(x)$ such that ${\bf A}\models\alpha_{k}(a)$ and any
similar algebra ${\bf B}$ with $b\in B$ satisfying $\alpha_{k}(b)$ has
$\operatorname{tp}_{k}({\bf B},b)=\operatorname{tp}_{k}({\bf A},a)$.

We shall prove the equivalence of (1) and (2) in Theorem 5.1, as well as the
following the back-and-forth equivalence (a standard step in this argument,
define here for convenience).

######  Definition 5.8.

We inductively define the back-and-forth relations $\simeq_{k}$ on finite
$\mathcal{F}$-structures ${\bf A}$ and ${\bf B}$ as follows.

  * •

${\bf A}\simeq_{0}{\bf B}$ iff ${\bf A}\equiv_{0}{\bf B}$; that is, ${\bf A}$
and ${\bf B}$ satisfy the same atomic sentences.

  * •

${\bf A}\simeq_{k+1}{\bf B}$ iff the following two conditions hold:
forth: for every $a\in{\bf A}$, there exists $b\in{\bf B}$ such that $({\bf
A},a)\simeq_{k}({\bf B},b)$.
back: for every $b\in{\bf B}$, there exists $a\in{\bf A}$ such that $({\bf
A},a)\simeq_{k}({\bf B},b)$.

The following extension of Theorem 5.1 now follows using the standard proof.

######  Theorem 5.9.

Let ${\bf A}$ and ${\bf B}$ be two finite structures of the same signature.
Then the following are equivalent:

  1. (1)

${\bf A}$ and ${\bf B}$ agree on FO[$k$].

  2. (2)

${\bf A}\equiv_{k}{\bf B}$

  3. (3)

${\bf A}\simeq_{k}{\bf B}$

###### Proof.

We omit the proof, as the one given by Libkin for [39, Theorem 3.18] (for
example) holds close to verbatim, with the only adjustments for algebraic
setting having occurred in the adjusted proof of Lemma 5.7 and its corollary
Lemma 5.6 (which are used in the proof of $(1)\implies(3)$), and in the
meaning of the relations $\equiv_{k}$, $\simeq_{k}$. We note that the primary
difference in the meaning of $\equiv_{k}$, $\simeq_{k}$ manifests at the
trivial base step: a statement

$({\bf A},a_{1},\dots,a_{n})\simeq_{0}({\bf B},b_{1},\dots,b_{n})$

(which is the base $\simeq_{0}$ assumption that relation $\simeq_{n}$ is
founded on) is equivalent to $\operatorname{Sg}^{\bf A}(a_{1},\dots,a_{n})$
being isomorphic to $\operatorname{Sg}^{\bf B}(b_{1},\dots,b_{n})$ under the
map sending each $a_{i}$ to the corresponding $b_{i}$. But this matches our
game-based definition of $\equiv_{0}$ and of agreement on
$\operatorname{FO}[0]$. ∎

Finally, we prove the final statement in Theorem 5.2, showing completeness of
the method for detecting failure of first order definability within uniformly
locally finite classes of finite algebras. We do this by proving the
contrapositive: a property $\mathcal{P}$ of a uniformly locally finite class
of finite algebras $\mathscr{U}$ is expressible in FO iff there exists a
number $k$ such that for every two algebras ${\bf A}$ and ${\bf B}$ in
$\mathscr{U}$, if ${\bf A}\in\mathcal{P}$ and ${\bf A}\equiv_{k}{\bf B}$, then
${\bf B}\in\mathcal{P}$.

###### Proof of final, statement in Theorem 5.2..

Let ${\bf A}$ and ${\bf B}$ be in the uniformly locally finite $\mathscr{U}$.
If $\mathcal{P}$ is expressible by a FO sentence $\Phi$, let
$\operatorname{qr}(\Phi)=k$. If ${\bf A}\in\mathcal{P}$, then ${\bf
A}\models\Phi$, and hence for ${\bf B}$ with ${\bf A}\equiv_{k}{\bf B}$ we
have ${\bf B}\models\Phi$. Thus ${\bf B}\in\mathcal{P}$.

Conversely, if ${\bf A}\in\mathcal{P}$ and ${\bf A}\equiv_{k}{\bf B}$ imply
${\bf B}\in\mathcal{P}$, then any two algebras in $\mathscr{U}$ with the same
rank-$k$ type agree on $\mathcal{P}$. Now, as $\mathscr{U}$ is a uniformly
locally finite class of finite algebras, there is a bound on the size of the
$n$-generated algebras and so there are only finitely many different rank-$k$
types. Thus, for every pair of algebras in $U$ with the same rank-$k$ type,
there exists a rank-$k$ formula, namely $\alpha_{k}(x)$ defined in Lemma 5.7,
such that ${\bf A}\models\alpha_{k}(a)$ iff ${\bf B}\models\alpha_{k}(b)$.
Hence $\mathcal{P}$ is just a disjunction of some of the $\alpha_{k}$’s (those
witnessed by members of $\mathscr{U}$). ∎

To conclude this section, we mention a further useful trick for demonstrating
non first order definability, that calls on the classical model theoretic
ultraproduct. This simple but effective idea has been used recently by Czédli
[15, §2] for example; we give the proof for completeness.

######  Lemma 5.10.

Let $\mathscr{K}$ be a class of finite structures such that for all large
enough $n$ there are finite structures $\mathbf{A}_{n}\in\mathscr{K}$ and
${\bf B}_{n}\notin\mathscr{K}$ for which there is an ultraproduct
$\prod_{n}{\bf A}_{n}/\mathscr{U}\cong\prod_{n}{\bf B}_{n}/\mathscr{U}$. Then
$\mathscr{K}$ is not first order definable at the finite level.

###### Proof.

Any first order sentence true of $\mathscr{K}$ is true of all of the
$\mathbf{A}_{n}$, and then of $\prod_{\mathbb{N}/\mathscr{U}}{\bf A}_{n}$, and
therefore of cofinitely many of the $\mathbf{B}_{n}$. Hence $\phi$ does not
define $\mathscr{K}$. ∎

An example usage of this lemma will be in Proposition 7.3 below.

##  6\. A first order definable pseudovariety that is not definable by a
$\forall^{*}\exists^{*}$ sentence.

The construction of a finite algebra with Variety membership problem in
$\operatorname{FO}$ is based on an idea used in Clark, Davey, Jackson and
Pitkethly [13, Theorem 4.2]: the congruence classes of any congruence on a
finite lattice are intervals. The result in [13] extends beyond finite
algebras to infinite Boolean topological algebras, but in the restriction to
finite structures only it suffices to have just a semilattice $\wedge$, as we
now prove.

######  Theorem 6.1.

If $\\{{\bf L}_{1},\dots,{\bf L}_{k}\\}$ is a finite set of semilattice-based
finite algebras, then the class $\mathsf{SP}_{\rm fin}^{+}(\\{{\bf
L}_{1},\dots,{\bf L}_{k}\\})$ is the class of finite models of a
$\forall^{*}\exists^{*}\forall^{*}$ sentence in first order logic. The same is
true for $\mathsf{SP}_{\rm fin}(\\{{\bf L}_{1},\dots,{\bf L}_{k}\\})$.

Before proving Theorem 6.1 we prove a lemma. With minor modifications, this
lemma (and then Theorem 6.1) can be adapted to include relations.

######  Lemma 6.2.

Let $\mathscr{L}$ be the class of finite algebras in some finite signature
including a binary operation $\wedge$ with respect to which, all members of
$\mathscr{L}$ are semilattices. Fix any ${\bf L}\in\mathscr{L}$. Then there is

  * •

a first order $\exists^{*}\forall^{*}$-sentence $\Xi_{\bf L}$ asserting the
existence of a surjective homomorphism onto ${\bf L}$,

  * •

a first order $\exists^{*}\forall^{*}$-formula ${\not\equiv_{\bf L}}(x,y)$
(written $x\not\equiv_{\bf L}y$) in two free variables such that for every
member ${\bf K}\in\mathscr{L}$ and every pair $a\neq b$ in $K$, we have that
there is a homomorphism $\phi$ from ${\bf K}$ onto ${\bf L}$ with
$\phi(a)\neq\phi(b)$ if and only if ${\bf K}\models a\not\equiv_{\bf L}b$.

###### Proof.

This is essentially a version of the first part of the proof of [13, Theorem
4.2]. Let the universe of ${\bf L}$ be denoted $\\{1,2,\dots,\ell\\}$. When
there is a surjective homomorphism $\phi:{\bf K}\to{\bf L}$, then the kernel
of $\phi$ can be understood entirely using the minimal elements of each
congruence class: two elements $a,b$ are equivalent modulo this kernel if and
only if they sit above precisely the same minimal elements:
$\operatornamewithlimits{\hbox{\Large$\&$}}_{1\leq i\leq\ell}(a\geq
x_{i}\leftrightarrow b\geq x_{i})$, where the $x_{i}$ are variables that will
later be existentially quantified over some larger expression; on satisfaction
of this expression, the $x_{i}$ variables will eventually evaluate as minimal
elements in congruence classes. We denote this relation by $\equiv_{L}$
(without boldface), noting that it is clearly an equivalence relation subject
to any evaluation of the variables $x_{1},\dots,x_{\ell}$. Notationally we
write $a\equiv_{L}b$. The fact that the kernel is a congruence on ${\bf K}$
can be asserted by the property that for each operation $f$, of arity $n$ say,
we have

$\forall a_{1},\dots,a_{n},b_{1},\dots,b_{n}\
\Big{(}\operatornamewithlimits{\hbox{\Large$\&$}}_{j=1}^{n}a_{j}\equiv_{L}b_{j}\Big{)}\rightarrow
f(a_{1},\dots,a_{n})\equiv_{L}f(b_{1},\dots,b_{n})$

The fact that $\phi$ maps onto ${\bf L}$ can also be asserted using
$\equiv_{L}$: for each fundamental operation $f$ (again, of arity $n$, say),
and for each value $f(i_{1},\dots,i_{n})=j$ in ${\bf L}$ we require
$f(x_{i_{1}},\dots,x_{i_{n}})\equiv_{L}x_{j}$; now take the conjunction over
$j=1,\dots,\ell$ and existentially quantify $x_{1},\dots,x_{\ell}$. We have
created the $\exists^{*}\forall^{*}$ sentence $\Xi_{\bf L}$ asserting that
there is a surjective homomorphism from ${\bf K}$ onto ${\bf L}$. We wished to
define the corresponding relation $\not\equiv_{\bf L}$ (now with boldface and
negated). To do this, we introduce two free variables $x,y$ and include
$\neg(x\equiv_{L}y)$ as a further conjunct within $\Xi_{\bf L}$. ∎

Now we may prove Theorem 6.1.

###### Proof of Theorem 6.1.

An algebra ${\bf A}$ is in the universal Horn class of $\\{{\bf
L}_{1},\dots,{\bf L}_{k}\\}$ if and only if there is at least one homomorphism
from ${\bf A}$ to one of the ${\bf L}_{i}$ and the following “separation
properties” hold: whenever $a,b\in A$ have $a\neq b$, there is an
$i\in\\{1,\dots,k\\}$ and homomorphism from ${\bf A}$ to ${\bf L}_{i}$ with
$\phi(a)\neq\phi(b)$. As $\\{{\bf L}_{1},\dots,{\bf L}_{k}\\}$ is a finite set
of finite algebras, we may enumerate the set of all subalgebras ${\bf
L}^{\prime}_{1},\dots,{\bf L}_{m}^{\prime}$. The following sentence (referring
to the sentences defined in Lemma 6.2) asserts the required properties:

$\Big{(}\bigvee_{1\leq i\leq m}\Xi_{{\bf L}^{\prime}_{i}}\Big{)}\And\forall
a\forall b\Big{(}a\not\approx b\rightarrow\bigvee_{1\leq i\leq
m}a\not\equiv_{{\bf L}^{\prime}_{i}}b\Big{)}$

Because $\Xi$ and $\not\equiv$ are $\exists^{*}\forall^{*}$, this disjunction
is a $\forall^{*}\exists^{*}\forall^{*}$-sentence. Once the semilattice axioms
for $\wedge$ have been incorporated, we have a single sentence defining
$\mathsf{SP}_{\rm fin}^{+}(\\{{\bf L}_{1},\dots,{\bf L}_{k}\\})$. The sentence
for $\mathsf{SP}_{\rm fin}(\\{{\bf L}_{1},\dots,{\bf L}_{k}\\})$ is the same
except that we do not include the $\bigvee_{1\leq i\leq k}\Xi_{{\bf
L}^{\prime}_{i}}$ conjunct. ∎

As a corollary of Theorem 6.1 we prove that the JP Problem is true for
algebras with a semilattice operation; this follows already from Willard’s
Finite Basis Theorem [52], but the relative simplicity of our proof is
suggestive of the possibility of more accessible results of this kind in the
finite realm.

######  Corollary 6.3.

If ${\bf A}$ is a finite semilattice-based algebra generating a pseudovariety
with only finitely many subdirectly irreducible members, then the
pseudovariety of ${\bf A}$ is definable in first order logic amongst finite
structures.

###### Proof.

Let ${\bf A}_{1}$, …, ${\bf A}_{k}$ be a complete list of the subdirectly
irreducible members of the variety of ${\bf A}$ (all finite). Because every
algebra is a subdirect product of its subdirectly irreducible quotients, the
pseudovariety generated by ${\bf A}$ coincides with $\mathsf{SP}_{\rm
fin}(\\{{\bf A}_{1},\dots,{\bf A}_{k}\\})$. Now apply Theorem 6.1. ∎

The _flat extension_ of an algebra ${\bf A}$ is the algebra $\flat({\bf A})$
formed over the universe $A\cup\\{0\\}$ (considered as a disjoint union;
rename elements of $A$ if necessary) and with the signature of ${\bf A}$
augmented by a further binary operation $\wedge$ (again, rename existing
operations if necessary). The existing operations of ${\bf A}$ are extended to
$0$ by making $0$ an absorbing element, and the operation $\wedge$ is defined
by

$x\wedge y=\begin{cases}x&\mbox{ if }x=y\\\ 0&\mbox{ otherwise.}\end{cases}$

The variety $\mathsf{HSP}(\flat({\bf A}))$ generated by the flat extension of
a finite algebra ${\bf A}$ (or even partial algebra), has some relationship to
the universal Horn class $\mathsf{SP}^{+}({\bf A})$ of the original algebra
${\bf A}$ [25, 51]. The relationship is particularly precise in the case that
${\bf A}$ has a binary term function acting as a projection: that is, there is
a binary term function $\triangleright$ such that $x\triangleright y=y$ for
every $x$ and $y$. In this situation, the subdirectly irreducible members of
$\mathsf{HSP}(\flat({\bf A}))$ are precisely the flat extensions of the
algebras in the universal Horn class of ${\bf A}$; see [25, §5]. Much of this
can be explained using the ternary term $(x\wedge y)\triangleright z$. On the
algebra $\flat({\bf A})$, this term acts as follows:

$(x\wedge y)\triangleright z=\begin{cases}z&\mbox{ if }x=y\neq 0\\\ 0&\mbox{
otherwise}.\end{cases}$

In [25, §5] a ternary term with this property is called a _pointed semi-
discriminator function_ and an algebra is said to be a _pointed semi-
discriminator algebra_ if it has an absorbing element $0$ and a term function
acting as a pointed semi-discriminator function. It is routine to show that
(up to isomorphism), pointed semi-discriminator algebras are exactly those
that are term equivalent to flat extensions of partial algebras with a binary
projection operation $\triangleright$. A variety $\mathscr{V}$ is a _pointed
semi-discriminator variety_ if there is a ternary term $p(x,y,z)$ such that
$\mathscr{V}$ can be generated by algebras on which the term $p$ acts as a
pointed semi-discriminator operation; equivalently, if the subdirectly
irreducible members of $\mathscr{V}$ are pointed semi-discriminator algebras
with respect to $p$. It is shown in [25, Theorem 5.8] that a complete
axiomatisation for the pointed semidiscriminator variety over all partial
algebras in signature $\mathscr{L}$ is given by the semilattice laws for
$\wedge$:

$x\wedge(y\wedge z)\approx(x\wedge y)\wedge z,\ x\wedge y\approx y\wedge x,\
x\wedge x\approx x,$

the right normal band laws for $\triangleright$:

$x\triangleright(y\triangleright z)\approx(x\triangleright y)\triangleright
z,\ x\triangleright(y\triangleright z)\approx y\triangleright(x\triangleright
z),\ x\triangleright x\approx x,$

the laws

$(x\wedge y)\triangleright z\approx x\wedge y,\ (x\triangleright y)\wedge
z\approx x\triangleright(y\wedge z)$

and the laws

$x\triangleright f(x_{1},\dots,x_{i},\dots,x_{n})\approx
f(x_{1},\dots,x\triangleright x_{i},\dots,x_{n})$

for each operation symbol $f\in\mathscr{L}\cup\\{\wedge,\triangleright\\}$ (of
arity $n$) and each $1\leq i\leq n$. The lattice of subvarieties of this
variety is isomorphic to the lattice of universal Horn subclasses of the class
of all partial algebras in the signature $\mathscr{L}$ ([25, Corollary 5.4]).
There is no loss of generality to these facts if the element $0$ is included
in the signature as a distinguished nullary satisfying the absorption laws for
$0$ with respect to all operations: all finite models and all subdirectly
irreducible members of a pointed semidiscriminator variety have this $0$. We
use the suffix “with $0$” to describe this amendment; it is included in a
nonessential way in the next lemma.

######  Lemma 6.4.

The pointed semidiscriminator variety with $0$ over any finite signature
$\mathscr{L}$ has definable cmi congruences. More precisely, if
$\pi_{1}(x,y,u,v)$ denotes the formula

$[((x\wedge y)\triangleright u\approx u)\vee(x\triangleright u\not\approx
u\And v\triangleright u\not\approx u)],$

then the formula

$\pi(x,y,u,v):=x\approx y\vee(u\not\approx u\wedge
v\And\pi_{1}(x,y,u,v))\vee(v\not\approx u\wedge v\And\pi_{1}(x,y,v,u))$

defines cmi congruences in the variety of pointed semi-discriminator algebras
over $\mathscr{L}$.

###### Proof.

This is established in the proof of Theorem 3.1(3) in [25]: see the argument
starting in paragraph three of the proof, where this congruence is described
in written form, and it is subsequently verified that the corresponding
quotient is subdirectly irreducible. Note that the proof in [25] is in a more
general context and uses expressions such as $\lambda(c\wedge d)=a$, where
$\lambda$ is an arbitrary translation. In the pointed semidiscriminator
setting, the property $\lambda(c\wedge d)=a$ is equivalent to $(c\wedge
d)\triangleright a=a$, which in the logical syntax given in the lemma
statement appears in subexpressions such as $((x\wedge y)\triangleright
u\approx u)$. ∎

We can now give the main result of the section.

######  Theorem 6.5.

Let ${\bf L}$ be a finite partial algebra (possibly total) with a semilattice
reduct and a projection term. Then the pseudovariety generated by $\flat({\bf
L})$ with distinguished $0$ is definable by a
$\forall^{*}\exists^{*}\forall^{*}$ sentence of first order logic.

###### Proof.

The subdirectly irreducible members of the pseudovariety of $\flat({\bf L})$
are just the flat extensions (with $0$ distinguished) of the members of the
universal Horn class of ${\bf L}$. By Theorem 6.1, the class
$\mathsf{SP}^{+}_{\rm fin}({\bf L})$ is first order definable by a
$\forall^{*}\exists^{*}\forall^{*}$ sentence $\forall x\forall y\ \Phi(x,y)$
where $\Phi(x,y)$ is an $\exists^{*}\forall^{*}$ sentence. The class of flat
extensions of members of this class can then be defined in first order logic
by asserting that the structure is flat, with bottom element $0$ (this uses
only universal quantifiers), and that $\forall x\forall y\ \Phi(x,y)$ holds
for all elements that are not $0$: for every variable $z$ in $\forall x\forall
y\ \Phi(x,y)$ we must include $\neg(z\approx 0)$. This is where having $0$ is
a constant is required; otherwise we would be required to existentially
quantify the existence of a zero element, adding an extra layer of quantifier
alternation to the sentence. Thus we have a sentence $\Psi$ defining the
subdirectly irreducible members of $\mathsf{HSP}_{\rm fin}(\flat({\bf L}))$.
We could now try to apply the one-to-many first order reduction of Theorem
3.5, but this calls on a linear order, which is acceptable from a complexity-
theoretic perspective, but steps outside of pure first order logic of the
algebras in consideration. We can avoid this entirely using the formula
$\pi(x,y,u,v)$ of Lemma 6.4. Let $\theta_{a,b}$ denote the congruence relation
defined by $\pi(a,b,u,v)$. For a model ${\bf K}$ we wish to assert that
$\forall a\forall b\ {\bf K}/\theta_{a,b}\models\Psi$. Let $\Psi^{\flat}(a,b)$
denote the result of replacing every instance of equality $u\approx v$ in
$\Psi$ by $\pi(a,b,u,v)$ (here $u$ and $v$ refer to any terms related by
equality in $\Psi$). Then $\forall a\forall b\ {\bf
K}/\theta_{a,b}\models\Psi$ is equivalent to

${\bf K}\models\forall a\forall b\ \neg(a\approx
b)\rightarrow\Psi^{\flat}(a,b).$

Thus the sentence $\forall a\forall b\ \neg(a\approx
b)\rightarrow\Psi^{\flat}(a,b)$ along with the equational axioms defining
pointed semidiscriminator varieties with $0$, define $\mathsf{HSP}_{\rm
fin}(\flat({\bf L}))$ amongst finite algebras. ∎

There are examples of lattices ${\bf L}$ for which $\mathsf{SP}({\bf L})$ has
no finite basis for its universal Horn theory: Belkin [3] has shown that the
10-element lattice $M_{3{-}3}$ has this property for example (noting that
$\mathsf{SP}({\bf L})$ and $\mathsf{SP}^{+}({\bf L})$ coincide for any
lattice). As lattices are semilattice based and have a projection term
$t(x,y):=x+x\wedge y$ (using $+$ for join, to avoid conflict with the logical
$\vee$), we have that $\mathsf{HSP}(\flat({\bf L}))$ (with $0$) has no finite
axiomatisation in first order logic. Theorem 6.5 above gives us the following
result.

######  Corollary 6.6.

If ${\bf L}$ is a finite lattice without a finite basis for its universal Horn
theory, then $\flat({\bf L})$ with $0$ generates a nonfinitely based variety
that is first order definable by a $\forall^{*}\exists^{*}\forall^{*}$
sentence amongst finite algebras.

Thus we have our simultaneous failure of the $\mathsf{S}$, $\mathsf{SP}$ and
$\mathsf{HSP}$ preservation theorems at the finite level.

It is also easy to see that the pseudovariety of $\flat({\bf L})$ with $0$ has
no finite axiomatisation by pseudoequations.

######  Corollary 6.7.

If ${\bf L}$ is a lattice without a finite basis for its universal Horn
theory, then the pseudovariety generated by $\flat({\bf L})$ with $0$ is
finitely axiomatisable by a $\forall^{*}\exists^{*}\forall^{*}$ sentence of
first order logic, but not finitely axiomatisable by pseudo-equations.

###### Proof.

Let $\Sigma$ be a finite set of pseudoequations holding in $\flat({\bf L})$
with $0$, and let $k$ be the number of variables appearing in $\Sigma$.
Because ${\bf L}$ has no finite basis for its equational theory, for each $n$
there exists a lattice ${\bf L}_{n}$ that lies outside of the universal Horn
class of ${\bf L}$ but whose $n$-generated sublattices lie within the
universal Horn class of ${\bf L}$. Because ${\bf L}$ has a finite basis for
its equational theory, there is no loss of generality in assuming that the
lattices ${\bf L}_{n}$ lie within the variety of ${\bf L}$, and so are finite.
Then $\flat({\bf L}_{n})$ lies outside of the pseudovariety of $\flat({\bf
L})$, but its $n$-generated subalgebras lie within the pseudovariety of
$\flat({\bf L})$. Then $\flat({\bf L}_{k})$ satisfies $\Sigma$, showing that
$\Sigma$ is not a basis by pseudoequations. ∎

As alluded to in Subsection 1.3, it would be interesting to see whether the
pseudovariety of $\flat({\bf L})$ can be defined by a finite set of equation
systems in the sense of Higgins and the second author [22].

##  7\. Pseudovariety membership complexity: Constraint Satisfaction Problems

There has been little exploration of fine level membership for $\textsf{var-
mem}(*,\mathbf{A})$ within tractable cases. In [29], the authors show that
$\textsf{var-mem}(*,\mathbf{L})$ is in NL for Lyndon’s algebra ${\bf L}$. In
[50] it is shown that a certain six-element semigroup $AC_{2}$ (also known as
$A_{2}^{g}$ [38], and not to be confused with the complexity class
$\texttt{AC}^{2}$) has $\textsf{var-mem}(*,AC_{2})$ solvable in polynomial
time. At the end of this section we show that their characterisation of the
pseudovariety of $AC_{2}$ in fact leads to NL solvability of $\textsf{var-
mem}(*,AC_{2})$, but that it does not lie in FO. In the present section we
translate CSP complexity into var-mem complexity, thereby providing a wealth
of examples within tractable complexity. For example, in [27, §10] it is shown
that there are infinitely many tractable complexity classes represented by
constraint problems of the kind we translate: as well as commonly encountered
classes such as L, NL, there are the classes
$\operatorname{Mod}_{p}(\texttt{L})$ for any prime $p$, and problems of
complexity in the $\cap/\cup$ closure of any combination of these.

Let $\mathbb{A}$ be a finite relational structure of finite signature. The
constraint satisfaction problem over $\mathbb{A}$ is the computational problem
defined as follows.

$\operatorname{CSP}(\mathbb{A})$
Instance: a finite structure $\mathbb{B}$ of the same signature as
$\mathbb{A}$.
Question: is there a homomorphism from $\mathbb{B}$ into $\mathbb{A}$?

We direct the reader to the collection [37] for a small sample of the wealth
of literature on the $\operatorname{CSP}(\mathbb{A})$ problem.

The main result in this section is the following theorem.

######  Theorem 7.1.

For every finite relational structure $\mathbb{A}$ there is a finite algebra
$\mathbf{A}^{\prime}$ (not typically on the same universe) such that
$\operatorname{CSP}(\mathbb{A})$ and $\textsf{var-mem}(*,{\bf A}^{\prime})$
are first order equivalent.

###### Proof.

The proof is mostly a corollary of constructions in [25] and [31], though the
first order equivalence requires fresh arguments.

It is shown in [31, §4] that for every finite relational structure
$\mathbb{A}$ of finite signature, there is a structure $\mathbb{A}^{\sharp}$
of the same signature with the property that for all $\mathbb{B}$ we have
$\mathbb{B}\rightarrow\mathbb{A}$ if and only if
$\mathbb{B}\in\mathsf{SP}(\mathbb{A}^{\sharp})$. Thus every fixed finite
template CSP is a universal Horn class membership problem: they are identical
as problems.

Any relational structure $\mathbb{A}$ gives rise to a partial algebra
$\pi(\mathbb{A})$ by replacing each fundamental relation by the projection
partial function: if $R$ has arity $n$, then it is replaced by the first
projection function on domain $R^{\mathbb{A}}\subseteq A^{n}$. To ensure that
we arrive at a pointed semidiscriminator variety we also add a projection term
$\triangleright$; this is equivalent to asking that a degenerate total binary
relation be added as a fundamental relation on $\mathbb{A}$. In [25, §7.1] it
is explained that the subdirectly irreducible members of
$\mathsf{HSP}(\flat(\pi(\mathbb{A})))$ are just the isomorphism closure of
$\flat(\pi(\mathbb{B}))$ for $\mathbb{B}\in\mathsf{SP}(\mathbb{A})$. The
translations between $\mathbb{B}$ and $\flat(\pi(\mathbb{B}))$ and back again
are easily seen to be first order reductions, so the combined effect of these
observations is that every problem of the form
$\operatorname{CSP}(\mathbb{A})$ is first order equivalent to $\textsf{var-si-
mem}(*,\mathbf{A}^{\prime})$, where $\mathbf{A}^{\prime}$ is the algebra
$\flat(\pi(\mathbb{A}^{\sharp}))$. As $\textsf{var-si-
mem}(*,\mathbf{A}^{\prime})$ is a restriction of $\textsf{var-si-
mem}(*,\mathbf{A}^{\prime})$, to complete the proof it suffices to find a
first order reduction from $\textsf{var-mem}(*,\mathbf{A}^{\prime})$ to
$\operatorname{CSP}(\mathbb{A})$.

It would suffice to reduce $\textsf{var-mem}(*,\mathbf{A}^{\prime})$ to
$\textsf{var-si-mem}(*,\mathbf{A}^{\prime})$, but it is easier to reduce all
the way to $\operatorname{CSP}(\mathbb{A})$. The strategy is as follows. We
are given a general instance $\mathbf{B}$ of $\textsf{var-
mem}(*,\mathbf{A}^{\prime})$, and there is no loss of generality in assuming
that $\mathbf{B}$ satisfies the finitely many equations that define the
pointed semidiscriminator variety of appropriate signature. Now
$\pi(\mathbb{A}^{\sharp})$ satisfies implications $f(x_{1},\dots,x_{n})\approx
f(x_{1},\dots,x_{n})\rightarrow f(x_{1},\dots,x_{n})\approx x_{1}$ asserting
that each of its operations are partial projections. Each of these finitely
many laws also translates to an equation that holds on
$\flat(\pi(\mathbb{A}^{\sharp}))$ (see [25, Lemma 5.9]), and there is also no
loss of generality in assuming that $\mathbf{B}$ satisfies these. In this
case, all of the subdirectly irreducible quotients of $\mathbf{B}$ (one for
each pair $a\neq b$ in $B$; denote them by $\mathbf{B}_{a,b}$) will be
isomorphic to algebras of the form $\flat(\pi(\mathbb{B}_{a,b}))$, where
$\mathbb{B}_{a,b}$ is an input to $\operatorname{CSP}(\mathbb{A})$. We have
$\mathbf{B}\in\mathsf{HSP}({\bf A}^{\prime})$ if and only if
$\mathbb{B}_{a,b}$ is a YES instance of $\operatorname{CSP}(\mathbb{A})$ for
each $a\neq b$ in $B$. The reader satisfied with a one-to-many first order
reduction can now simply use the one-to-many reduction supplied by Theorem
3.5. But we can do slightly better, as the property that all of the structures
$\mathbb{B}_{a,b}$ are YES instances of $\operatorname{CSP}(\mathbb{A})$ is
equivalent to the single instance $\dot{\bigcup}_{a\neq b\text{ in
}B}\mathbb{B}_{a,b}$ being a YES instance of $\operatorname{CSP}(\mathbb{A})$,
and as we now show, this structure can be made as a single first order query.
We make essential recourse to the implicit linear order $<$ available in first
order query definition.

Let $\pi(a,b,x,y)$ be the formula defining cmi congruences. The universe of
$\mathbb{B}^{\prime}$ will defined as a subset of $B^{3}$, consisting of all
tuples $(a,b,c)$ where $a\neq b$, none of $a,b,c$ are $\infty$, and where $c$
is a $<$-minimum element in an equivalence class of the congruence
$\pi(a,b,x,y)$: so $\pi(a,b,c,d)\rightarrow c\leq d$. Each relation $R$ (of
arity $n$ say) corresponded to an operation $f_{R}$ in the signature of
$\mathbf{B}$ of the same arity, and we define $R$ on our defined universe as
all tuples $((a_{1},b_{1},c_{1}),\dots,(a_{n},b_{n},c_{n}))$ where
$a_{1}=a_{2}=\dots=a_{n}$, $b_{1}=b_{2}=\dots=b_{n}$ and
$\pi(a_{1},b_{1},f^{\mathbf{B}}(c_{1},\dots,c_{n}),c_{1})$. ∎

We finish this section by proving the claims around the semigroup $AC_{2}$ at
the start of section; the proof of the first claim simply involves verifying
that the algorithmic check from [50] can be performed on a nondeterministic
Turing machine in logspace. The proof of the second claim is by an application
of Lemma 5.10.

######  Proposition 7.2.

$\textsf{var-mem}(*,AC_{2})$ is in NL.

###### Proof.

A polynomial time algorithm for $\textsf{var-mem}(*,AC_{2})$ is given in
Section 3 of [50], and consists of checking finitely many equations (which is
first order, hence in L), then verifying that the subsemigroup generated by
idempotents has trivial subgroups. We may verify failure of this last property
in nondeterministic logspace as follows. First note that the single equation
$x^{2}\approx x^{4}$ ensures that all subgroups have exponent $2$ or are
trivial, and we tacitly assume this throughout. Next observe that the property
that there is a proper subgroup generated by some idempotent elements is
equivalent to the existence of idempotents $e_{1},e_{2},\dots,e_{k}$ with the
product $a:=e_{1}\dots e_{k}$ having $a^{3}=a$ but $a\neq a^{2}$. We can
discover this in nondeterministic logspace as follows. We use three small
sections of work tape, each logarithmic in size. We have a small section of
work tape to record the current value of a product $a$; initially it is empty.
We have a section to record a current idempotent guess $e$. We also have a
small section to check if the current product value $a$ satisfies $a^{3}=a$
but $a\neq a^{2}$. The algorithm proceeds by nondeterministically selecting an
element $e$ one by one at random, checking if $e$ is idempotent (this only
involves storing the current guess on the work tape and consulting the input
tape to see if the square of the listed element is identical to what we stored
as our guess). If the current guess $e$ is idempotent, we replace the current
product value $a$ by the new value $a\cdot e$. Note that we record just the
value of this product, not both the values $a$ and $e$. Then we check the
input to see if $a^{3}=a$ but $a\neq a^{2}$: if $a=a^{2}$ then this test has
failed, but otherwise we may write the value of $a^{2}$ to the third section
of our working tape, and then check if $a\cdot a^{2}=a$. If $a\cdot a^{2}\neq
a$ then we continue our search. If $a\cdot a^{2}=a$ then the input algebra is
not in the variety of $AC_{2}$. Because co-$\texttt{NL}=\texttt{NL}$ we have
$\textsf{var-mem}(*,AC_{2})$ is in NL. ∎

To complement Proposition 7.2 we now show that this example does not provide a
counterexample to the first order ES problem.

######  Proposition 7.3.

$\textsf{var-mem}(*,AC_{2})$ is not in FO.

###### Proof.

We give sketch details only, and direct the reader to [50] or to any semigroup
theory text (such as Clifford and Preston [14]) for definitions of Rees matrix
semigroups and their isomorphism theory. Let $C_{2}=\\{e,g\\}$ be a copy of
the $2$-element group with $g^{2}=e$. For each $n>2$, consider the Rees matrix
semigroup ${\bf A}_{n}$ over $C_{2}$ whose sandwich matrix is as follows:

$\left[\begin{matrix}e&e&0&0&\cdots&0&0\\\ 0&e&e&0&\cdots&0&0\\\
0&0&e&e&\cdots&0&0\\\ \vdots&\vdots&\vdots&&\ddots&\vdots&\vdots\\\
0&0&0&0&\cdots&e&e\\\ g&0&0&0&\cdots&0&e\\\ \end{matrix}\right].$

It is useful to think of this sandwich matrix as recording the adjacency
matrix of a labelled directed graph: $0$ entries correspond to no edge, while
nonzero edges are labelled by their value (either $e$ or $g$). Evidently the
directed graph for ${\bf A}_{n}$ is a directed $n$-cycle with loops at each
vertex; all labels are $e$ except for one that is $g$. The isomorphism theory
of Rees matrix semigroups shows that this is not a terribly stable
representation: for example the label $g$ can be moved to any other edge, but
worse than that, the entire graph structure can be changed. For our purposes
though, we may lock this $n$-cycle interpretation in by adding a relation to
our signature that records at least the underlying unlabelled graph: for
example we can include a binary relation $\sim$ to our signature that is
defined as linking idempotents corresponding to the diagonal entries in the
sandwich matrix according to how they should be linked in the adjacency matrix
definition. The general pattern of nonzero entries in the matrix can then be
recorded as a first order sentence in this expanded language: for example all
nonzero idempotents are either part of a $\sim$-edge, or they result as the
product of two idempotents $e$ and $f$ where $e\sim f$. Such properties, as
well as the property of being completely $0$-simple over $C_{2}$, will be
preserved by ultraproducts. We denote this expansion of ${\bf A}_{n}$ to the
added binary relation by ${\bf A}_{n}^{\prime}$.

Now let ${\bf B}_{n}$ denote the Rees matrix semigroup over $C_{2}$ with the
same sandwich matrix as for ${\bf A}_{n}$ except that the one entry labelled
$g$ is replaced by $e$. Again we can expand the signature to include $\sim$ as
described for ${\bf A}_{n}$, and denote the corresponding structure ${\bf
B}_{n}^{\prime}$. It is routine to show that ${\bf B}_{n}$ is in
$\mathsf{HSP}(AC_{2})$ and that ${\bf A}_{n}$ is not (it fails the condition
from [50] used in the proof of Proposition 7.2 for example). Let $\mathscr{U}$
be any nonprincipal ultrafilter over $\\{3,4,5,\dots\\}$. In order to deduce
that $\prod_{n}{\bf A}_{n}/\mathscr{U}\cong\prod_{n}{\bf B}_{n}/\mathscr{U}$
we observe that properties of the relation $\sim$ are also preserved in the
ultraproduct, and as ${\bf A}_{n}$ and ${\bf B}_{n}$ are identical on their
reduct to $\sim$, the inherited definition of $\sim$ on $\prod_{n}{\bf
A}_{n}^{\prime}/\mathscr{U}$ and $\prod_{n}{\bf B}_{n}^{\prime}/\mathscr{U}$
is also identical: the corresponding directed graph is a union of infinite
directed paths with loops on each vertex and with no terminal nor initial
vertices. This records an identical structure of nonzero entries in the
sandwich matrix for the two ultraproducts, and as the underlying directed
graph has no cycles (beyond the loops), the general isomorphism theory of Rees
matrix semigroups enables us to remove any entries that are not either $0$ or
$e$, leaving trivially isomorphic semigroups. By Lemma 5.10 we have that
$\mathsf{HSP}_{\rm fin}(AC_{2})$ is not definable by a first order sentence. ∎

##  8\. Undecidability of complexity of finite membership.

In a groundbreaking series of papers [40, 41, 42] Ralph McKenzie showed that
there is no algorithm to decide if a given finite algebra has a finite basis
for its equational theory, thereby solving Tarski’s long standing Finite Basis
Problem. Later, Willard [52] showed how the construction $A(\mathcal{T})$
(here $\mathcal{T}$ is a Turing machine program) of the second of these papers
[41] could be used to the same effect, thereby avoiding the much more
challenging construction $F(\mathcal{T})$ of [42]. It is natural to ask if the
finite model theoretic version of Tarski’s Finite Basis Problem is also
undecidable, especially in view of our examples from Section 6. In this
section we give a standalone proof demonstrating that McKenzie’s
$A(\mathcal{T})$ construction does indeed show the undecidability of
determining whether the pseudovariety of a finite algebra is first order
definable at the finite level.

######  Theorem 8.1.

The following problem is undecidable: given a finite algebra ${\bf A}$,
determine if the pseudovariety of ${\bf A}$ is first order definable at the
finite level.

###### Proof.

We show that the pseudovariety of $A(\mathcal{T})$ is first order definable if
and only if a Turing machine executing program $\mathcal{T}$ on the blank tape
eventually halts. For the “if” direction we need only know the fact that
$A(\mathcal{T})$ has a semilattice operation and that when the Turing machine
program $\mathcal{T}$ eventually halts on the blank tape, the variety of
$A(\mathcal{T})$ contains only finitely many subvarieties: this is [41,
Theorem 5.1]. Our Corollary 6.3 above implies first order definability of the
pseudovariety of $A(\mathcal{T})$ at the finite level, though of course we
could also have used the much more powerful [52] or [53].

Now we must show that when $\mathcal{T}$ does not halt, then the pseudovariety
of $A(\mathcal{T})$ is not first order definable. For this we need more
details of $A(\mathcal{T})$ and of some of the subdirectly irreducibles in the
pseudovariety of $A(\mathcal{T})$. The algebra $A(\mathcal{T})$ has a very
large number of operations and elements, but our arguments will mainly centre
on the multiplication operation, which is remarkably simple. There is a
multiplicative $0$ element, and the only nonzero products exist amongst just 7
of the elements: $1,2,H,C,\bar{C},D,\bar{D}$, with only $1\cdot C=C$,
$1\cdot\bar{C}=\bar{C}$, $2\cdot D=H\cdot C=D$ and
$2\cdot\bar{D}=H\cdot\bar{C}=\bar{D}$.

Claim 1.

$A(\mathcal{T})\models x_{0}(x_{1}(x_{2}\dots
x_{i}(x_{i+1}(\dots(x_{n-1}(x_{0}y))\dots))\dots))\approx\\\
x_{0}(x_{1}(x_{2}\dots x_{i+1}(x_{i}(\dots(x_{n-1}(x_{0}y))\dots))\dots))$

for each $n>3$ and $0<i<n-2$.

###### Proof of Claim 1..

Assume that the left hand side is nonzero. So $y$ is amongst
$C,\bar{C},D,\bar{D}$, and as the barred elements are simply duplicates of
their unbarred versions, it suffices to assume that $y=C$ or $y=D$. If $y=D$,
then consulting the nonzero products, it is clear that
$x_{0}=x_{1}=\dots=x_{n-1}=2$ and both sides of the equation take the value
$D$. Now assume that $y=C$. Then $x_{1}$ cannot be $H$ because $H\cdot C=D$,
forcing $x_{n-1}=x_{n-2}=\dots=x_{1}=x_{0}=2$, contradicting $x_{0}=H$. So
$x_{0}=1$. Because the left hand side is nonzero and of the form $x_{0}\cdot
t$ for some term $t$, it follows that $t$ takes the value $C$, which again
forces $x_{0}=x_{1}=\dots=x_{n-1}=1$, and both sides are again equal. ∎

Now we recall the structure of some of the large finite subdirectly
irreducibles in the variety of $A(\mathcal{T})$: specifically, the algebras
denoted $S_{n}$ by McKenzie [41, Definition 4.1]. The elements are
$0,a_{0},\dots,a_{n-1},b_{0},\dots,b_{n}$, and almost all of the complex array
of operations in the signature are constantly equal to $0$, except for
multiplication: $a_{i}\cdot b_{i+1}=b_{i}$ (and $0$ for all other pairs) and
the semilattice $\wedge$, with

$x\wedge y=\begin{cases}x&\text{ if $x=y$}\\\ 0&\text{ otherwise,}\end{cases}$

and three further operations, which conveniently are just term functions in
$\cdot$ and $\wedge$. In the case where $\mathcal{T}$ does not halt, the
subdirectly irreducible algebra $S_{n}$ lies in the variety of
$A(\mathcal{T})$ for every $n$. We now consider a distorted version of
$S_{n}$, which we call $T_{n}$: it is an extension of $S_{n}$ to include some
new elements $c_{0},\dots,c_{n-1}$ and $d_{0},\dots,d_{n-1}$, with the same
multiplication pattern, $c_{i}\cdot d_{i\oplus 1}=d_{i}$, except now
interpreted modulo $n$ (here $\oplus$ denotes addition modulo $n$). The
semilattice $\wedge$ is also flat, and all other operations share their
previous definitions, as constantly equal to $0$ or as term functions in
$\cdot,\wedge$. In either of $S_{n}$ or $T_{n}$, we will refer to elements of
the form $a_{i}$ and $c_{i}$ as being of _$a$ -type_, and elements of the form
$b_{i}$ and $d_{i}$ as being of _$b$ -type_. (So, the $a$-type elements of
$S_{n}$ are $a_{0},\dots,a_{n-1}$, whereas the $a$-type elements of $T_{n}$
are $a_{0},\dots,a_{n-1},c_{0},\dots,c_{n-1}$.)

Claim 2. $T_{n}\notin\mathsf{HSP}_{\rm fin}(A(\mathcal{T}))$.

###### Proof of Claim 2..

This is because $T_{n}$ fails the law in Claim 1: assign $x_{i}$ to $c_{i}$
and $y$ to $d_{1}$: the left hand side equals $b_{0}$, while the right hand
side equals $0$. ∎

We can now use Ehreunfeuct-Fraïssé games on the algebras $S_{n}$ and $T_{n}$
to show that $\mathsf{HSP}_{\rm fin}(A(\mathcal{T}))$ is not first order
definable. Note that we do not need to show that there exists a uniformly
locally finite class containing $S_{n}$ and $T_{n}$, as this only guarantees
that an Ehrenfeucht-Fraïssé game is a possible approach to proving non first
order definability.

Both $S_{n}$ and $T_{n}$ have very weak generation power, in the sense that no
new indices of elements can be generated from those already present in a set
of generators: the only nonzero products are $a_{i}\cdot b_{i+1}=b_{i}$ and
$c_{i}\cdot d_{i\oplus 1}=d_{i}$ in $T_{n}$. These indices can also be used to
determine a weak notion of distance: the difference in index suffices, though
in the case of $T_{n}$ we will additionally count elements of the form $a_{j}$
or $b_{j}$ as having infinite distance from elements of type $c_{j^{\prime}}$
or $d_{j^{\prime}}$. At this point, readers familiar with Ehrenfeucht-Fraïssé
games will see immediately that Duplicator has a winning strategy in the
$k$-round game provided $n$ is large enough. Readers unfamiliar with the idea
are best served by consulting a text: in particular, Figure 3.4 of Libkin [39]
and accompanying text presents a situation that is almost identical, save for
the fact that in our situation Duplicator must additionally match the correct
type of element to that chosen by Spoiler: a choice of $a$-type by Spoiler
requires Duplicator to choose $a$-type and likewise for $b$-type. ∎

## References

  * [1] N. Alechina and Yu. Gurevich, Syntax vs. semantics on finite structures, in _Structures in Logic and Computer Science. A Selection of Essays in Honor of A. Ehrenfeucht_ , Springer, 1997, pp. 14–33.
  * [2] J. Almeida, Finite Semigroups and Universal Algebra
  * [3] V.P. Belkin, Quasi-identities of finite rings and lattices, Algebra Logika 17 (1978) 247–259 (in Russian).
  * [4] C. Bergman, Universal Algebra: Fundamentals and Selected Topics, Chapman Hall/CRC Press, 2011.
  * [5] C. Bergman and G. Slutzki, Complexity of some problems concerning varieties and quasi-varieties of algebras, SIAM J. Comput. 30 (2000), 359–382.
  * [6] C. Bergman and G. Slutzki, Computational complexity of some problems involving congruences on algebras. 15th Annual IEEE Symposium on Logic in Computer Science (Santa Barbara, CA, 2000), 168–174, IEEE Comput. Soc. Press, Los Alamitos, CA, 2000.
  * [7] C. Bergman and G. Slutzki, Computational complexity of some problems involving congruences on algebras, Theoret. Comp. Sci. 270 (2002), 591–608.
  * [8] G. Bezhanishvili, Locally finite varieties, Algebra Universalis 46 (2001), 531–548.
  * [9] G. Birkhoff, On the structure of abstract algebras, Math. Proc. Cambridge Phil. Soc. 31 (1935), 433–454.
  * [10] J. Bulín, D. Delic, M. Jackson and T Niven, A finer reduction of constraint problems to digraphs, Log. Methods Comp. Sci. 11 (2015), 1–33.
  * [11] S. Burris and H.P. Sankappanavar, A Course in Universal Algebra, Graduate Texts in Mathematics 78, Springer Verlag, 1980.
  * [12] D.M. Clark, B.A. Davey, R.S. Freese, M. Jackson, Standard topological algebras: Syntactic and principal congruences and profiniteness, Algebra Universalis 52 (2004) 343–376.
  * [13] D.M. Clark, B.A. Davey, M.G. Jackson and J.G. Pitkethly, The axiomatizability of topological prevarieties, Adv. Math. 218 (2008), 1604–1653.
  * [14] Clifford A.H. and G.B. Preston, The algebraic theory of semigroups, Vol. I, AMS Mathematical Surveys, (1961).
  * [15] G. Czédli, Cyclic congruences of slim semimodular lattices and non-finite axiomatizability of some finite structures, Arch. Math. (Brno) 58 (2022), 15–33.
  * [16] J. Demel, M. Demlová and V. Koubek, Fast algorithms constructing minimal subalgebras, congruences and ideals in a finite algebra, Theoret. Comp. Sci. 36 (1985), 203–216.
  * [17] S. Eilenberg, Automata languages and machines, Pure and Applied Mathematics, Volume B (Academic Press, New York, 1976).
  * [18] S. Eilenberg, M.-P. Schützenberger, On pseudovarieties. Adv. Math. 19 (1976), 413–418.
  * [19] V.A. Gorbunov, Algebraic Theory of Quasivarieties, Consultants Bureau, New York, 1998.
  * [20] Y. Gurevich, Toward logic tailored for computational complexity, in Computation and Proof Theory, Lecture Notes in Mathematics 1104, 1984, pp. 175–216.
  * [21] L. Ham, Relativised Homomorphism Preservation at the Finite Level, Studia Logica 105 (2017), 761–786.
  * [22] P.M. Higgins and M. Jackson, Algebras defined by equations, J. Algebra 555 (2020), 131–151.
  * [23] D. Hobby and R. McKenzie, The Structure of Finite Algebras, Contemporary Mathematics 76, American Mathematical Society, Providence, RI, 1988.
  * [24] N. Immerman, Descriptive Complexity, Graduate Texts in Computer Science, Springer 1999.
  * [25] M. Jackson, Flat algebras and the translation of universal Horn logic to equational logic, J. Symbolic Logic, 73 (2008), 90–128.
  * [26] M. Jackson, Flexible constraint satisfaction and a problem in semigroup theory, arXiv:1512.03127v2
  * [27] M. Jackson, T. Kowalski and T. Niven, Complexity and polymorphisms for digraph constraint problems under some basic constructions, Internat. J. Algebra Comput. 26 (2016), 1395–1433.
  * [28] M. Jackson and R.N. McKenzie, Interpreting graph colorability in finite semigroups, Internat. J. Algebra Comput. 16 (2006), 119–140.
  * [29] M. Jackson and G.F. McNulty, The equational complexity of Lyndon’s algebra, Algebra Universalis 65 (2011), 243–262.
  * [30] M. Jackson, M. Ren and X. Zhao, Nonfinitely based ai-semirings with finitely based semigroup reducts, J. Algebra 611 (2022), 211–245.
  * [31] M. Jackson and B. Trotta, The division relation: congruence conditions and axiomatisability, Comm. Algebra 38 (2010), 534–566.
  * [32] M. Jackson and M.V. Volkov, The Algebra of Adjacency Patterns: Rees Matrix Semigroups with Reversion, in A. Blass, N. Dershowitz, and W. Reisig (Eds.): Gurevich Festschrift, LNCS 6300, pp. 414–443, 2010.
  * [33] H.J. Keisler, Reduced products and Horn classes, Trans. Am. Math. Soc. 117 (1965) 307–328.
  * [34] O.G. Kharlampovich and M.V. Sapir, Algorithmic problems in varieties, Internat. J. Algebra Comput. 5 (1995), 379–602.
  * [35] M. Kozik, Computationally and algebraically complex finite algebra membership problems, Internat. J. Algebra Comput. 17 (2007), 1635–1666.
  * [36] M. Kozik, A 2EXPTIME complete varietal membership problem, SIAM J. Comput. 38 (2009), 2443–2467.
  * [37] A. Korkhin and S. Žviný (eds), The Constraint Satisfaction Problem: Complexity and Approximability, Dagstuhl Follow Ups 7 (2017).
  * [38] E.W.H. Lee and W.T. Zhang, Finite basis problem for semigroups of order six, LMS J. Comput. Math. 18 (2015), 1–129.
  * [39] L. Libkin, Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer-Verlag, Berlin, 2004.
  * [40] R. McKenzie: The residual bounds of finite algebras. Internat. J. Alg. Comput. 6 (1996), 1–28.
  * [41] R. McKenzie: The residual bound of a finite algebra is not computable. Internat. J. Alg. Comput. 6 (1996), 29–48.
  * [42] R. McKenzie: Tarski’s finite basis problem is undecidable. Internat. J. Alg. Comput. 6 (1996), 49–104.
  * [43] R. Park, Equational classes of non-associative ordered systems, Ph.D. dissertation, UCLA, 1976.
  * [44] O. Reingold, Undirected st-connectivity in log-space. In Harold N. Gabow and Ronald Fagin, editors, STOC, pages 376–385. ACM, 2005.
  * [45] O. Reingold, Undirected connectivity in log-space, J. ACM, 55(4), 2008.
  * [46] B. Rossman, Homomorphism preservation theorems, J. ACM 55 (2008), no. 3, Art. 15, 53 pp.
  * [47] E. Rosen, Some aspects of finite model theory and finite structures, Bull. Symb. Logic 8 (2002), 380–403.
  * [48] Z. Szekely, Computational complexity of the finite algebra membership problem for varieties, Internat. J. Algebra Comput. 12 (2002), 811–823.
  * [49] W.W. Tait, A counterexample to a conjecture of Scott and Suppes, J. Symbolic Logic 24 (1959), 15–16.
  * [50] M.V. Volkov, S.V. Goldberg, and S.I. Kublanovsky, J. Math. Sci. 177 (2011), 847–859.
  * [51] R. Willard, On McKenzie’s method, Periodica Mathematica Hungarica 32 (1996), 149–165.
  * [52] R. Willard, Tarski’s finite basis problem via ${\bf A}(\mathcal{T})$, Trans. Amer. Math. Soc. 349 (1997), 2755–2774.
  * [53] R. Willard, A finite basis theorem for residually finite, congruence meet-semidistributive varieties. J. Symbolic Logic 65, 187–200. (1997), 2755–2774.
  * [54] R. Willard, The finite basis problem, Contributions to General Algebra, vol. 15, 199–206, Heyn, Klagenfurt, 2004.