# Decidability, Complexity, and Expressiveness of First-Order Logic Over the
Subword Ordering

Simon Halfon  Lab. Specification & Verification (LSV), ENS Paris-Saclay,
Cachan, France<EMAIL_ADDRESS>,  Philippe Schnoebelen  Lab. Specification &
Verification (LSV), ENS Paris-Saclay, Cachan, France<EMAIL_ADDRESS>and  Georg
Zetzsche  Lab. Specification & Verification (LSV), ENS Paris-Saclay, Cachan,
France<EMAIL_ADDRESS>
###### Abstract.

We consider first-order logic over the subword ordering on finite words, where
each word is available as a constant. Our first result is that the
$\Sigma_{1}$ theory is undecidable (already over two letters).

We investigate the decidability border by considering fragments where all but
a certain number of variables are alternation bounded, meaning that the
variable must always be quantified over languages with a bounded number of
letter alternations. We prove that when at most two variables are not
alternation bounded, the $\Sigma_{1}$ fragment is decidable, and that it
becomes undecidable when three variables are not alternation bounded.
Regarding higher quantifier alternation depths, we prove that the $\Sigma_{2}$
fragment is undecidable already for one variable without alternation bound and
that when all variables are alternation bounded, the entire first-order theory
is decidable.

The third author is supported by a fellowship within the Postdoc-Program of
the German Academic Exchange Service (DAAD) and by Labex Digicosme, ENS Paris-
Saclay, project VERICONISS

##  1\. Introduction

A subsequence of a (finite) sequence $u$ is a sequence obtained from $u$ by
removing any number of elements. For example, if $u=({a},{b},{a},{b},{a})$
then $u^{\prime}=({b},{b},{a})$ is a subsequence of $u$, a fact we denote with
$u^{\prime}\sqsubseteq u$. Other examples that work for any $u$ are
$u\sqsubseteq u$ (remove nothing) and $()\sqsubseteq u$. In the rest of this
paper, we shall use the terminology from formal methods and will speak of
_words_ and their _subwords_ rather than finite sequences.

Reasoning about subwords occurs prominently in many areas of computer science,
e.g., in pattern matching (of texts, of DNA strings, etc.), in coding theory,
in theorem proving, in algorithmics, etc. Closer to our own motivations, the
automatic verification of unreliable channel systems and related problems
involves the subword ordering or some of its variants [2, 5, 16, 23]. Our
experience is that reasoning about subwords and related concepts (e.g.,
shuffles of words) involves ad hoc techniques quite unlike the standard tools
that work well with prefixes and suffixes [21].

### The logic of subwords

In this paper we consider the first-order logic $\FO(A^{*},\sqsubseteq)$ of
words over some alphabet $A=\\{a,b,c,\ldots\\}$ equipped with the subword
relation only. Our main objective is to understand how and when one can decide
queries formulated in this logic, or decide whether a given formula is valid.

For example, we consider formulas like

$\displaystyle\varphi_{1}{:}$ $\displaystyle\forall u,v,w:$
$\displaystyle\>u\sqsubseteq v\land v\sqsubseteq w\implies u\sqsubseteq w$
$\displaystyle\varphi_{2}{:}$ $\displaystyle\exists u:$
$\displaystyle\>{a}{b}{c}{d}\sqsubseteq u\land{b}{c}{d}{e}\sqsubseteq
u\land{a}{b}{c}{d}{e}\not\sqsubseteq u$ $\displaystyle\varphi_{3}{:}$
$\displaystyle\forall u,v:\exists w:$
$\displaystyle\left(\\!\\!\\!\begin{array}[]{rl}&u\sqsubseteq w\land
v\sqsubseteq w\\\ \land\\!\\!&\forall t:u\sqsubseteq t\land v\sqsubseteq
t\implies w\sqsubseteq t\end{array}\\!\\!\\!\right)$

Here $\varphi_{1}$ states that the subword relation is transitive (which it
is).

More interesting is $\varphi_{2}$, stating that it is possible that a word
contains both ${a}{b}{c}{d}$ and ${b}{c}{d}{e}$ as subwords but not
${a}{b}{c}{d}{e}$. This formula is true and, beyond knowing its validity, one
is also interested in _solutions_ : can we design a constraint solver that
will produce a witness, e.g., $u={bcdeabcd}$, or more generally the set of
solutions?

Our third example, $\varphi_{3}$, states that words ordered by subwords are an
upper semilattice. This is a more complex formula with $\Pi_{3}$ quantifier
alternation. It is not valid in general (e.g., ${a}{b}$ and ${b}{a}$ have no
lub) but this depends on the alphabet $A$ at hand: $\varphi_{3}$ holds if $A$
is a singleton alphabet, i.e., $\\{{a}\\}^{*}\models\varphi_{3}$ but
$\\{{a},{b}\\}^{*}\not\models\varphi_{3}$.

We say that formulas like $\varphi_{1}$ or $\varphi_{3}$ where constants from
$A^{*}$ do not appear are in the _pure fragment_. Formally, there are two
logics at hand here. The _pure_ logic is the logic of the purely relational
structure $({A}^{*},\mathord{\sqsubseteq})$ while the _extended_ logic is over
the expansion $({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ where
there is a constant symbol $w_{i}$ for every word in $A^{*}$.

As we just illustrated with $\varphi_{3}$, the validity of a formula may
depend on the underlying alphabet even for the pure fragment. We note that
this phenomenon is not limited to the degenerate case of singleton alphabets.
Indeed, observe that it is possible to state that $x$ is a letter, i.e., is a
word of length 1, in the pure fragment:

$\exists z:\forall u:z\sqsubseteq u\land(u\sqsubseteq
x\implies\bigl{(}x\sqsubseteq u\lor u\sqsubseteq z\bigr{)})$

Thus, even in the pure fragment, one can state that $A$ contains $2$, $3$, …,
or exactly $n$ letters. Similarly one can state that $A$ is infinite by saying
that no word contains all letters.

### State of the art

Relatively little is known about deciding the validity of
$({A}^{*},\mathord{\sqsubseteq})$ formulas and about algorithms for computing
their solutions. By comparison, it is well known that the $\Sigma_{2}$-theory
of $\FO(A^{*},\cdot)$, the logic of strings with concatenation, is undecidable
[33, 11], and that its $\Sigma_{1}$ fragment (aka “word equations”) is
decidable in $\PSPACE$ [9, 32]. Moreover, introducing counting predicates
leads to an undecidable $\Sigma_{1}$ fragment [6].

Regarding the logic of subwords, Comon and Treinen showed undecidability for
an extended logic $\FO(A^{*},\sqsubseteq,p_{\\#})$ where $A=\\{a,b,{\\#}\\}$
has three letters and $p_{\\#}$ is a unary function that prepends ${\\#}$ in
front of a word, hence is a restricted form of concatenation [8, Prop. 9].
Kuske showed that, when only the subword predicate is allowed, the logic
$({A}^{*},\mathord{\sqsubseteq})$ is undecidable and already its $\Sigma_{3}$
fragment is undecidable when $|A|=2$. Kudinov et al. considered definability
in $({A}^{*},\mathord{\sqsubseteq})$ and showed that the predicates definable
in $({A}^{*},\mathord{\sqsubseteq})$ are exactly the arithmetical
predicates111Those that are invariant under the automorphisms of the structure
[28].

Kuske’s result on the $\Sigma_{3}$ theory leaves open the question whether
smaller fragments are decidable. Karandikar and Schnoebelen showed that the
$\Sigma_{2}$ theory is undecidable [22] and this is tight since the
$\Sigma_{1}$ fragment is decidable, in fact $\NP$-complete [29, 22].
Karandikar and Schnoebelen also showed that the two-variable fragment
$\FO^{2}(A^{*},\sqsubseteq)$ is decidable[22] and that it has an elementary
complexity upper bound [24]. Decidability extends to
$\FO^{2}(A^{*},\sqsubseteq,R_{1},R_{2},\ldots)$ where arbitrary regular
languages (monadic predicates) are allowed.

### Objectives of this paper

We are interested in solving constraints built with the subword ordering. This
corresponds to the $\Sigma_{1}$ fragment but beyond deciding validity, we are
interested in computing sets of solutions: a formula like $\varphi_{2}$ can be
seen as a conjunctive set of constraints, “${a}{b}{c}{d}\sqsubseteq
x\land{b}{c}{d}{e}\sqsubseteq x\land{a}{b}{c}{d}{e}\not\sqsubseteq x$” that
define a set of words (a set of tuples when there are several free variables).

A first difficulty is that Kuske’s decidability result for the $\Sigma_{1}$
fragment only applies to the pure fragment, where constants are not allowed.
That is, we know how to decide the validity of formulas like $\varphi_{1}$ but
not like $\varphi_{2}$. However, using constants inside constraints is natural
and convenient. In particular, it makes it easy to express piecewise-testable
constraints (see below), and we would like to generalise Kuske’s result to the
extended logic.

We note that, in principle, the difference between the pure and the extended
logic is only superficial since, up to automorphisms, arbitrary words can be
defined in the logic,222This is a common situation, shared with, e.g.,
$\FO(A^{*},\cdot)$ and $\FO(\mathbb{N},<)$. see [22, 28]. However _this
involves $\Sigma_{2}$ definitions_ that are not allowed when restricting to
the $\Sigma_{1}$ fragment. So this avenue is closed.

### Summary of results

Our first result is that, _when constants are allowed_ , the $\Sigma_{1}$
fragment of $\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ is
actually undecidable! This holds as soon as $A$ contains two distinct letters
and exhibits a sharp contrast between the pure and the extended logic. We
found this very surprising because, before hitting on undecidability, we had
already developed algorithms that solve large classes of $\Sigma_{1}$
constraints.

Our second result identifies a key factor influencing decidability: it turns
out that free variables ranging over a “thin” language like
$L={a}^{+}{b}{c}^{*}$, are easier to handle than variables ranging over a
“wide” language like $L^{\prime}=({a}+{b})^{*}$. The key difference is that a
thin language only allows a bounded number of letter changes (in $L$ we have
${a}$’s, then ${b}$’s, then ${c}$’s) while a wide language contains words with
arbitrarily many alternations between distinct letters.

These observations lead to a new descriptive complexity measure for formulas
in $\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$. The associated
fragments, denoted $\Sigma_{i,j}$ for $i,j\in\mathbb{N}$, consist of all
$\Sigma_{i}$ formulas where $j$ variables, say $x_{1},x_{2},\ldots,x_{j}$ can
be used without any restrictions, while all the other variables must be
restricted with respect to letter alternations, say using
$x\in(a^{*}_{1}a^{*}_{2}\ldots a^{*}_{n})^{\ell}$ for some $\ell\in\mathbb{N}$
and assuming that $a_{1},\ldots,a_{n}$ is a fixed enumeration of $A$. In
computer-aided verification, such bounded quantifications occur in the
analysis of bounded context-switching protocols.

Within this classification framework, we can delineate a precise
undecidability landscape. The $\Sigma_{1,2}$ fragment is decidable while
$\Sigma_{1,3}$ is undecidable even for $|A|=2$. The $\Sigma_{2,0}$ fragment is
decidable while $\Sigma_{2,1}$ is not. In fact, when all variables are
alternation bounded, the entire first-order theory is decidable.

$\Sigma_{i,j}$ | 0 | 1 | 2 | 3
---|---|---|---|---
1 | $\NP$ | $\NP$ | in $\NEXP$ | U
$i\geq 2$ | ${\ComplexityFont{\Sigma}}_{i-1}^{\ComplexityFont{EXP}}$ | U | U | U
Table 1. The cell in row $i$ and column $j$ shows the decidability/complexity
of the fragment $\Sigma_{i,j}$.

The computational complexity of all mentioned fragments is summarised in Table
1. Note that, in this table,
${\ComplexityFont{\Sigma}}_{n}^{\ComplexityFont{EXP}}$ denotes the $n$-th
level of the weak $\EXP$ hierarchy, which lies between $\NEXP$ and $\EXPSPACE$
[18, 15].

Finally, we offer a series of expressiveness results showing how various
predicates like concatenation or length function can, or cannot, be defined in
the $\Sigma_{i,j}$ fragments. Beyond their theoretical interest, and since
pinning down precise properties of words is not easy when only the subword
ordering is available, these results provide a welcome intermediate language
for defining more complex formulas.

### Related work

We already mentioned works on the logic of concatenation, or the two-variable
fragment $\FO^{2}(A^{*},\sqsubseteq)$. Because undecidability appears so
easily when reasoning about words, the focus is often on restricted fragments,
typically $\Sigma_{1}$, aka “constraint solving”. Decision methods for
constraints over words have been considered in several contexts but this
usually does not include the subsequence predicate: these works rather
consider the prefix ordering, and/or membership in a regular language, and/or
functions for taking contiguous subsequences or computing the length of
sequences, see, e.g., [19, 13, 1].

### Outline of the paper

We provide in Section 2 the basic definitions and results necessary for our
later developments. Then we show the undecidability of the $\Sigma_{1}$
fragment and prove several expressiveness results (Section 3) before focusing
on the decidable fragments (Section 4). Finally Section 5 provides a
characterisation of properties expressible in the $\Sigma_{1,0}$ fragment and
applies this to expressiveness questions. For completeness, a technical
appendix contains proofs omitted from the main text.

##  2\. Subwords and their logics

We consider finite words $u,v,...$ over a given finite alphabet $A$ of letters
like $a,b,\ldots$. Concatenation of words is written multiplicatively, with
the empty word $\varepsilon$ as unit. We freely use regular expressions like
$(ab)^{*}+(ba)^{*}$ to denote regular languages.

The length of a word $u$ is written $|u|$ while, for a letter $a\in A$,
$|u|_{a}$ denotes the number of occurrences of $a$ in $u$. The set of all
words over $A$ is written $A^{*}$.

A word $v$ is a _factor_ of $u$ if there exist words $u_{1}$ and $u_{2}$ such
that $u=u_{1}vu_{2}$. If furthermore $u_{1}=\varepsilon$ then $v$ is a
_prefix_ of $u$, while if $u_{2}=\varepsilon$ then $v$ is a _suffix_.

### Subwords.

We say that a word $u$ is a _subword_ (i.e., a subsequence) of $v$, written
$u\sqsubseteq v$, when $u$ is some $a_{1}\cdots a_{n}$ and $v$ can be written
as $v_{0}a_{1}v_{1}\cdots a_{n}v_{n}$ for some $v_{0},v_{1},\ldots,v_{n}\in
A^{*}$, e.g., $\varepsilon\sqsubseteq bba\sqsubseteq ababa$. We write
$u\sqsubset v$ for the associated strict ordering, where $u\neq v$. Two words
$u$ and $v$ are _incomparable_ (with respect to the subword relation), denoted
$u\perp v$, if $u\not\sqsubseteq v$ and $v\not\sqsubseteq u$. Factors are a
special case of subwords.

With any $u\in A^{*}$ we associate its _upward closure_
${\uparrow}{u}\stackrel{{\scriptstyle\mbox{\scriptsize def}}}{{=}}\\{v\in
A^{*}~{}|~{}u\sqsubseteq v\\}$. For example,
${\uparrow}{ab}=A^{*}aA^{*}bA^{*}$. The definition of ${\uparrow}{u}$ involves
an implicit alphabet $A$ that will always be clear from the context.

#### Piecewise testable languages

Piecewise testable languages (abbreviated PT) constitute a subvariety of the
languages of dot-depth one, themselves a subvariety of the star-free
languages, which are a subvariety of the regular languages [10]. Among the
several characterisations of PT languages, the most convenient for our
purposes is the following one: $L\subseteq A^{*}$ is PT if, and only if, it is
a boolean combination of languages of the form ${\uparrow}u$ for some $u\in
A^{*}$. Thus the PT languages are exactly the monadic predicates that can be
defined by a boolean combination of constraints of the form $u_{i}\sqsubseteq
x$ and/or $u_{j}\not\sqsubseteq x$, or equivalently by a quantifier-free
$\varphi_{L}(x)$ formula in the
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ logic. In the
following, we often write $x\in L$, where $L$ is a given PT language, as an
abbreviation for that $\Sigma_{0}$ formula.

### Logic of subwords

Let $V$ be the set of variables with typical elements $x,y,\ldots,u,v,\ldots\
$

For any first-order formula, $\mathsf{fv}(\varphi)$ denotes the set of free
variables. Moreover, for a first-order logic formula $\varphi$ over a
structure with domain $D$, we denote by $\llbracket\varphi\rrbracket\subseteq
D^{V}$ the set of satisfying assignments. If $\varphi$ has only one free
variable, say $x$, and there is no danger of confusion, we sometimes write
$\llbracket\varphi\rrbracket$ to mean
$\\{\alpha(x)\mid\alpha\in\llbracket\varphi\rrbracket\\}$.

By $\FO({A}^{*},\mathord{\sqsubseteq})$, we denote the first-order logic over
the structure $({A}^{*},\mathord{\sqsubseteq})$, whereas
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ is the first-order
logic over the structure
$({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$, where for each word
$w\in A^{*}$, the signature provides a constant symbol. In the case of
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ and
$\FO({A}^{*},\mathord{\sqsubseteq})$, assignments are members of
$(A^{*})^{V}$. Here, we will sometimes write $\varepsilon$ to denote the
assignment that maps every variable to the empty word $\varepsilon$.

### Bounding alternations

We define a fragment of first-order logic over the structure
$({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$. Let
$A=\\{a_{1},\ldots,a_{n}\\}$. The starting point for introducing the fragments
$\Sigma_{i,j}$ is the observation that if every variable in a sentence
$\varphi$ is introduced by a restricted quantifier of the form $\exists
x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$ or $\forall x\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell}$ for some $\ell\in\mathbb{N}$, then one can reduce the truth
of $\varphi$ to Presburger arithmetic. Note that the language
$(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$ is PT, implying that such restrictions,
which we call _alternation bounds_ , can be imposed within
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ and without any
additional quantifiers. This raises the question of how many variables without
alternation bound one can allow without losing decidability.

Intuitively, $\Sigma_{i,j}$ allows formulas in the $\Sigma_{i}$ fragment with
$j$ variables without alternation bound. A formalisation of this _for
sentences_ could just be a syntactic restriction: Every quantifier for all but
at most $j$ variables must be relative to some $(a_{1}^{*}\cdots
a_{n}^{*})^{\ell}$. However, this would not restrict free variables, which we
need in order to build complex $\Sigma_{i,j}$ formulas from predicates defined
in $\Sigma_{i,j}$.

Let $V$ be the set of variables. Formally, a _formula with alternation bounds_
consists of a formula $\varphi$ of
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ and a function
$\ell\colon V\to\mathbb{N}\cup\\{\infty\\}$, which specifies the alternation
bounds. This means, the semantics $\llbracket(\varphi,\ell)\rrbracket$ of
$(\varphi,\ell)$ is defined as $\llbracket\tilde{\varphi}\rrbracket$, where
$\tilde{\varphi}$ is defined as follows. First, we replace every quantifier
$\mathcal{Q}x$ ($\mathcal{Q}\in\\{\exists,\forall\\}$) by the relativised
$\mathcal{Q}x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell(x)}$. In the second step, we
build the conjunction with
$\bigwedge_{x\in\mathsf{fv}(\varphi),\ell(x)<\infty}x\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell(x)}$.

The fragment $\Sigma_{i,j}$ consists of those formulas with alternation bounds
$(\varphi,\ell)$ where $\varphi$ belongs to the $\Sigma_{i}$ fragment of
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ and has at most
$j$ variables $x\in V$ with $\ell(x)=\infty$. We will always represent a
formula in $\Sigma_{i,j}$ by its $\Sigma_{i}$ formula and the function $\ell$
will be clear from the context. Variables $x\in V$ with $\ell(x)<\infty$ will
be called _alternation bounded_ , the others _alternation unbounded_. In order
to permit a polynomial translation into an equivalent formula in ordinary
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$, the alternation
bounds are always encoded in unary. The fragment $\Pi_{i,j}$ is defined with
$\Pi_{i}$ instead of $\Sigma_{i}$.

Sometimes we define predicates that are satisfied for words with unbounded
alternations (such as “$u\in\\{a,b\\}^{*}$” when $A=\\{a,b,c\\}$), but want to
use the corresponding formula in a context where the variables are alternation
bounded (“$u\in\\{a,b\\}^{*}\wedge ab\not\sqsubseteq u$”). In that situation,
we want to record the number of alternation unbounded variables we need for
the definition, _disregarding the free variables_. Hence,
$\Sigma^{\prime}_{i,j}$ denotes those formulas with alternation bound in
$\Sigma_{i}$, where there are at most $j$ _quantified variables_ without
alternation bound. The semantics is defined as for $\Sigma_{i,j}$. The
fragment $\Pi^{\prime}_{i,j}$ is defined with $\Pi_{i}$ instead of
$\Sigma_{i}$.

##  3\. Undecidability

###  3.1. The $\Sigma_{1,3}$ fragment

We begin with our main result, the undecidability of the $\Sigma_{1}$ theory
of $\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ for $|A|\geq
2$. In fact, we will even prove undecidability for the $\Sigma_{1,3}$
fragment. We need a few ingredients. A word $u\in A^{+}$ is called _primitive_
if there is no $v\in A^{+}$, $|v|<|u|$, with $u\in v^{*}$. The following is a
well-known basic fact from word combinatorics (see e.g. [4, Exercise 2.5])

######  Fact 3.1.

If $p\in A^{+}$ is primitive, then $pu=up$ is equivalent to $u\in p^{*}$.

We also use the following version of the fact that Diophantine sets are
precisely the recursively enumerable sets [30].

######  Theorem 3.2.

Let $S\subseteq\mathbb{N}$ be a recursively enumerable set. Then there is a
finite set of variables $\\{x_{0},\ldots,x_{m}\\}$ and a finite set $E$ of
equations, each of the form

$\displaystyle x_{i}=x_{j}+x_{k}$ $\displaystyle x_{i}=x_{j}\cdot x_{k}$
$\displaystyle x_{i}=1$

with $i,j,k\in[0,m]$, such that

$S=\\{y_{0}\in\mathbb{N}\mid\exists
y_{1},\ldots,y_{m}\in\mathbb{N}\colon\text{$(y_{0},\ldots,y_{m})$ satisfies
$E$}\\}.$

We are now ready to prove our main result.

######  Theorem 3.3.

Let $|A|\geq 2$ and $a\in A$. For each recursively enumerable set
$S\subseteq\mathbb{N}$, there is a $\Sigma_{1,3}$ formula $\varphi$ over the
structure $\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ with one
free variable such that $\llbracket\varphi\rrbracket=\\{a^{k}\mid k\in S\\}$.
In particular, the truth problem for $\Sigma_{1,3}$ is undecidable.

###### Proof.

We show how to express some basic properties of words and combine these to
build more complex predicates, all the time keeping track of what fragments
are involved. Recall that for every PT language $L\subseteq A^{*}$, we can
express “$x\in L$” in $\Sigma^{\prime}_{0,0}$: we will use this silently,
mainly for languages of the form $ua^{*}v$ where $a$ is a letter and $u,v$ are
two words.333That any language of the form $ua^{*}v$ is PT is easy to prove,
e.g., using the characterisation of [26]. Note also that, since
“$u\in(a+b)^{*}\,$” can be expressed in $\Sigma^{\prime}_{0,0}$ for $a,b\in
A$, it suffices to prove the theorem in the case $|A|=2$.

  1. (1)

We can express “$|u|_{a}<|v|_{a}$” in $\Sigma^{\prime}_{1,0}$:

$\exists x\in a^{*}\colon x\sqsubseteq v\wedge x\not\sqsubseteq u.$

  2. (2)

We can express “$\exists n\colon u=a^{n}\wedge v=a^{n-1}b$” in $\Sigma_{1,0}$.
Clearly, it suffices to show that we can express “$\exists n\geq 2\colon
u=a^{n}\wedge v=a^{n-1}b$”. Consider the formula:

$\displaystyle u\in aaa^{*}\wedge v\in a^{*}b\wedge\exists x\in
a^{*}baa\colon|v|_{a}<|u|_{a}\wedge v\not\sqsubseteq x\wedge u\sqsubseteq x.$

Suppose the formula is satisfied with $u=a^{n}$, $x=a^{\ell}baa$ and
$v=a^{m}b$. Then $|v|_{a}<|u|_{a}$ implies $m<n$. By $v\not\sqsubseteq x$, we
have $\ell<m$ and thus $\ell<m<n$, hence $\ell+2\leq n$. On the other hand,
$u\sqsubseteq x$ implies $n\leq\ell+2$ and thus $n=\ell+2$ and $m=n-1$.

Conversely, if $u=a^{n}$ and $v=a^{n-1}b$ for some $n\geq 2$, then the formula
is satisfied with $x=a^{n-2}baa$.

  3. (3)

We can express “$u,v\in(a+b)^{*}b\wedge|u|_{a}=|v|_{a}$” in
$\Sigma^{\prime}_{1,0}$:

$\displaystyle u,v\in(a+b)^{*}$ $\displaystyle~{}\wedge~{}\exists x\in
a^{*}\colon\exists y\in a^{*}b\colon\left[\exists n\colon x=a^{n}\wedge
y=a^{n-1}b\right]$ $\displaystyle~{}\wedge~{}y\sqsubseteq
u~{}\wedge~{}y\sqsubseteq v~{}\wedge~{}x\not\sqsubseteq
u~{}\wedge~{}x\not\sqsubseteq v.$

Suppose the formula is satisfied. Then $a^{n-1}b\sqsubseteq u$ and
$a^{n}\not\sqsubseteq u$ imply $|u|_{a}=n-1$. Moreover, if $u$ ended in $a$,
then $a^{n-1}b\sqsubseteq u$ would entail $a^{n}\sqsubseteq u$, which is not
the case. Since $|u|\geq 1$, we therefore have $u\in\\{a,b\\}^{*}b$. By
symmetry, we have $|v|_{a}=n-1$ and $v\in\\{a,b\\}^{*}b$. Hence,
$|u|_{a}=n-1=|v|_{a}$.

If $u,v\in\\{a,b\\}^{*}b$ with $|u|_{a}=|v|_{a}$, then the formula is
satisfied with $n=|u|_{a}+1$.

  4. (4)

We can express “$\exists n\colon u=aaba^{n}b\wedge v=aba^{n+1}b\wedge
w=ba^{n+2}b$” in $\Sigma_{1,0}$:

$\displaystyle u\in aaba^{*}b\wedge v\in aba^{*}b\wedge w\in ba^{*}b$
$\displaystyle~{}\wedge~{}\left[u,v,w\in\\{a,b\\}^{*}b\wedge|u|_{a}=|v|_{a}=|w|_{a}\right].$

  5. (5)

We can express “$\exists n\colon u=ba^{n}b\wedge v=ba^{n+1}b$” in
$\Sigma_{1,0}$. It suffices to show that we can express “$\exists n\geq
1\colon u=ba^{n}b\wedge v=ba^{n+1}b$”. Consider the formula:

$\displaystyle\exists x\in aaba^{*}b,y\in aba^{*}b,z\in ba^{*}b\colon$
$\displaystyle\left[\exists m\colon x=aaba^{m}b\wedge y=aba^{m+1}b\wedge
z=ba^{m+2}b\right]$ $\displaystyle~{}\wedge~{}u,v\in
ba^{*}b~{}\wedge~{}u\sqsubseteq y~{}\wedge~{}u\not\sqsubseteq
x~{}\wedge~{}v\sqsubseteq z~{}\wedge~{}v\not\sqsubseteq y.$

Suppose the formula is satisfied for $u=ba^{k}b$ and $v=ba^{\ell}b$. Then
$u\sqsubseteq y$ and $u\not\sqsubseteq x$ imply $k\leq m+1$ and $k>m$, hence
$k=m+1$. Moreover, $v\sqsubseteq z$ and $v\not\sqsubseteq y$ imply $\ell\leq
m+2$ and $\ell>m+1$, hence $\ell=m+2$. Hence, with $n=m+1$ we have $u=ba^{n}b$
and $v=ba^{n+1}b$ and $n\geq 1$.

Conversely, if $u=ba^{n}b$ and $v=ba^{n+1}b$ for some $n\geq 1$, then the
formula is satisfied with $m=n-1$.

  6. (6)

We can express “$\exists n\colon u=a^{n}\wedge v=a^{n+1}$” in $\Sigma_{1,0}$.
For this, it suffices to express “$\exists n\geq 1\colon u=a^{n}\wedge
v=a^{n+1}$”. As in 5, one verifies correctness of the following:

$\displaystyle\exists x,y,z\colon\left[\exists m\colon x=ba^{m}b\wedge
y=ba^{m+1}b\wedge z=ba^{m+2}b\right]$ $\displaystyle\wedge~{}u,v\in
a^{*}~{}\wedge~{}u\sqsubseteq y~{}\wedge~{}u\not\sqsubseteq
x~{}\wedge~{}v\sqsubseteq z~{}\wedge~{}v\not\sqsubseteq y.$

  7. (7)

We can express “$v=a^{|u|_{a}}$” in $\Sigma^{\prime}_{1,0}$:

$\exists x\in a^{*}\colon\left[\exists n\colon v=a^{n}\wedge
x=a^{n+1}\right]\wedge v\sqsubseteq u\wedge x\not\sqsubseteq u.$

  8. (8)

We can express “$|u|_{a}=|v|_{a}$” in $\Sigma^{\prime}_{1,0}$:

$\exists x\colon x=a^{|u|_{a}}\wedge x=a^{|v|_{a}}.$

  9. (9)

For $a\neq b$, we can express “$u\in a^{*}\wedge v=bu$” in $\Sigma_{1,0}$:

$u\in a^{*}\wedge v\in ba^{*}\wedge|v|_{a}=|u|_{a}.$

  10. (10)

For $a\neq b$, we can express “$u\in a^{*}\wedge v=ub$” in $\Sigma_{1,0}$:

$u\in a^{*}\wedge v\in a^{*}b\wedge|v|_{a}=|u|_{a}.$

  11. (11)

We can express “$|w|_{a}=|u|_{a}+|v|_{a}$” for any $a\in A$ in
$\Sigma^{\prime}_{1,0}$. Let $b\in A\smallsetminus\\{a\\}$:

$\displaystyle\exists x,y\in a^{*}\colon\exists z\in a^{*}ba^{*}\colon
x=a^{|u|_{a}}\wedge y=a^{|v|_{a}}$ $\displaystyle\wedge\ xb\sqsubseteq z\wedge
xab\not\sqsubseteq z\wedge by\sqsubseteq z\wedge bya\not\sqsubseteq z$ (1)
$\displaystyle\wedge\ |w|_{a}=|z|_{a}$ (2)

Note that we can define $xb$, $(xa)b$ and $b(ya)$ thanks to Items 9, 10 and 6
The constraints in Eq. 1 enforce that $z=xby$ and hence
$|z|_{a}=|x|_{a}+|y|_{a}=|u|_{a}+|v|_{a}$.

  12. (12)

For $k,n_{0},\ldots,n_{k}\in\mathbb{N}$, $a\neq b$, let
$r_{a}(a^{n_{0}}ba^{n_{1}}\cdots ba^{n_{k}})=n_{k}$, which defines a function
$r_{a}\colon\\{a,b\\}^{*}\to\mathbb{N}$. We can express “$v=a^{r_{a}(u)}$” in
$\Sigma^{\prime}_{1,0}$:

$\displaystyle v\in a^{*}\wedge~{}\exists x\in b^{*}a^{*}\colon\exists y\in
b^{*}a^{*}\colon$
$\displaystyle|x|_{b}=|y|_{b}=|u|_{b}~{}\wedge~{}|y|_{a}=|x|_{a}+1$
$\displaystyle\wedge~{}x\sqsubseteq u~{}\wedge~{}y\not\sqsubseteq
u~{}\wedge~{}|v|_{a}=|x|_{a}.$

Note that $|x|_{b}=|y|_{b}=|u|_{b}$ can be expressed according to Item 8 and
$|y|_{a}=|x|_{a}+1$ can be expressed thanks to Item 11. Write
$u=a^{n_{0}}ba^{n_{1}}\cdots ba^{n_{k}}$.

Suppose the formula is satisfied. Then $|x|_{b}=|y|_{b}=|u|_{b}$ and
$|y|_{a}=|x|_{a}+1$ imply that $x=b^{k}a^{m}$ and $y=b^{k}a^{m+1}$ for some
$m\in\mathbb{N}$. Moreover, $x\sqsubseteq u$ implies $m\leq n_{k}$ and
$y\not\sqsubseteq u$ implies $m+1>n_{k}$, thus $m=n_{k}$. Thus,
$|v|_{a}=|x|_{a}$ entails $|v|_{a}=n_{k}$.

Conversely, if $v=a^{n_{k}}$, then the formula is satisfied with
$x=b^{k}a^{n_{k}}$ and $y=b^{k}a^{n_{k}+1}$.

  13. (13)

For $a\in A$, we can express “$v\in a^{*}\wedge w=uv$” in
$\Sigma^{\prime}_{1,0}$. Let $b\neq a$ and consider the formula

$\displaystyle v\in a^{*}~{}\wedge$ $\displaystyle\wedge~{}~{}$
$\displaystyle\exists x\in a^{*}~{}\colon\exists y\in a^{*}~{}\colon
x=r_{a}(u)~{}\wedge~{}y=r_{a}(w)$ $\displaystyle\wedge~{}~{}$
$\displaystyle|w|_{b}=|u|_{b}~{}\wedge~{}u\sqsubseteq w$ (3)
$\displaystyle\wedge~{}~{}$
$\displaystyle|y|_{a}=|x|_{a}+|v|_{a}~{}\wedge~{}|w|_{a}=|u|_{a}+|v|_{a}$ (4)

To show correctness, suppose the formula is satisfied with
$u=a^{n_{0}}ba^{n_{1}}\cdots ba^{n_{k}}$ and $w=a^{m_{0}}ba^{m_{1}}\cdots
ba^{m_{\ell}}$. The conditions in Eq. 3 imply that $k=\ell$ and
$w=a^{m_{0}}ba^{m_{1}}\cdots ba^{m_{k}}$ and $n_{i}\leq m_{i}$ for
$i\in[0,k]$. The conditions in Eq. 4 then entail $m_{k}=n_{k}+|v|_{a}$ and
$\sum_{i=0}^{k}m_{i}=\sum_{i=0}^{k}n_{i}+|v|_{a}$, which together is only
possible if $m_{i}=n_{i}$ for $i\in[0,k-1]$. This means we have $w=uv$. The
converse is clear.

  14. (14)

We can express “$u$ is prefix of $v$” in $\Sigma_{1,3}$:

$\bigwedge_{a\in A}\exists x\colon\exists y\in a^{*}\colon
x=uy~{}\wedge~{}x\sqsubseteq v~{}\wedge~{}|x|_{a}=|v|_{a}.$

Suppose the formula is satisfied. Then $uy\sqsubseteq v$ for some $y\in
A^{*}$, which implies $u\sqsubseteq v$. Let $p$ be the shortest prefix of $v$
with $u\sqsubseteq p$. Observe that whenever $uw\sqsubseteq v$, we also have
$pw\sqsubseteq v$, because the leftmost embedding of $uw$ in $v$ has to match
up $u$ with $p$. Now towards a contradiction, assume $|p|>|u|$. Then there is
some $a\in A$ with $|p|_{a}>|u|_{a}$. The formula tells us that for some
$m\in\mathbb{N}$, we have $ua^{m}\sqsubseteq v$ and $|u|_{a}+m=|v|_{a}$. Our
observation yields $pa^{m}\sqsubseteq v$, and hence
$|v|_{a}\geq|p|_{a}+m>|u|_{a}+m=|v|_{a}$, a contradiction. The converse is
clear.

  15. (15)

We can express “$w=uv$” in $\Sigma_{1,3}$: Since expressibility is preserved
by mirroring, we can express prefix and suffix by Item 14. Let
$\sqsubseteq_{\mathsf{p}}$ and $\sqsubseteq_{\mathsf{s}}$ denote the prefix
and suffix relation, respectively. We can use the formula

$u\sqsubseteq_{\mathsf{p}}w~{}\wedge~{}v\sqsubseteq_{\mathsf{s}}w~{}\wedge~{}\bigwedge_{a\in
A}|w|_{a}=|u|_{a}+|v|_{a}.$

  16. (16)

For $a,b\in A$, $a\neq b$, we can express “$u\in(ab)^{*}$” in $\Sigma_{1,3}$:
By Item 15, we can use the formula $\exists v\colon v=uab\wedge v=abu,$ which,
according to 3.1, is equivalent to $u\in(ab)^{*}$.

  17. (17)

For $a,b\in A$, $a\neq b$, we can express “$|u|_{a}=|v|_{b}$” in
$\Sigma_{1,3}$ by using

$\exists x\in(ab)^{*}\colon|u|_{a}=|x|_{a}\wedge|v|_{b}=|x|_{b}.$

  18. (18)

We can express “$\exists m,n\colon u=a^{n}\wedge v=a^{m}\wedge w=a^{m\cdot
n}$” in $\Sigma_{1,3}$:

$\displaystyle u,v,w\in a^{*}$ $\displaystyle~{}\wedge~{}\exists
x\colon[\exists y,z\colon~{}y=bu~{}\wedge~{}z=yx~{}\wedge~{}z=xy]$
$\displaystyle~{}\wedge~{}|x|_{b}=|v|_{a}~{}\wedge~{}|w|_{a}=|x|_{a}.$

The conditions in brackets require $(bu)x=x(bu)$. Since $bu\in ba^{*}$ is
primitive, this is equivalent to $x\in(bu)^{*}$ (_cf_ 3.1).

  19. (19)

We use the fact that every recursively enumerable set of natural numbers is
Diophantine. Applying Theorem 3.2 to $S$ yields a finite set $E$ of equations
over the variables $\\{x_{0},\ldots,x_{m}\\}$. The formula $\varphi$ is of the
form

$\varphi\equiv\exists x_{1},x_{2},\dots,x_{m}\in a^{*}\colon\psi,$

where $\psi$ is a conjunction of the following $\Sigma_{1,3}$ formulas. For
each equation $x_{i}=1$, we add $x_{i}=a$. For each equation
$x_{i}=x_{j}+x_{k}$, we add a formula expressing
$|x_{i}|_{a}=|x_{j}|_{a}+|x_{k}|_{a}$. For each equation $x_{i}=x_{j}\cdot
x_{k}$, we add a formula expressing $x_{i}=a^{|x_{j}|\cdot|x_{k}|}$. Then we
clearly have $\llbracket\varphi\rrbracket=\\{a^{k}\mid k\in S\\}$.∎

∎

######  Remark 3.4.

Our result also shows that there is a fixed finite set of constants that is
sufficient for undecidability of $\Sigma_{1,3}$. Indeed, let
$S\subseteq\mathbb{N}$ be undecidable and let $\varphi$ be the formula
provided by Theorem 3.3. Let $x$ be a variable. We define the formulas
$\varphi_{0}\equiv\varphi$ and $\varphi_{i+1}\equiv\exists y\colon
y=xa\wedge\varphi_{i}(y)$. Then, all formulas $\varphi_{1},\varphi_{2},\ldots$
use the same finite set of constants. Moreover, given a number
$i\in\mathbb{N}$, it is undecidable whether the sentence $\exists
x:x=\varepsilon\wedge\varphi_{i}(x)$ is satisfied.

###  3.2. The $\Sigma_{2,1}$ fragment

Our next result is that if we allow one more quantifier alternation, then
already one variable without alternation bound is sufficient to prove
undecidability.

######  Theorem 3.5.

Let $|A|\geq 2$ and $a\in A$. For each recursively enumerable set
$S\subseteq\mathbb{N}$, there is a $\Sigma_{2,1}$ formula $\varphi$ over the
structure $\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ with one
free variable such that $\llbracket\varphi\rrbracket=\\{a^{k}\mid k\in S\\}$.
In particular, the truth problem for $\Sigma_{2,1}$ is undecidable.

###### Proof.

  1. (1)

We can express “$|u|_{a}\leq|v|_{a}$” in $\Pi^{\prime}_{1,0}$:

$\forall x\in a^{*}\colon x\not\sqsubseteq u\vee x\sqsubseteq v$

Hence, we can express “$|u|_{a}=|v|_{a}$” in $\Pi^{\prime}_{1,0}$.

  2. (2)

We can express “$|u|_{a}>|v|_{a}$” in $\Pi^{\prime}_{1,0}$: This follows from
the fact that $|u|_{a}\leq|v|_{a}$ is expressible in $\Sigma^{\prime}_{1,0}$.

  3. (3)

We can express “$|u|_{a}\neq|v|_{a}$” in $\Pi^{\prime}_{1,0}$ according to the
previous point.

  4. (4)

We can express “$u\in a^{*}\wedge v\in(bu)^{*}$” in $\Pi_{1,1}$:

$\displaystyle v\in b\\{a,b\\}^{*}~{}\wedge~{}\forall x\in
b^{+}a^{*}b^{*}\colon[|x|_{b}\neq|v|_{b}$
$\displaystyle~{}\vee~{}(|x|_{a}>|u|_{a}\wedge x\not\sqsubseteq
v)~{}\vee~{}(|x|_{a}\leq|u|_{a}\wedge x\sqsubseteq v)]$

Note that “$v\in b\\{a,b\\}^{*}$” is expressible in $\Pi^{\prime}_{1,0}$
because $v\in a\\{a,b\\}^{*}$ is expressible in $\Sigma^{\prime}_{1,0}$ (see
Item 3 in the proof of Theorem 3.3).

Moreover, notice that since
$b^{*}a^{*}b^{*}=\\{a,b\\}^{*}\smallsetminus{\uparrow}{aba}$, the language
$b^{+}a^{*}b^{*}=(b^{*}a^{*}b^{*})\cap({\uparrow}{ba}\cup({\uparrow}{b}\smallsetminus{\uparrow}{a}))$
is piecewise testable and thus definable in $\Sigma^{\prime}_{0,0}$.

  5. (5)

We can express “$|u|_{a}=|v|_{b}$” in $\Sigma_{2,1}$:

$\exists x\in(ab)^{*}\colon|u|_{a}=|x|_{a}\wedge|v|_{b}=|x|_{b}.$

  6. (6)

We can express “$\exists m,n\colon u=a^{m}\wedge v=a^{n}\wedge w=a^{m\cdot
n}$” in $\Sigma_{2,1}$:

$\displaystyle u\in a^{*}\wedge v\in a^{*}\wedge w\in a^{*}\wedge\exists y\in
b^{*}\colon\exists x\in(bu)^{*}\colon$
$\displaystyle|x|_{b}=|y|_{b}\wedge|y|_{b}=|v|_{a}\wedge|x|_{a}=|w|_{a}.$

  7. (7)

Recall that “$|w|_{a}=|u|_{a}+|v|_{a}$” is expressible in
$\Sigma^{\prime}_{1,0}$ (see Item 11 of Theorem 3.3) and hence “$\exists
m,n\colon u=a^{m}\wedge v=a^{n}\wedge w=a^{m+n}$” in $\Sigma_{1,0}$. Thus, we
can implement Diophantine equations as in the proof of Theorem 3.3.

∎

###  3.3. The $\Sigma_{2}$ fragment over two letters in the pure logic

The final result in this section settles the question of how many letters are
needed to make the $\Sigma_{2}$ fragment of
$\FO({A}^{*},\mathord{\sqsubseteq})$ undecidable. We show here that two
letters suffice. Observe that if $|A|=1$, $\FO({A}^{*},\mathord{\sqsubseteq})$
can be interpreted in $\FO(\mathbb{N},<)$ and is thus decidable.

Note that if we have no constants, we cannot define a language in $a^{*}$,
because all definable subsets are closed under automorphisms of
$(A^{*},\mathord{\sqsubseteq})$, in particular under $w\mapsto
w^{\mathsf{rev}}$ and under every morphism $A^{*}\to A^{*}$ that permutes $A$.

######  Corollary 3.6.

Let $|A|\geq 2$. For each recursively enumerable set $S\subseteq\mathbb{N}$,
there is a $\Sigma_{2}$ formula $\tau$ over the structure
$\FO({A}^{*},\mathord{\sqsubseteq})$ that defines the language

$\llbracket\tau\rrbracket=\\{a^{k}\mid a\in A,~{}k\in S\\}.$

In particular, the truth problem for $\Sigma_{2}$ is undecidable.

###### Proof.

Fix a letter $a\in A$. Let $S\subseteq\mathbb{N}$ be recursively enumerable,
let $\varphi$ be the $\Sigma_{1,3}$ formula provided by Theorem 3.3 with
$\llbracket\varphi\rrbracket=\\{a^{k}\mid k\in S\\}$, and let
$w_{1},\ldots,w_{m}\in A^{*}$ be the constants used in the formula $\varphi$.

It was shown in [22] that from $w_{1},\ldots,w_{m}$, one can construct a
$\Sigma_{2}$ formula $\psi$ over $\FO({A}^{*},\mathord{\sqsubseteq})$ with
free variables $V=\\{x_{1},\ldots,x_{m}\\}$ such that for
$\alpha\in(A^{*})^{V}$, we have $\alpha\in\llbracket\psi\rrbracket$ if and
only if there is a morphism $\beta\colon A^{*}\to A^{*}$ that permutes $A$
such that

  1. (1)

$\alpha(x_{i})=\beta(w_{i})$ for every $i\in[1,m]$, or

  2. (2)

$\alpha(x_{i})=\beta(w_{i})^{\mathsf{rev}}$ for every $i\in[1,m]$.

Let $\varphi^{\prime}$ be the formula obtained from $\varphi$ by replacing
every occurrence of $w_{i}$ with $x_{i}$. Consider the formula

$\tau~{}\equiv~{}\exists
x_{1},\ldots,x_{m}\colon\psi~{}\wedge~{}\varphi^{\prime}.$

Then, $\tau$ is clearly a $\Sigma_{2}$ formula and has exactly one free
variable (the same as $\varphi$). We claim that

$\llbracket\tau\rrbracket=\\{b^{k}\mid b\in A,~{}k\in S\\}.$ (5)

If $k\in S$, then $a^{k}\in\llbracket\varphi\rrbracket$ and hence clearly
$b^{k}\in\llbracket\tau\rrbracket$ for each $b\in A$. Moreover, if
$w\in\llbracket\tau\rrbracket$, then for some
$\alpha\in\llbracket\psi\rrbracket$, we have $(\alpha,x\mapsto
w)\models\varphi^{\prime}$. In the case 1, we have
$w\in\beta(\llbracket\varphi\rrbracket)$ and thus $w=\beta(a)^{k}$ with $k\in
S$. In the case 2, we have
$w\in\beta(\llbracket\varphi\rrbracket)^{\mathsf{rev}}$ and thus again
$w=\beta(a)^{k}$ with $k\in S$.

Thus, we have established Eq. 5, which implies that $\tau$ defines an
undecidable set. ∎

##  4\. Complexity

In this section, we study the complexity of the truth problem for the
$\Sigma_{i,j}$ fragments of
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$.

###  4.1. Complexity of $\Sigma_{i,0}$

We begin with the case $j=0$. In the following,
${\ComplexityFont{\Sigma}}_{n}^{\ComplexityFont{EXP}}$ denotes the $n$-th
level of the weak $\EXP$ hierarchy [18, 15].

######  Theorem 4.1.

If $|A|\geq 2$, then the truth problem for $\Sigma_{i,0}$ is $\NP$-complete
for $i=1$ and
${\ComplexityFont{\Sigma}}_{i-1}^{\ComplexityFont{EXP}}$-complete for $i>1$.

We provide a polynomial inter-reduction with the $\Sigma_{i}$ fragment of
$\FO(\mathbb{N},0,1,\mathord{+},\mathord{<})$, a.k.a. Presburger Arithmetic
(PA), for which Haase [17] has recently proven
${\ComplexityFont{\Sigma}}_{i-1}^{\ComplexityFont{EXP}}$-completeness for
$i>1$. The $\Sigma_{1}$ fragment of PA is $\NP$-complete [31].

The reduction from PA to $\Sigma_{1,0}$ fixes a letter $a\in A$ and encodes
every number $k\in\mathbb{N}$ by $a^{k}$. Addition can then be expressed in
$\Sigma_{1,0}$ (Item 11 of Theorem 3.3). Note that although this ostensibly
works with one letter, we need another letter in $A$ to express addition. This
is crucial: If $|A|=1$, then
$\FO({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$ is just
$\FO(\mathbb{N},<)$, which has a $\PSPACE$-complete truth problem [12, 34].
Moreover, an inspection of the proof of Theorem 3.3 shows that an alternation
bound of $\ell=2$ suffices to define addition, which is tight: if we only use
a bound of $1$, we can also easily reduce to $\FO(\mathbb{N},<)$.

The reduction from $\Sigma_{i,0}$ to Presburger arithmetic encodes a word $w$
known to belong to $(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, i.e., of the form

$\prod_{i=1}^{\ell}\prod_{j=1}^{n}a_{j}^{x_{i,j}},$

by the vector $(x_{1,1},\ldots)\in\mathbb{N}^{\ell\cdot n}$ of exponents. With
this encoding, it suffices to show how to express literals $w\sqsubseteq
w^{\prime}$ (and also $w\not\sqsubseteq w^{\prime}$) by polynomial-size
existential Presburger formulas for $w,w^{\prime}\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell}$. For a vector $x=(x_{1,1},\ldots,x_{\ell,n})$ from
$\mathbb{N}^{\ell\cdot n}$, let
$w_{x}=\prod_{i=1}^{\ell}\prod_{j=1}^{n}a_{j}^{x_{i,j}}$.

######  Proposition 4.2.

There are existential Presburger formulas $\varphi$ and $\psi$ of size
polynomial in $n$ and $\ell$ such that

$\displaystyle\varphi(x_{1,1},\ldots,x_{\ell,n},y_{1,1},\ldots,y_{\ell,n})\iff
w_{x}\sqsubseteq w_{y},$
$\displaystyle\psi(x_{1,1},\ldots,x_{\ell,n},y_{1,1},\ldots,y_{\ell,n})\iff
w_{x}\not\sqsubseteq w_{y}.$

Let us briefly describe these formulas. Let $I=[1,\ell]\times[1,n]$ and order
the pairs $(i,j)\in I$ lexicographically: $(i^{\prime},j^{\prime})<(i,j)$ if
$i^{\prime}<i$ or $i=i^{\prime}$ and $j^{\prime}<j$. This captures the order
of the $a_{j}^{x_{i,j}}$ factors in $w_{x}$. We now define formulas
$\tau_{i,j}$ and $\eta_{i,j}$ where the $t_{i,j,k}$’s and $e_{i,j,k}$’s are
extra free variables:

$\displaystyle\tau_{i,j}\colon$ $\displaystyle\bigwedge_{1\leq
k\leq\ell}t_{i,j,k}$ $\displaystyle=\begin{cases}0\quad\text{if
$e_{i^{\prime},j^{\prime},k^{\prime}}>0$ for some}\\\
\quad\quad\quad(i^{\prime},j^{\prime})<(i,j)\text{ and }k^{\prime}>k\\\
y_{k,j}-\sum_{i^{\prime}=1}^{i-1}e_{i^{\prime},j,k}\quad\text{otherwise}\end{cases}$
$\displaystyle\eta_{i,j}\colon$ $\displaystyle\bigwedge_{1\leq
k\leq\ell}e_{i,j,k}$
$\displaystyle=\min\left\\{t_{i,j,k}~{},~{}x_{i,j}-\sum_{r=1}^{k-1}e_{i,j,r}\right\\}$

These expressions define the leftmost embedding of $w_{x}$ into $w_{y}$: the
variable $t_{i,j,k}$ describes how many letters from $a_{j}^{y_{k,j}}$ are
available for embedding the $a_{j}^{x_{i,j}}$ factor of $w_{x}$ into $w_{y}$.
The variable $e_{i,j,k}$ counts how many of these available letters are
actually used for the $a_{j}^{x_{i,j}}$ factor in the left-most embedding of
$w_{x}$ into $w_{y}$. Since $i$ and $j,k$ are bounded by $n$ and $\ell$, we
have polynomially many formulas of polynomial size.

Define $\xi=\bigwedge_{(i,j)\in I}\tau_{i,j}\wedge\eta_{i,j}$ and the formulas
$\varphi,\psi$ as:

$\displaystyle\begin{array}[]{c}\exists t_{1,1,1}\cdots\exists
t_{\ell,n,\ell}\\\ \quad\exists e_{1,1,1}\cdots\exists
e_{\ell,n,\ell}\end{array}\colon\xi\wedge\bigwedge_{(i,j)\in
I}\left(x_{i,j}\leq\sum_{k=1}^{\ell}e_{i,j,k}\right)$ (8)
$\displaystyle\begin{array}[]{c}\exists t_{1,1,1}\cdots\exists
t_{\ell,n,\ell}\\\ \quad\exists e_{1,1,1}\cdots\exists
e_{\ell,n,\ell}\end{array}\colon\xi\wedge\bigvee_{(i,j)\in
I}\left(x_{i,j}>\sum_{k=1}^{\ell}e_{i,j,k}\right)$ (11)

Since formulas $\tau_{i,j}$ and $\eta_{i,j}$ are inductive equations that
uniquely define the values of $t_{i,j,k}$ and $e_{i,j,k}$ as functions of the
$x$ and $y$ vectors, $\psi$ is equivalent to the negation of $\varphi$.
Moreover, $\varphi$ expresses that there is enough room to embed each factor
$a_{j}^{x_{i,j}}$ in $w_{y}$, i.e., that $w_{x}\sqsubseteq w_{y}$ as claimed,
and both formulas are easily constructed in polynomial time.

###  4.2. Complexity of $\Sigma_{1,1}$

######  Theorem 4.3.

The truth problem for the $\Sigma_{1,1}$ fragment is $\NP$-complete.

Of course, hardness is inherited from $\Sigma_{1,0}$. Conversely,
$\NP$-membership is shown by a reduction to the $\Sigma_{1,0}$ fragment. For
this reduction, we first explain how a single “unbounded” word can be made
alternation bounded while respecting its relationships with other alternation
bounded words.

For this we use a slightly different measure of alternation levels for words:
we factor words in _blocks_ of repeating letters, writing
$u=\prod_{i=1}^{k}{a_{i}}^{\ell_{i}}$ with $\ell_{i}>0$ and
$a_{i}\not=a_{i+1}$ for all $i$. By “an $a$-block of $u$” we mean an
occurrence of a factor $a_{i}^{\ell_{i}}$ with $a_{i}=a$. We note that
requiring some bound in the number of blocks is equivalent to bounding the
number of alternation when it comes to defined the $\Sigma_{i,j}$ fragments.
However, counting blocks is more precise.

######  Lemma 4.4.

Let $t,x_{1},\dots,x_{n},y_{1},\dots,y_{m}\in A^{*}$ such that:

  * •

for all $i$, $x_{i}\sqsubseteq t$,

  * •

for all $j$, $y_{j}\not\sqsubseteq t$,

  * •

for all $i$ and $j$, $x_{i}$ and $y_{j}$ have less than $\ell$ blocks,

  * •

$t$ has $k>(m+n)\cdot\ell+|A|$ blocks.

Then there exists $t^{\prime}\in A^{*}$ such that:

  * •

for all $i$, $x_{i}\sqsubseteq t^{\prime}$,

  * •

for all $j$, $y_{j}\not\sqsubseteq t^{\prime}$,

  * •

$t^{\prime}$ has either $k-1$ or $k-2$ blocks.

###### Proof.

Given $u\in A^{*}$, we write $\operatorname{Im}u$ for the image of the left-
most embedding of $u$ into $t$. This is a set of positions in $t$ and, in case
$u\not\sqsubseteq t$, these positions only account for the longest prefix of
$u$ that can be embedded in $t$. In particular, and since we assumed
$x_{i}\sqsubseteq t$ and $y_{j}\not\sqsubseteq t$, then
$|\operatorname{Im}x_{i}|=|x_{i}|$ and $|\operatorname{Im}y_{j}|<|y_{j}|$ for
all $i,j$.

Let $b_{0}$ be an $a$-block of $t$. This block is said to be _irreducible_ if
either (1) it is the last, i.e. right-most, $a$-block of $t$, or (2) writing
$t$ under the form $t=t_{0}b_{0}t_{1}b_{1}t_{2}$ where $b_{1}$ is the next
$a$-block, i.e. $a\notin t_{1}$, one of the following holds:

  * •

there is some $i$ s.t. $b_{0}\cap\operatorname{Im}x_{i}\neq\emptyset$ and
$t_{1}\cap\operatorname{Im}x_{i}\neq\emptyset$.

  * •

there is $j$ s.t. $b_{0}\cap\operatorname{Im}y_{j}=\emptyset$ and
$t_{1}\cap\operatorname{Im}y_{j}\neq\emptyset$ and
$b_{1}\cap\operatorname{Im}y_{j}\neq\emptyset$.

Otherwise $b_{0}$ is said to be _reducible_.

Claim: $t$ contains a reducible block.

Indeed, every irreducible block is either a right-most $a$-block for some $a$,
or can be associated with a letter alternation in some $x_{i}$, or in some
$y_{j}$. Furthermore, this association is injective. Thus there are at most
$(n+m)\cdot\ell$ irreducible blocks that are not right-most (and at most $|A|$
right-most blocks). Since $k>(n+m)\cdot\ell+|A|$, $t$ has a reducible block.

So let us pick one such reducible block, say an $a$-block $b_{0}$, write $t$
under the form $t=t_{0}b_{0}t_{1}b_{1}t_{2}$ as above, and let
$t^{\prime}=t_{0}t_{1}b_{0}b_{1}t_{2}$.

Claim: $t^{\prime}$ fulfills the requirements of Lemma 4.4.

Since $b_{1}$ is an $a$-block, $b_{0}b_{1}$ is now a block of $t^{\prime}$ and
$t^{\prime}$ has less than $k$ blocks. Moreover, the only other possible block
merge is in $t_{0}t_{1}$, thus $t^{\prime}$ has at least $k-2$ blocks. We now
show that $x_{i}\sqsubseteq t^{\prime}$ and $y_{j}\not\sqsubseteq t^{\prime}$
for all $i,j$.

  * •

Pick some $i$. Since $x_{i}\sqsubseteq t$, there is a unique decomposition
$x_{i}=u_{0}u_{1}u_{2}u_{3}u_{4}$ of $x_{i}$ such that
$\operatorname{Im}u_{0}\subseteq t_{0}$, $\operatorname{Im}u_{1}\subseteq
b_{0}$, $\operatorname{Im}u_{2}\subseteq t_{1}$,
$\operatorname{Im}u_{3}\subseteq b_{1}$ and $\operatorname{Im}u_{4}\subseteq
t_{2}$. Since $b_{0}$ is reducible one of $\operatorname{Im}u_{1}$ or
$\operatorname{Im}u_{2}$ is empty. Thus one of $u_{1}$ or $u_{2}$ is the empty
word, allowing $x_{i}\sqsubseteq t^{\prime}$.

  * •

Assume, by way of contradiction, that for some $j$, $y_{j}\sqsubseteq
t^{\prime}$. Let $z_{1}$ be the maximal prefix of $y_{j}$ that embeds into
$t$. We proceed to show that $b_{0}$ is irreducible.

    * –

First, $b_{0}\cap\operatorname{Im}z_{1}=\emptyset$. Otherwise, since $a\notin
t_{1}$, the left-most embedding of $z_{1}$ into
$t^{\prime}=t_{0}t_{1}b_{0}b_{1}t_{2}$ does not use $t_{1}$ at all and we
would have $y_{j}\sqsubseteq t_{0}b_{0}b_{1}t_{2}\sqsubseteq t$.

    * –

Secondly, $t_{1}\cap\operatorname{Im}z_{1}$ is not empty. If it were, since
$b_{0}$ is made of $a$’s only and $a\notin t_{1}$, the left-most embedding of
$z_{1}$ into $t_{0}t_{1}b_{0}b_{1}t_{2}$ would not use $t_{1}$ and again we
would have $y_{j}\sqsubseteq t_{0}b_{0}b_{1}t_{2}\sqsubseteq t$.

    * –

Lastly, $b_{1}\cap\operatorname{Im}z_{1}\neq\emptyset$. Otherwise, the already
established condition $b_{0}\cap\operatorname{Im}z_{1}=\emptyset$ implies that
$y_{j}$ embeds not only in $t^{\prime}$ but in $t_{0}t_{1}t_{2}$, which is a
subword of $t$.

Since $b_{0}$ is reducible, we conclude that the original assumption that
$y_{j}\sqsubseteq t^{\prime}$ does not hold, i.e., that $y_{j}\not\sqsubseteq
t^{\prime}$ as required.

∎

We now proceed to prove Theorem 4.3: as announced we show how any
$\Sigma_{1,1}$ sentence can be replaced by an equivalent $\Sigma_{1,0}$
sentence.

Let $\varphi$ be a $\Sigma_{1,1}$ sentence, where $t$ is the only variable
which is not alternation bounded. Consider an existential quantification of
$t$ in $\varphi$, i.e., a subformula of the form $\exists t:\psi$. Any free
occurrence of $t$ in $\psi$ is in a literal of one of the following types:

  1. (i)

$x\sqsubseteq t$, where $x$ is an alternation bounded variable,

  2. (ii)

$y\not\sqsubseteq t$, where $x$ is an alternation bounded variable,

  3. (iii)

$t\not\sqsubseteq u$, where $u$ is an alternation bounded variable,

  4. (iv)

$t\sqsubseteq z$, where $z$ is an alternation bounded variable,

  5. (v)

$t\sqsubseteq t$,

  6. (vi)

$t\not\sqsubseteq t$.

Assertions of types (v) and (vi) can be replaced by their truth value. If a
literal $t\sqsubseteq z$ of type (iv) occurs in $\exists t:\psi$, then that
formula is equivalent to $\exists t\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell}\colon\psi$, where $\ell$ is the alternation bound of
variable $z$.

Otherwise, only literals of types (i), (ii) and (iii) occur in $\psi$. Let $n$
be the number of variables $x$ that occur in literals of type (i), $m$ the
number of variables $y$ that occur in literals of type (ii), $\ell$ the
maximum alternation level of these variables, and $k$ the maximum alternation
level of all variables $u$ that appear in literals of type (iii). Let

$p=\max\\{(m+n)\cdot(\ell\cdot|A|)+|A|,~{}k\cdot|A|+3\\}.$

(here $\ell$ and $k$ are multiplied by $|A|$ to obtain a number of blocks from
a maximum alternation). Then $\exists t:\psi$ is equivalent to $\exists
t\in(a_{1}^{*}\cdots a_{n}^{*})^{p}:\psi$. Indeed, if the restricted formula
has a solution, it is a solution for $\psi$. Conversely, if $\psi$ is
satisfiable via some $t\in A^{*}$ having more than $p$ blocks, then by Lemma
4.4, one can also use a $t$ having between $k\cdot|A|$ and $p$ blocks. The
fact that $t$ has more than $k\cdot|A|$ blocks ensures that all literals
$t\not\sqsubseteq u$ are still satisfied.

Finally, we can replace every $\exists t$ in $\varphi$ by a bounded
quantification and obtain an equivalent formula in $\Sigma_{1,0}$ which proves
Theorem 4.3

To the authors’ knowledge, the following was not known.

######  Corollary 4.5.

If PT languages are represented as boolean combinations of sets of the form
${\uparrow}{w}$ with $w\in A^{*}$, then their non-emptiness problem is
$\NP$-complete.

Membership in $\NP$ follows from Theorem 4.3. For hardness, we can reduce CNF-
SAT as follows. We encode an assignment
$\alpha\colon\\{x_{1},\ldots,x_{n}\\}\to\\{0,1\\}$ as a word
$ba^{\alpha(x_{1})}ba^{\alpha(x_{2})}\cdots ba^{\alpha(x_{n})}$. With literals
$x_{i}$ and $\neg x_{i}$, we associate the languages
$K_{x_{i}}={\uparrow}{b^{i}ab^{n-i}}$ and $K_{\neg
x_{i}}=\\{a,b\\}^{*}\smallsetminus{\uparrow}{b^{i}ab^{n-i}}$. A clause
$C=L_{1}\vee\cdots\vee L_{m}$ is then translated to
$K_{C}=K_{L_{1}}\cup\cdots\cup K_{L_{n}}$ and the conjunction
$C_{1}\wedge\cdots\wedge C_{k}$ results in the language
$(b(a+\varepsilon))^{n}\cap K_{C_{1}}\cap\cdots\cap K_{C_{k}}$.

In particular, given a finite number of PT languages, the problem of deciding
whether they intersect is $\NP$-complete. This is in contrast with general
regular languages represented by DFAs (or NFAs), for which the problem is
well-known to be $\PSPACE$-complete [27].

###  4.3. Complexity of $\Sigma_{1,2}$

Our next result is an upper bound for the truth problem of $\Sigma_{1,2}$.

######  Theorem 4.6.

The truth problem for $\Sigma_{1,2}$ is in $\NEXP$.

We prove Theorem 4.6 in two steps. The first step of our decidability result
is to transform a $\Sigma_{1,2}$ formula into a system of constraints where
the relations among those variables without an alternation bound have a tree
shape. In the second step, we exploit the tree shape to construct an
exponential-size counter automaton for the set of satisfying assignments.

### Tree-shaped constraints

Let $A=\\{a_{1},\ldots,a_{n}\\}$ and let $V$ be a set of variables. A
_constraint system_ is a set of constraints of the form $x\sqsubseteq y$,
$x\not\sqsubseteq y$, $x=y$, $x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, or
$x=w$, where $x,y\in V$, $\ell\in\mathbb{N}$ and $w\in A^{*}$. A constraint of
the form $x\sqsubseteq y$, $x\not\sqsubseteq y$, or $x=y$ is also called
_$(x,y)$ -constraint_ or _$(y,x)$ -constraint_. Constraints of the form
$x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$ are called _alternation constraints_.
The set of assignments $\alpha\in(A^{*})^{V}$ that satisfy $S$ is denoted by
$\llbracket S\rrbracket$. For a subset $U\subseteq V$, by existentially
quantifying all variables outside of $U$, the constraint system $S$ also
defines a set of assignments in $(A^{*})^{U}$, which we denote by $\llbracket
S\rrbracket_{U}$.

For a constraint system $S$ over $V$, we define the graph $\Gamma(S)=(V,E)$
where $\\{x,y\\}\in E$ if and only if $S$ contains an $(x,y)$-constraint. We
say that $S$ is _tree-shaped_ if $\Gamma(S)$ is a forest. Furthermore, $S$ is
called _alternation bounded_ if every variable occurring in $S$ also has an
alternation constraint in $S$.

######  Proposition 4.7.

For any disjunction-free $\Sigma_{1,2}$-formula $\varphi$, one can construct
polynomial-size constraint systems $T$ and $S$ over variables
$V^{\prime}\supseteq\mathsf{fv}(\varphi)$ such that

  1. (1)

$T$ is tree-shaped,

  2. (2)

$S$ is alternation bounded, and

  3. (3)

$\llbracket T\cup
S\rrbracket_{\mathsf{fv}(\varphi)}=\llbracket\varphi\rrbracket$.

###### Proof.

We will need the notion of quotients of constraint systems. The idea is to
identify certain pairs of variables. Suppose $S$ is a constraint system over
$V$. Furthermore, let $\sim\subseteq V\times V$ be an equivalence relation
that specifies which variables we want to identify with each other. Then we
define the _quotient_ $S/\mathord{\sim}$ as a constraint system over the
variable set $V/\mathord{\sim}$ with the constraints

$\displaystyle S/\mathord{\sim}~{}=$
$\displaystyle~{}\\{[x]\delta[y]\mid\delta\in\\{\sqsubseteq,\not\sqsubseteq\\},~{}(x\delta
y)\in S\\}.$ $\displaystyle\cup~{}\\{[x]=w\mid(x=w)\in S\\}$
$\displaystyle\cup~{}\\{[x]\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell}\mid(x\in(a_{1}^{*}\cdots a_{n})^{\ell})\in S\\}$

In the course of constructing the constraint systems, it will be convenient to
assume that two constraint systems are defined over disjoint sets of
variables. To this end, we need some notation to state that a constraint
system is equivalent to a formula even though its variables have different
names. Suppose we have a constraint system $S$ over the set of variables
$V^{\prime}$ and $\psi\colon\mathsf{fv}(\varphi)\to V^{\prime}$ is an
injective map. Then, via $\psi$, the formula $\varphi$ defines a set of
assignments
$\llbracket\varphi\rrbracket_{\psi}\subseteq(A^{*})^{\mathsf{im}(\psi)}$. We
say that $\varphi$ and $S$ are _$\psi$ -equivalent_ if $\llbracket
S\rrbracket_{\mathsf{im}(\psi)}=\llbracket\varphi\rrbracket_{\psi}$.

We may clearly assume that all literals are of the form $x\sqsubseteq y$,
$x\not\sqsubseteq y$, or $x=w$ for $w\in A^{*}$ (and there are no literals
$w\sqsubseteq x$ etc.).

We show the following stronger statement. Let $B$ be the set of variables in
$\varphi$ that are alternation bounded. For each disjunction-free
$\Sigma_{1,2}$-formula $\varphi$, there is a set of variables $V^{\prime}$,
constraint systems $T$ and $S$ over $V^{\prime}$, an injective map
$\psi\colon\mathsf{fv}(\varphi)\to V^{\prime}$ such that the following holds.
If $B^{\prime}\subseteq V^{\prime}$ denotes the set of variables for which
there is an alternation bound in $S$, then

  1. (i)

$T$ is tree-shaped,

  2. (ii)

$S$ is alternation-bounded,

  3. (iii)

$T\cup S$ and $\varphi$ are $\psi$-equivalent,

  4. (iv)

for every $x\in B$ we have $\psi(x)\in B^{\prime}$, and

  5. (v)

if $|\mathsf{fv}(\varphi)\smallsetminus B|=2$ with
$\mathsf{fv}(\varphi)\smallsetminus B=\\{x,y\\}$, then $\psi(x)$ and $\psi(y)$
are either neighbors in $\Gamma(T)$ or in distinct components.

To prove this statement by induction, we need to consider three cases.

  1. (1)

Literals, i.e. $x\sqsubseteq y$, $x\not\sqsubseteq y$, or $x=w$. There are
only two variables so we can just take the literal as the set $T$ and let $S$
contain the global alternation constraints for the variables in the literal.

  2. (2)

Existentially quantified formulas $\exists x\colon\varphi$. Here, we just
reduce the set of free variables, so it suffices to adjust the map $\psi$.

  3. (3)

Conjunctions $\varphi\equiv\varphi_{0}\wedge\varphi_{1}$. Suppose we have
constructed $T_{i},S_{i},V^{\prime}_{i},\psi_{i},B^{\prime}_{i}$ as above for
$i=0,1$. We may clearly assume $V_{0}\cap V_{1}=\emptyset$. We construct
$T,S,V^{\prime},\psi,B^{\prime}$ as follows. Let
$\sim\subseteq(V^{\prime}_{0}\cup V^{\prime}_{1})\times(V^{\prime}_{0}\cup
V^{\prime}_{1})$ be the smallest equivalence relation with
$\psi_{0}(x)\sim\psi_{1}(x)$ for all $x\in\mathsf{fv}(\varphi)\smallsetminus
B$. Then we take $V^{\prime}=(V^{\prime}_{0}\cup
V^{\prime}_{1})/\mathord{\sim}$ and define $T=(T_{0}\cup
T_{1})/\mathord{\sim}$. Moreover, let

$S=S_{0}\cup S_{1}\cup\\{[\psi_{0}(x)]=[\psi_{1}(x)]\mid
x\in\mathsf{fv}(\varphi)\cap B\\}.$

Moreover, we choose $\psi\colon\mathsf{fv}(\varphi)\to V^{\prime}$ so that
$\psi(x)=\psi_{0}(x)$ if $x\in\mathsf{fv}(\varphi_{0})$ and
$\psi(x)=\psi_{1}(x)$ if $x\notin\mathsf{fv}(\varphi_{0})$.

It is clear that Items (ii), (iii) and (iv) above are satisfied. It remains to
verify Items (i) and (v). We distinguish the following cases.

     * •

$|\mathsf{fv}(\varphi_{i})\smallsetminus B|\leq 1$ for some $i\in\\{0,1\\}$.
Then there is at most one variable in $V^{\prime}_{i}$ that is identified with
a variable in $V^{\prime}_{1-i}$ by $\sim$. Hence, $\Gamma(T)$ is obtained
from $\Gamma(T_{0})$ and $\Gamma(T_{1})$ either by disjoint union or by
identifying one vertex from $\Gamma(T_{0})$ with one vertex from
$\Gamma(T_{1})$. In any case, $\Gamma(T)$ is a forest. Hence, Item (i) is
satisfied.

Let us now show Item (v). Hence, assume $|\mathsf{fv}(\varphi)\smallsetminus
B|=2$ with $\mathsf{fv}(\varphi)\smallsetminus B=\\{x,y\\}$.

Clearly, if $\mathsf{fv}(\varphi_{0})\smallsetminus B$ and
$\mathsf{fv}(\varphi_{1})\smallsetminus B$ are disjoint, then no variables are
identified and hence $\psi(x)$ and $\psi(y)$ are in distinct components of
$\Gamma(T)$. Hence, we assume that $\mathsf{fv}(\varphi_{0})\smallsetminus B$
and $\mathsf{fv}(\varphi_{1})\smallsetminus B$ have a variable in common, say
$x$.

Since $|\mathsf{fv}(\varphi_{0})\smallsetminus B|\leq 1$, this means
$\mathsf{fv}(\varphi_{1})\smallsetminus B=\\{x,y\\}$ and hence $\psi_{1}(x)$
and $\psi_{1}(y)$ are neighbors in $\Gamma(T_{1})$ or they are in distinct
components of $\Gamma(T_{1})$.

$\Gamma(T)$ is obtained from $\Gamma(T_{0})$ and $\Gamma(T_{1})$ by
identifying $\psi_{0}(x)$ and $\psi_{1}(x)$. Therefore, $\psi(x)$ and
$\psi(y)$ are neighbors in $\Gamma(T)$ if and only if they are neighbors in
$\Gamma(T_{1})$. Moreover, they are in disjoint components of $\Gamma(T)$ if
and only if they are in disjoint components of $\Gamma(T_{1})$. This proves
Item (v).

     * •

$|\mathsf{fv}(\varphi_{0})|=|\mathsf{fv}(\varphi_{1})|=2$. Write
$\mathsf{fv}(\varphi_{0})\smallsetminus B=\mathsf{fv}(\varphi_{1})=\\{x,y\\}$.
Note that $\Gamma(T)$ is obtained from $\Gamma(T_{0})$ and $\Gamma(T_{1})$ by
identifying $\psi_{0}(x)$ with $\psi_{1}(x)$ and identifying $\psi_{0}(y)$
with $\psi_{1}(y)$. Since for each $i\in\\{0,1\\}$ we know that $\psi_{i}(x)$
and $\psi_{i}(y)$ are either neighbors in $\Gamma(T_{i})$ or in distinct
components, this clearly implies that $\Gamma(T)$ is a forest. Hence, we have
shown Item (i).

Moreover, if for some $i\in\\{0,1\\}$, $\psi_{i}(x)$ and $\psi_{i}(y)$ are
neighbors in $\Gamma(T_{i})$, then $\psi(x)$ and $\psi(y)$ are neighbors in
$\Gamma(T)$. Otherwise, $\psi(x)$ and $\psi(y)$ are in disjoint components of
$\Gamma(T)$. This proves Item (v).

∎

### Counter automata

In the next step, we exploit the decomposition into a tree-shaped constraint
system and an alternation-bounded constraint system to reduce satisfiability
to non-emptiness of counter automata. To this end, we use a type of counter
automata known as _Parikh automata_ [25, 7]. In terms of expressiveness, these
are equivalent to the classical reversal-bounded counter automata [20], but
their syntax makes them convenient for our purposes.

Let $V$ be a finite set of variables. A _counter automaton over $V$_ is a
tuple $\mathcal{A}=(Q,A,C,E,q_{0},F)$, where $Q$ is a finite set of _states_ ,
$A$ is the input alphabet, $C$ is a set of _counters_ ,

$E\subseteq Q\times(A\cup\\{\varepsilon\\})^{V}\times\mathbb{N}^{C}\times Q$

is the finite set of _edges_ , $q_{0}\in Q$ is the _initial state_ , and $F$
is a finite set of pairs $(q,\varphi)$, where $q\in Q$ and $\varphi$ is an
existential Presburger formula with free variables in $C$. A _configuration of
$\mathcal{A}$_ is a tuple $(q,\alpha,\mu)$, where $q\in Q$,
$\alpha\in(A^{*})^{V}$, $\mu\in\mathbb{N}^{C}$. The step relation is defined
as follows. We have
$(q,\alpha,\mu)\rightarrow_{\mathcal{A}}(q^{\prime},\alpha^{\prime},\mu^{\prime})$
iff there is an edge $(q,\beta,\nu,q^{\prime})\in E$ such that
$\alpha^{\prime}=\alpha\beta$ and $\mu^{\prime}=\mu+\nu$. A counter automaton
accepts a set of assignments, namely

$\displaystyle L(\mathcal{A})=\\{\alpha\in(A^{*})^{V}\mid\exists(q,\varphi)\in
F\colon(q_{0},\varepsilon,0)\xrightarrow{*}_{\mathcal{A}}(q,\alpha,\mu),~{}\mu\models\varphi\\}$

We call a subset $R\subseteq(A^{*})^{V}$ a _counter relation_ if there is a
counter automaton $\mathcal{A}$ with $R=L(\mathcal{A})$. If $|V|=1$, say
$V=\\{x\\}$, then $\mathcal{A}$ defines a subset of $A^{*}$, namely the
language $\\{w\in A^{*}\mid(x\mapsto w)\in L(\mathcal{A})\\}$. Languages of
this form are called _counter languages_.

Suppose $V_{0},V_{1}$ are sets of variables with $|V_{0}\cap V_{1}|\leq 1$.
Let $\mathcal{A}_{i}=(Q_{i},A,C_{i},E_{i},q_{0,i},F_{i})$ be a counter
automaton over $V_{i}$ for $i=0,1$ such that $C_{0}\cap C_{1}=\emptyset$. Then
a simple product construction yields a counter automaton
$\mathcal{A}_{0}\otimes\mathcal{A}_{1}=(Q_{0}\times Q_{1},A,C_{0}\cup
C_{1},E,(q_{0,0},q_{0,1}),F)$ over $V_{0}\cup V_{1}$ such that
$((p_{0},p_{1}),\alpha,\mu)\xrightarrow{*}_{\mathcal{A}_{0}\otimes\mathcal{A}_{1}}((p^{\prime}_{0},p^{\prime}_{1}),\alpha^{\prime},\mu^{\prime})$
iff

$\displaystyle(p_{i},\alpha|_{V_{i}},\mu|_{C_{i}})\xrightarrow{*}_{\mathcal{A}_{i}}(p^{\prime}_{i},\alpha^{\prime}|_{V_{i}},\mu^{\prime}|_{C_{i}})$

for $i=0,1$ and

$F=\\{((p_{0},p_{1}),\varphi_{0}\wedge\varphi_{1})\mid\text{$(p_{i},\varphi_{i})\in
F_{i}$ for $i=0,1$}\\}.$

######  Proposition 4.8.

Given a tree-shaped constraint system $T$, one can construct in exponential
time a counter automaton $\mathcal{A}$ with $L(\mathcal{A})=\llbracket
T\rrbracket$.

###### Proof.

First, observe that it suffices to consider the case where every constraint in
$T$ involves two variables: The other constraints have the form $x=w$ for some
$w\in A^{*}$ or $x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$ for some
$\ell\in\mathbb{N}$ and can thus be imposed afterwards.

We construct the automaton inductively. The statement is trivial if $T$
involves only one variable, so assume $|V|\geq 2$ from now on.

Since $\Gamma(T)$ is a forest, it contains a vertex $x\in V$ with at most one
neighbor. Let $T^{\prime}$ be the constraint system obtained from $T$ by
removing all constraints involving $x$ and suppose we have already constructed
a counter automaton $\mathcal{A}^{\prime}$ with
$L(\mathcal{A}^{\prime})=\llbracket T^{\prime}\rrbracket$.

Now if $x$ has no neighbor, it is easy to construct the automaton for $T$. So
suppose $x$ has a unique neighbor $y$. Then, the additional constraints
imposed in $T$ are all $(x,y)$-constraints. Let $T^{\prime\prime}$ be the set
of all $(x,y)$-constraints in $T$. Now note that if
$\mathcal{A}^{\prime\prime}$ is a counter automaton with
$L(\mathcal{A}^{\prime\prime})=\llbracket T^{\prime\prime}\rrbracket$, then we
have

$L(\mathcal{A}^{\prime}\otimes\mathcal{A}^{\prime\prime})=\llbracket
T^{\prime}\cup T^{\prime\prime}\rrbracket=\llbracket T\rrbracket.$

Therefore, it suffices to construct in polynomial time a counter automaton
$\mathcal{A}^{\prime\prime}$ with $L(\mathcal{A}^{\prime\prime})=\llbracket
T^{\prime\prime}\rrbracket$.

Observe that any set of $(x,y)$-constraints can be written as a disjunction of
one of the following constraints:

(i) $x=y$ (ii) $x\sqsubset y$ (iii) $y\sqsubset x$ (iv) $x\bot y$

Since it is easy to construct a counter automaton for the union of two
relations accepted by counter automata, it suffices to construct a counter
automaton for the set of solutions to each of the constraints (i)—(iv). This
is obvious in all cases but the last. In the last case, one can notice that
$x\bot y$ holds if either  (1) $|x|<|y|$and $x\not\sqsubseteq y$ or  (2)
$|y|<|x|$and $y\not\sqsubseteq x$ or  (3) $|x|=|y|$and $x\neq y$.  Note that
each of these cases is easily realized in a counter automaton since we can use
the counters to guarantee the length constraints. Moreover, the resulting
counter automaton can clearly be constructed in polynomial time, which
completes the proof. ∎

We can now prove Theorem 4.6 by taking the constraint system provided by
Proposition 4.7 and construct a counter automaton just for $T$ using
Proposition 4.8. Then, we can impose the constraints in $S$ by using
additional counters. Note that since all variables in $S$ are alternation
bounded, we can store these words, in the form of their occurring exponents,
in counters. We can then install the polynomial-size Presburger formulas from
Proposition 4.2 in the counter automaton to impose the binary constraints
required by $S$. This results in an exponential size counter automaton that
accepts the satisfying assignments of $\varphi$. The $\NEXP$ upper bound then
follows from the fact that non-emptiness for counter automata is
$\NP$-complete (Lemma 4.9).

Since counter automata are only a slight extension of reversal-bounded counter
automata, the following is well-known.

######  Lemma 4.9.

The non-emptiness problem for counter automata is $\NP$-complete.

###### Proof.

Given a counter automaton $\mathcal{A}=(Q,A,C,E,q_{0},F)$, and a state $q\in
Q$, we can construct an existential Presburger formula $\theta_{q}$ with a
free variable for each edge in $\mathcal{A}$ that is satisfied for an
assignment $\nu\in\mathbb{N}^{E}$ iff there is a run from $q_{0}$ to $q$ where
each edge $e\in E$ occurs exactly $\nu(e)$ times. This is just the fact that
we can construct in polynomial time an existential Presburger formula for the
Parikh image of a finite automaton [35].

For each edge $e=(p,\alpha,\mu,p^{\prime})$, define $\mu_{e}=\mu$. Then the
formula

$\bigvee_{(q,\varphi)\in F}\theta_{q}\wedge\bigwedge_{c\in C}c=\mu_{e}(c)\cdot
e\wedge\varphi$

expresses precisely that there is an accepting run. The fact that the
satisfiability problem for existential Presburger arithmetic is $\NP$-complete
[31] now gives us the upper bound as well as the lower bound. ∎

We are now ready to prove Theorem 4.6.

###### Proof.

First we use Proposition 4.7 to turn the formula $\varphi$ into constraint
systems $T$ and $S$ such that $T$ is tree-shaped, $S$ is alternation bounded,
and $\llbracket T\cup
S\rrbracket_{\mathsf{fv}(\varphi)}=\llbracket\varphi\rrbracket$. Then we use
Proposition 4.8 to to obtain in exponential time a counter automaton
$\mathcal{A}$ with $L(\mathcal{A})=\llbracket T\rrbracket$.

Let $U=\\{x_{1},\ldots,x_{m}\\}$ be the set of variables occurring in $S$. It
remains to impose the constraints in $S$. We do this by first building the
product with one automaton $\mathcal{A}_{i}$ for each $x_{i}$. This automaton
imposes the alternation constraint on $x_{i}$ and stores the word read into
$x_{i}$ in a set of counters. Note that this is possible because the word is
alternation bounded. After taking the product with all these automata, we
impose the remaining constraints from $S$ (which are binary constraints or of
the form $x=w$ with $x\in U$, $w\in A^{*}$) by adding existential Presburger
formulas that express subword constraints as provided by Proposition 4.2.

We may clearly assume that whenever there is a variable $x$, an alternation
constraint $x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, and a constraint $x=w$,
then $w\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$: Otherwise, the system is not
satisfiable and clearly has an equivalent counter automaton.

Let $A=\\{a_{1},\ldots,a_{n}\\}$. Since $S$ is alternation bounded, $S$
contains an alternation constraint $x_{i}\in(a_{1}^{*}\cdots
a_{n}^{*})^{\ell_{i}}$ for each $i\in[1,m]$. Let $\ell$ be the maximum of all
these $\ell_{i}$. We will use the counter variables $c_{i,j,k}$ for each
$i\in[1,m]$, $j\in[1,\ell]$, and $k\in[1,n]$. We set up the automaton
$\mathcal{A}_{i}$ over $V_{i}=\\{x_{i}\\}$ such that it has an initial state
$q_{0}$, a state $q_{1}$, and satisfies

$(q_{0},\varepsilon,0)\xrightarrow{*}_{\mathcal{A}_{i}}(q_{1},\alpha,\mu)$

if and only if $\alpha$ maps $x_{i}$ to the word

$a_{1}^{\mu(c_{i,1,1})}\cdots a_{n}^{\mu(c_{i,1,n})}\cdots
a_{1}^{\mu(c_{i,\ell_{i},1})}\cdots a_{n}^{\mu(c_{i,\ell_{i},n})}.$ (12)

This can clearly be done with $n\cdot\ell$ states. Moreover, let
$F_{i}=\\{(q_{1},\top)\\}$. Note that $\mathcal{A}_{i}$ has the counters
$c_{i,j,k}$ even for $j>\ell_{i}$ although it never adds to them. The reason
we have the variables $c_{i,j,k}$ for $j>\ell_{i}$ is that this way, the
formulas from Proposition 4.2 are applicable.

Note that since each $V_{i}$ is a singleton, the automaton
$\mathcal{B}=\mathcal{A}\times\mathcal{A}_{1}\otimes\cdots\otimes\mathcal{A}_{m}$
is defined. It satisfies $L(\mathcal{B})=\llbracket S^{\prime}\rrbracket$,
where $S^{\prime}$ is the set of alternation constraints in $S$.

It remains to impose the remaining constraints from $S$, namely the binary
constraints and those of the form $x=w$ with $x\in U$, $w\in A^{*}$. Let
$R\subseteq S$ be the set of these remaining constraints. For each $i$ and for
$\mu\in(A^{*})^{V}$, let $w_{\mu,i}$ be the word in Eq. 12. According to
Proposition 4.2, for each constraint $r\in R$, we can construct a polynomial
size existential Presburger formula $\kappa_{r}$ such that
$\mu\models\kappa_{r}$ if and only if the constraint is satisfied for the
assignment $\alpha$ with $\alpha(x_{i})=w_{\mu,i}$. Moreover, let
$\kappa=\bigwedge_{r\in R}\kappa_{r}$.

Suppose $\mathcal{B}=(Q,A,C,E,q_{0},F)$. In the last step, we construct the
counter automaton $\mathcal{B}^{\prime}=(Q,A,C,E,q_{0},F^{\prime})$, where

$F^{\prime}=\\{(q,\psi\wedge\kappa)\mid(q,\psi)\in F\\}.$

Now $\mathcal{B}^{\prime}$ clearly satisfies
$L(\mathcal{B}^{\prime})=\llbracket T\cup S\rrbracket$. Thus, if we obtain
$\mathcal{B}^{\prime\prime}$ from $\mathcal{B}^{\prime}$ by projecting the
input to those variables that occur freely in $\varphi$, then
$L(\mathcal{B}^{\prime\prime})=\llbracket T\cup
S\rrbracket_{\mathsf{fv}(\varphi)}$. Moreover, $\mathcal{B}^{\prime\prime}$
can clearly be constructed in exponential time.

The membership of the truth problem in $\NEXP$ follows from the fact that
emptiness of counter automata is in $\NP$ (Lemma 4.9). ∎

##  5\. Expressiveness

In this section, we shed some light on which predicates or languages are
definable in our fragments $\Sigma_{i,j}$.

###  5.1. Expressiveness of the $\Sigma_{1,0}$ fragment

In the case of $\Sigma_{1,0}$, a definable language $L$ always satisfies
$L\subseteq(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$ for some $\ell\in\mathbb{N}$.
Hence, it can be described by the set of vectors that contain the occurring
exponents. As can be derived from results in Section 4, these sets are always
semilinear. In this section, we provide a decidable characterization of the
semilinear sets that are expressible in this way. Stating the characterization
requires some terminology.

Let $V$ be a set of variables. By $\mathbb{N}^{V}$, we denote the set of
mappings $V\to\mathbb{N}$. By a _partition of $V$_, we mean a set
$P=\\{V_{1},\ldots,V_{n}\\}$ of subsets $V_{1},\ldots,V_{n}\subseteq V$ such
that $V_{i}\cap V_{j}=\emptyset$ for $i\neq j$ and $V_{1}\cup\cdots\cup
V_{n}=V$. If $U\cap V=\emptyset$ and $\alpha\in\mathbb{N}^{U}$,
$\beta\in\mathbb{N}^{V}$, we write $\alpha\times\beta$ for the map
$\gamma\in\mathbb{N}^{U\cup V}$ such that $\gamma|_{U}=\alpha$ and
$\gamma|_{V}=\beta$. Furthermore, if $S\subseteq\mathbb{N}^{U}$,
$T\subseteq\mathbb{N}^{V}$, then $S\times T=\\{\alpha\times\beta\mid\alpha\in
S,~{}\beta\in T\\}$. A semilinear set $S\subseteq\mathbb{N}^{V}$ is _$P$
-compatible_ if it has a semilinear representation where each occurring period
vector belongs to $\mathbb{N}^{V_{i}}$ for some $i\in[1,n]$.

######  Theorem 5.1.

Suppose $L\subseteq(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$. Let $V=\\{x_{i,j}\mid
i\in[1,\ell],~{}j\in[1,n]\\}$ and consider the partition
$P=\\{V_{1},\ldots,V_{n}\\}$ where $V_{j}=\\{x_{i,j}\mid i\in[1,\ell]\\}$ for
$j\in[1,n]$. The language $L$ is definable in $\Sigma_{1,0}$ if and only if
the set

$S=\\{\alpha\in\mathbb{N}^{V}\mid a_{1}^{\alpha(x_{1,1})}\cdots
a_{n}^{\alpha(x_{1,n})}\cdots a_{1}^{\alpha(x_{\ell,1})}\cdots
a_{n}^{\alpha(x_{\ell,n})}\in L\\}$

is a $P$-compatible semilinear set.

For example, this means we can define $\\{a^{n}ba^{n}\mid n\in\mathbb{N}\\}$,
but not $\\{a^{n}b^{n}\mid n\in\mathbb{N}\\}$: A semilinear representation for
the latter requires a period that produces both $a$’s and $b$’s.

The proof of Theorem 5.1 employs a characterization of $P$-compatible sets in
terms of Presburger arithmetic. Let $V$ be a set of variables and $\varphi$ be
a Presburger formula whose variables are in $V$. Let
$P=\\{V_{1},\ldots,V_{n}\\}$ be a partition of $V$. We say $\varphi$ is _$P$
-compatible_ if there is a set of variables $V^{\prime}\supseteq V$ and a
partition $P^{\prime}=\\{V^{\prime}_{1},\ldots,V^{\prime}_{n}\\}$ of
$V^{\prime}$ such that

  1. (1)

$V_{j}\subseteq V^{\prime}_{j}$ for each $j\in[1,n]$ and

  2. (2)

in each literal in $\varphi$, all variables belong to the same set
$V^{\prime}_{j}$ for some $j\in[1,n]$.

The following is a simple observation.

######  Theorem 5.2.

Let $P=\\{V_{1},\ldots,V_{n}\\}$ be a partition of $V$. For sets
$S\subseteq\mathbb{N}^{V}$, the following conditions are equivalent:

  1. (1)

$S$ is a $P$-compatible semilinear set.

  2. (2)

$S=\llbracket\varphi\rrbracket$ for some $P$-compatible existential Presburger
formula $\varphi$.

  3. (3)

$S$ is a finite union of sets of the form $A_{1}\times\cdots\times A_{n}$
where each $A_{j}$ is a semilinear subset of $\mathbb{N}^{V_{j}}$.

###### Proof.

The directions “3$\Rightarrow$1” and “1$\Rightarrow$2” are easy to see, so we
show “2$\Rightarrow$3”.

If a set satisfies the condition of 3, then projecting to a subset of the
coordinates yields again a set of this form. Therefore, it suffices to
consider the case where in $\varphi$, there are no quantifiers. Now, bring
$\varphi$ into disjunctive normal form. Since each literal in $\varphi$ only
mentions variables from $V_{j}$ for some $j\in[1,n]$, we can sort the literals
of each co-clause of the DNF according to the subset $V_{j}$ they mention.
Hence, we arrive at the form

$\varphi\equiv\bigvee_{i=1}^{k}\bigwedge_{j=1}^{n}\varphi_{i,j},$

where $\varphi_{i,j}$ only mentions variables from $V_{j}$. This implies

$\llbracket\varphi\rrbracket=\bigcup_{i=1}^{k}\llbracket\varphi_{1,j}\rrbracket\times\cdots\times\llbracket\varphi_{n,j}\rrbracket,$

which is the form required in 3. ∎

We are now ready to prove Theorem 5.1.

###### Proof.

If $L$ is definable in $\Sigma_{1,0}$, we can write down a Presburger formula
that defines $S$. Here, in order to express the subword ordering (and its
negation), we use the formulas from Proposition 4.2. Observe that these
formulas are $P$-compatible. This means that $S$ is $P$-compatible.

For the converse, suppose $S$ is $P$-compatible. According to Theorem 5.21,
$S$ is defined by a $P$-compatible existential Presburger formula $\varphi$.
Hence, $\varphi$ has free variables $V=\\{x_{i,j}\mid
i\in[1,\ell],j\in[1,n]\\}$ and uses variables $V^{\prime}\supseteq V$ that are
partitioned as $V^{\prime}=\biguplus_{j=1}^{n}V^{\prime}_{j}$ so that in each
literal, all occurring variables belong to the same $V^{\prime}_{j}$.

In the first step, we turn $\varphi$ into a $\Sigma_{1,0}$ formula
$\bar{\varphi}$ with the same number of free variables. For each $x\in
V^{\prime}$, we take a fresh variable $\bar{x}$, which will hold words in
$a_{j}^{*}$. More precisely, we have our new variables $\bar{V}=\\{\bar{x}\mid
x\in V^{\prime}\\}$ and a mapping
$\iota\colon\mathbb{N}^{V^{\prime}}\to(A^{*})^{\bar{V}}$ defined by
$\iota(\alpha)(\bar{x})=a_{j}^{\alpha(x)}$, where $j$ is the unique index with
$x\in V^{\prime}_{j}$. We want to construct $\bar{\varphi}$ so that
$\llbracket\bar{\varphi}\rrbracket=\iota(\llbracket\varphi\rrbracket)$.

We obtain $\bar{\varphi}$ from $\varphi$ as follows. For each literal $x=y+z$,
we know that there is a $j\in[1,n]$ with $x,y,z\in V^{\prime}_{i}$, so we can
replace the literal with
$|\bar{x}|_{a_{j}}=|\bar{y}|_{a_{j}}+|\bar{z}|_{a_{j}}$, which is expressible
in $\Sigma_{1,0}$ according to Item 11 in the proof of Theorem 3.3 (note that
in this case, we actually are in $\Sigma_{1,0}$ because the variables
$\bar{x}$, $\bar{y}$, and $\bar{z}$ range over $a_{j}^{*}$ and are thus
alternation bounded). Since we can clearly also express
$|\bar{x}|_{a_{j}}\neq|\bar{y}|_{a_{j}}$ in $\Sigma_{1,0}$, we use this to
implement literals $x\neq y$ with $x,y\in V^{\prime}_{j}$. Literals of the
form $x=k$ with $k\in\mathbb{N}$ and $x\in V^{\prime}_{j}$ can just be
replaced by $\bar{x}=a_{j}^{k}$. Then we clearly have
$\llbracket\bar{\varphi}\rrbracket=\iota(\llbracket\varphi\rrbracket)$.

In the second step, we construct the words

$a_{1}^{\alpha(x_{1,1})}\cdots a_{n}^{\alpha(x_{1,n})}\cdots
a_{1}^{\alpha(x_{\ell,1})}\cdots a_{n}^{\alpha(x_{\ell,n})}$

for $\alpha\in\llbracket\varphi\rrbracket$. This is possible thanks to Item 13
of the proof of Theorem 3.3. We can express

$u=\bar{x}_{1,1}\cdots\bar{x}_{1,n}\cdots\bar{x}_{\ell,1}\cdots\bar{x}_{\ell,n}$

by applying Item 13 exactly $\ell\cdot n-1$ times, once to append each
$x_{i,j}$ to the word defined so far, using $\ell\cdot n-1$ additional
variables. Of course, all these variables can be restricted to
$(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, which means the resulting formula
belongs to $\Sigma_{1,0}$. Moreover, it clearly defines $L$. ∎

Our characterization of $\Sigma_{1,0}$ is decidable. We use a technique from
[14], where it is shown that recognizability is decidable for semilinear sets.
The idea is to characterize $P$-compatibility as the finiteness of the index
of certain equivalence relations, which can be expressed in Presburger
arithmetic.

######  Theorem 5.3.

Given a semilinear subset $S\subseteq\mathbb{N}^{V}$ and a partition $P$ of
$V$, it is decidable whether $S$ is $P$-compatible.

###### Proof.

For $\alpha\in\mathbb{N}^{V_{i}}$ and $\gamma\in\mathbb{N}^{V}$, we write
$\gamma[i/\alpha]$ to be the element of $\mathbb{N}^{V}$ with

$\gamma[i/\alpha](v)=\begin{cases}\alpha(v)&\text{if $v\in V_{i}$}\\\
\gamma(v)&\text{otherwise}\end{cases}$

For $\alpha,\beta\in\mathbb{N}^{V_{i}}$, we write $\alpha\sim_{i}\beta$ if for
every $\gamma\in\mathbb{N}^{V}$, we have $\gamma[i/\alpha]\in S$ if and only
if $\gamma[i/\beta]\in S$. Moreover, for $\gamma\in\mathbb{N}^{V}$, we will
use the norm $\|\cdot\|$ as defined by $\|\gamma\|=\sum_{v\in V}\gamma(v)$. We
claim that $S$ is $P$-compatible if and only if

$\exists
k\in\mathbb{N}\colon\bigwedge_{i=1}^{n}\forall\alpha\in\mathbb{N}^{V_{i}}\colon\exists\beta\in\mathbb{N}^{V_{i}}\colon\|\beta\|\leq
k,~{}\alpha\sim_{i}\beta.$ (13)

Suppose Eq. 13 holds. For each $\beta\in\mathbb{N}^{V_{i}}$, we define
$S_{i,\beta}=\\{\alpha\in\mathbb{N}^{V_{i}}\mid\alpha\sim_{i}\beta\\}$. Then
$S_{i,\beta}\subseteq\mathbb{N}^{V_{i}}$ is semilinear and we have

$S=\bigcup_{\beta_{1}\in\mathbb{N}^{V_{1}},\|\beta_{1}\|\leq
k}\cdots\bigcup_{\beta_{n}\in\mathbb{N}^{V_{n}},\|\beta_{n}\|\leq
k}S_{1,\beta_{1}}\times\cdots\times S_{n,\beta_{n}}.$

Hence, $S$ is $P$-compatible.

Now assume $S$ is $P$-compatible. Then we can write
$S=\bigcup_{j=1}^{\ell}A_{j,1}\times\cdots\times A_{j,n}$, where each
$A_{j,i}\subseteq\mathbb{N}^{V_{i}}$ is semilinear. For each $i\in[1,n]$,
consider the function $\kappa_{i}\colon\mathbb{N}^{V_{i}}\to
2^{\\{1,\ldots,\ell\\}}$ with

$\kappa_{i}(\alpha)=\\{j\in[1,\ell]\mid\alpha\in A_{j,i}\\}.$

Observe that if $\kappa_{i}(\alpha)=\kappa_{i}(\beta)$, then
$\alpha\sim_{i}\beta$. Since $\kappa_{i}$ has a finite codomain, this means
the equivalence relation $\sim_{i}$ on $\mathbb{N}^{V_{i}}$ has finite index.
This immediately implies Eq. 13.

Since we can clearly formulate the condition Eq. 13 in Presburger arithmetic,
$P$-compatibility is decidable. ∎

In fact, it is not hard to see that if $P$ consists only of singletons, a
semilinear set is $P$-compatible iff it is recognizable. Hence, Theorem 5.3
generalizes the decidability of recognizability. Let $M$ be a monoid. A subset
$S\subseteq M$ is called _recognizable_ if there is a finite monoid $F$ and a
morphism $\varphi\colon M\to F$ such that $S=\varphi^{-1}(\varphi(S))$.

######  Theorem 5.4.

Suppose $P$ consists only of singletons. Then $S\subseteq\mathbb{N}^{V}$ is
$P$-compatible if and only if it is recognizable.

###### Proof.

Mezei’s Theorem [4] states that if $M_{1},\ldots,M_{n}$ are monoids, then a
subset of $M_{1}\times\cdots\times M_{n}$ is recognizable if and only if it is
a finite union of sets $S_{1}\times\cdots\times S_{n}$ such that
$S_{i}\subseteq M_{i}$ is recognizable for $i\in\\{1,\ldots,n\\}$.

Combined with the fact that a subset of $\mathbb{N}$ is semilinear if and only
if it is recognizable, the condition 3 of Theorem 5.2 yields the result. ∎

###  5.2. Expressiveness of $\Sigma_{1,0}$ vs. $\Sigma_{1,1}$

When comparing $\Sigma_{1,0}$ and $\Sigma_{1,1}$, it is obvious that
$\Sigma_{1,1}$ is more expressive, because it permits the definition of
languages with unbounded alternations, such as $\\{a,b\\}^{*}$. But is this
the only difference between the two? In other words: Restricted to alternation
bounded languages, is $\Sigma_{1,1}$ more expressive?

######  Theorem 5.5.

If $L\subseteq(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, then $L$ is definable in
$\Sigma_{1,1}$ if and only if it is definable in $\Sigma_{1,0}$.

This is because, given a $\Sigma_{1,1}$ formula $\varphi$ where the free
variable is alternation bounded, Lemma 4.4 yields a (polynomial) bound $\ell$
so that if we replace every quantification $\exists x$ by $\exists
x\in(a_{1}^{*}\cdots a_{n}^{*})^{\ell}$, the resulting $\Sigma_{1,0}$ formula
is equivalent.

This allows us to reason beyond alternation bounded languages. We have seen in
the proof of Theorem 3.3 that one can express “$|u|_{a}=|v|_{b}$” in
$\Sigma_{1,3}$, which required significantly more steps, and two more
alternation unbounded variables, than the ostensibly similar
“$|u|_{a}=|v|_{a}$”. This raises the question: Can we define the former in
$\Sigma^{\prime}_{1,1}$? We cannot:

######  Corollary 5.6.

In $\Sigma_{1,1}$, we cannot express “$|u|_{a}=|u|_{b}$”.

###### Proof.

Otherwise, we could define the set $\\{a^{n}b^{n}\mid n\geq 0\\}$ in
$\Sigma_{1,1}$, hence in $\Sigma_{1,0}$, contradicting Theorem 5.1. ∎

###  5.3. Expressiveness of $\Sigma_{1,2}$ vs. $\Sigma_{1,3}$

We have seen in Theorem 3.3 that $\Sigma_{1,3}$ can express all recursively
enumerable unary languages. Moreover, Theorem 4.6 tells us that the languages
definable in $\Sigma_{1,2}$ are always counter languages.

How do the fragments compare with respect to natural (binary) predicates on
words. We already know from Item 14 in Theorem 3.3 that over two letters, the
prefix relation is expressible in $\Sigma_{1,3}$. Note that the following
Theorem does not follow directly from the fact that for any $\Sigma_{1,2}$
formula $\varphi$, the set $\llbracket\varphi\rrbracket$ is a counter
relation, as shown in Section 4. This is because the prefix relation is a
counter relation (and even rational).

######  Theorem 5.7.

In $\Sigma_{1,2}$, “$u$ is a prefix of $v$” is not expressible.

###### Proof.

Suppose the prefix relation were expressible using a $\Sigma_{1,2}$ formula
$\varphi$. Then, by reversing all constants in $\varphi$, we obtain a formula
expressing the suffix relation. Let $\sqsubseteq_{\mathsf{p}}$ denote the
prefix relation and $\sqsubseteq_{\mathsf{s}}$ the suffix relation. We can now
express

$\exists v\in\\{a,b\\}^{*}\colon v\sqsubseteq_{\mathsf{p}}u\wedge
v\sqsubseteq_{\mathsf{s}}u\wedge|u|_{a}=2\cdot|v|_{a}\wedge|u|_{b}=2\cdot|v|_{b},$

which is equivalent to $u\in S$, where $S=\\{vv\mid v\in\\{a,b\\}^{*}\\}$.
Note that $|u|_{a}=2\cdot|v|_{a}$ can be expressed by using
$|u|_{a}=|v|_{a}+\cdot|v|_{a}$, which can be done in $\Sigma^{\prime}_{1,0}$
according to Item 11 in Theorem 3.3.

However, $S$ is not a counter language. This is due to the fact that the class
of recursively enumerable languages is the smallest language class that
contains $S$, is closed under rational transductions, union, and intersection
(this can be shown as in the case of the set of palindromes [3]). However, the
class of counter languages also has these closure properties and is properly
contained in the recursively enumerable languages. Hence, $S$ is indeed not a
counter language. This is in contradiction with the fact that for any
$\Sigma_{1,2}$ formula $\varphi$, the set $\llbracket\varphi\rrbracket$ is a
counter relation, as shown in Section 4. ∎

##  6\. Conclusion

We have shown that the $\Sigma_{1}$ theory of the subword ordering is
undecidable (already for two letters), if all words are available as
constants. This implies that the $\Sigma_{2}$ theory is undecidable already
for two letters, even without constants.

In order to shed light on decidable fragments of first-order logic over the
structure $({A}^{*},\mathord{\sqsubseteq},w_{1},\mathord{\ldots})$, we
introduced the fragments $\Sigma_{i,j}$. We have completely settled their
decidability status. In terms of complexity, the only open case is the
$\Sigma_{1,2}$ fragment. We have an $\NP$ lower bound and an $\NEXP$ upper
bound.

This aligns with the situation for expressiveness. We have a decidable
characterization for the expressiveness of $\Sigma_{1,0}$ and, obvious
exceptions aside, $\Sigma_{1,1}$ is as expressive as $\Sigma_{1,0}$. However,
we do not know whether $\Sigma_{1,1}$ and $\Sigma_{1,2}$ differ significantly:
Of course, $\Sigma_{1,2}$ can have two alternation unbounded free variables,
but it is conceivable that $\Sigma_{1,1}$ and $\Sigma_{1,2}$ define the same
languages.

## References

  * [1] P. A. Abdulla et al.  “String Constraints for Verification”  In _Proc. CAV 2014, LNCS 8559_ Springer, 2014, pp. 150–166  DOI: http://dx.doi.org/10.1007/978-3-319-08867-9˙10
  * [2] P. A. Abdulla, A. Collomb-Annichini, A. Bouajjani and B. Jonsson  “Using Forward Reachability Analysis for Verification of Lossy Channel Systems”  In _Form. Methods Sys. Des._ 25.1, 2004, pp. 39–65  DOI: http://dx.doi.org/10.1023/B:FORM.0000033962.51898.1a
  * [3] Brenda S. Baker and Ronald V. Book  “Reversal-bounded multipushdown machines”  In _J. Comput. System Sci._ 8.3, 1974, pp. 315–332
  * [4] J. Berstel  “Transductions and Context-Free Languages”  Stuttgart: B. G. Teubner, 1979  DOI: http://dx.doi.org/10.1007/978-3-663-09367-1˙2
  * [5] P. Bouyer et al.  “On Termination and Invariance for Faulty Channel Machines”  In _Form. Asp. Comp._ 24.4–6, 2012, pp. 595–607  DOI: http://dx.doi.org/10.1007/s00165-012-0234-7
  * [6] J. R. Büchi and S. Senger  “Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory”  In _Z. Math. Logik Grundlag. Math._ 34.4, 1988, pp. 337–342  DOI: http://dx.doi.org/10.1002/malq.19880340410
  * [7] Michaël Cadilhac, Alain Finkel and Pierre McKenzie  “Affine Parikh automata”  In _RAIRO Theor. Inf. Appl._ 46.4, 2012, pp. 511–545  DOI: http://dx.doi.org/10.1051/ita/2012013
  * [8] H. Comon and R. Treinen  “Ordering Constraints on Trees”  In _Proc. CAAP ’94, LNCS 787_ Springer, 1994, pp. 1–14  DOI: http://dx.doi.org/10.1007/BFb0017470
  * [9] V. Diekert  “Makanin’s Algorithm”  In _Algebraic Combinatorics on Words_ 90, Encyclopedia of Mathematics and Its Applications  Cambridge Univ. Press, 2002, pp. 387–442
  * [10] V. Diekert, P. Gastin and M. Kufleitner  “A Survey on Small Fragments of First-Order Logic over Finite Words”  In _Int. J. Found. Comput. Sci._ 19.3, 2008, pp. 513–548  DOI: http://dx.doi.org/10.1142/S0129054108005802
  * [11] Valery G. Durnev  “Undecidability of the positive $\forall\exists^{3}$-theory of a free semigroup”  In _Sib. Math. J._ 36.5 Springer, 1995, pp. 917–929  DOI: http://dx.doi.org/10.1007/BF02112533
  * [12] J. Ferrante and C. W. Rackoff  “The computational complexity of logical theories” 718, Lecture Notes in Mathematics  Springer, 1979  DOI: http://dx.doi.org/10.1007/BFb0062837
  * [13] V. Ganesh, M. Minnes, A. Solar-Lezama and M. C. Rinard  “Word Equations with Length Constraints: What’s Decidable?”  In _Proc. HVC 2012, LNCS 7857_ Springer, 2013, pp. 209–226  DOI: http://dx.doi.org/10.1007/978-3-642-39611-3˙21
  * [14] Seymour Ginsburg and Edwin H. Spanier  “Bounded Regular Sets”  In _Proc. Amer. Math. Soc._ 17.5, 1966, pp. 1043–1049  DOI: http://dx.doi.org/10.2307/2036087
  * [15] G. Gottlob, N. Leone and H. Veith  “Second Order Logic and the Weak Exponential Hierarchies”  In _Proc. MFCS ’95, LNCS 969_ Springer, 1995, pp. 66–81  DOI: http://dx.doi.org/10.1007/3-540-60246-1˙113
  * [16] Ch. Haase, S. Schmitz and Ph. Schnoebelen  “The Power of Priority Channel Systems”  In _Log. Methods Comput. Sci._ 10.4:4, 2014  DOI: http://dx.doi.org/10.2168/LMCS-10(4:4)2014
  * [17] Christoph Haase  “Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy”  In _Proc. CSL-LICS 2014_ ACM, 2014, pp. 47:1–47:10  DOI: http://dx.doi.org/10.1145/2603088.2603092
  * [18] L. Hemachandra  “The strong exponential hierarchy collapses”  In _J. Comput. System Sci._ 39.3, 1989, pp. 299–322  DOI: http://dx.doi.org/10.1016/0022-0000(89)90025-1
  * [19] P. Hooimeijer and W. Weimer  “StrSolve: solving string constraints lazily”  In _Autom. Softw. Eng._ 19.4, 2012, pp. 531–559  DOI: http://dx.doi.org/10.1007/s10515-012-0111-x
  * [20] Oscar H. Ibarra  “Reversal-bounded multicounter machines and their decision problems”  In _Journal of the ACM_ 25.1 ACM, 1978, pp. 116–133  DOI: 10.1145/322047.322058
  * [21] P. Karandikar, M. Niewerth and Ph. Schnoebelen  “On the state complexity of closures and interiors of regular languages with subwords and superwords”  In _Theoret. Comput. Sci._ 610, 2016, pp. 91–107  DOI: http://dx.doi.org/10.1016/j.tcs.2015.09.028
  * [22] P. Karandikar and Ph. Schnoebelen  “Decidability in the Logic of Subsequences and Supersequences”  In _Proc. FST &TCS 2015, LIPIcs 45_ Leibniz-Zentrum für Informatik, 2015, pp. 84–97  DOI: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.84
  * [23] P. Karandikar and Ph. Schnoebelen  “Generalized Post Embedding Problems”  In _Theory of Computing Systems_ 56.4, 2015, pp. 697–716  DOI: http://dx.doi.org/10.1007/s00224-014-9561-9
  * [24] P. Karandikar and Ph. Schnoebelen  “The height of piecewise-testable languages with applications in logical complexity”  In _Proc. CSL 2016, LIPIcs 62_ Leibniz-Zentrum für Informatik, 2016, pp. 37:1–37:22  DOI: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.37
  * [25] Felix Klaedtke and Harald Rueß  “Monadic Second-Order Logics with Cardinalities”  In _Proc. ICALP 2003, LNCS 2719_ Springer, 2003, pp. 681–696  DOI: http://dx.doi.org/10.1007/3-540-45061-0˙54
  * [26] O. Klíma and L. Polák  “Alternative Automata Characterization of Piecewise Testable Languages”  In _Proc. DLT 2013, LNCS 7907_ Springer, 2013, pp. 289–300  DOI: http://dx.doi.org/10.1007/978-3-642-38771-5˙26
  * [27] Dexter C. Kozen  “Lower bounds for natural proof systems”  In _Proc. FOCS ’77_ IEEE, 1977, pp. 254–266  DOI: http://dx.doi.org/10.1109/SFCS.1977.16
  * [28] O. V. Kudinov, V. L. Selivanov and L. V. Yartseva  “Definability in the Subword Order”  In _Proc. CiE 2010, LNCS 6158_ Springer, 2010, pp. 246–255  DOI: http://dx.doi.org/10.1007/978-3-642-13962-8˙28
  * [29] D. Kuske  “Theories of orders on the set of words”  In _RAIRO Theor. Inf. Appl._ 40.1, 2006, pp. 53–74  DOI: http://dx.doi.org/10.1051/ita:2005039
  * [30] Yuri V. Matiyasevich  “Hilbert’s Tenth Problem”  Cambridge, Massachusetts: MIT Press, 1993
  * [31] Derek C. Oppen  “A $2^{2^{2^{pn}}}$ upper bound on the complexity of Presburger Arithmetic”  In _J. Comput. System Sci._ 16.3, 1978, pp. 323–332
  * [32] W. Plandowski  “Satisfiability of word equations with constants is in PSPACE”  In _J. ACM_ 51.3, 2004, pp. 483–496  DOI: http://dx.doi.org/10.1145/990308.990312
  * [33] W. V. Quine  “Concatenation as a basis for arithmetic”  In _J. Symb. Logic_ 11.4, 1946, pp. 105–114  DOI: http://dx.doi.org/10.2307/2268308
  * [34] Larry Joseph Stockmeyer  “The complexity of decision problems in automata theory and logic” Available as Report MAC-TR-133, 1974
  * [35] Kumar Neeraj Verma, Helmut Seidl and Thomas Schwentick  “On the Complexity of Equational Horn Clauses”  In _Proc. CADE 2005, LNCS 3632_ Springer, 2005, pp. 337–352