Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering
Simon Halfon Philippe Schnoebelen Georg Zetzsche



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






halfon@lsv.fr



phs@lsv.fr



The third author is supported by a fellowship within the
Postdoc-Program of the German Academic Exchange Service (DAAD) and by Labex
DigiCosme, Univ. Paris-Saclay, project VERICONISS
zetzsche@lsv.fr



[
    Georg Zetzsche
    December 30, 2023
=====================





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 Σ_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 Σ_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 Σ_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.















§ INTRODUCTION





A subsequence of a (finite) sequence u is a
sequence obtained from u by removing any number of elements. For
example, if u=(, , , , ) then u'=(, 
,) is a subsequence of u, a fact we denote with u'
u. Other examples that work for any u are u u (remove
nothing) and () 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 <cit.>.
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 <cit.>.







 §.§ The logic of subwords


In this paper we consider the first-order logic (A^*,) of
words over some alphabet A={,,,…} equipped with the subword relation .
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
@true 
    *ϕ_1:∀ u,u',u”:
     u u' u' u” u u” ,
    
    *ϕ_2:∃ u:  u
     u
    u
     ,
    
    *ϕ_3:∀ u, v: ∃ s:
    ([                             u s v s;                   ∀ t: u t v t  s t ])
     .


Here φ_1 states that the subword relation is transitive
(which it is).

More interesting is φ_2, stating that it is possible that
a word contains both  and  as
subwords but not . 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, φ_3, states that words ordered by
subwords are an upper semilattice. This is a more complex formula with
Π_3 quantifier alternation. It is not valid in general (e.g.,
 and  have no lub) but this depends on the
alphabet A at hand: φ_3 holds if A is a singleton alphabet, i.e.,
{}^*φ_3 but {,}^*φ_3.

We say that formulas like φ_1 or φ_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
while the extended logic is over the expansion
A where there is a constant
symbol w_i for every word in A^*.

As we just illustrated with φ_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 u is a letter, i.e., is a word of length 1,
in the pure fragment:

    ∃ z:∀ x: z x
    
    (x u(u x x z))
     .

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
formulas and about algorithms for computing their solutions. By comparison, it
is well known that the Σ_2-theory of (A^*,·), the
logic of strings with concatenation, is
undecidable <cit.>,  and that its
Σ_1 fragment (aka “word equations”) is decidable in
 <cit.>. Moreover, introducing counting
predicates leads to an undecidable Σ_1 fragment <cit.>.


Regarding the logic of subwords,  Comon and
Treinen showed undecidability for an extended logic
(A^*,,p_) where A={,,} has three
letters and p_ is a unary function that prepends 
in front of a word, hence is a restricted form of
concatenation <cit.>.  Kuske showed that, when only
the subword predicate is allowed, the logic A is
undecidable and already its Σ_3 fragment is undecidable when
|A|≥ 2.  Kudinov et al. considered definability in
A and showed that the predicates definable in
A are exactly the arithmetical
predicates[Those
that are invariant under the automorphisms of the
structure] <cit.>.

Kuske's result on the Σ_3 theory leaves open the question
whether smaller fragments are decidable. Karandikar and Schnoebelen
showed that the Σ_2 theory is undecidable <cit.> and
this is tight since the Σ_1 fragment is decidable, in fact
-complete <cit.>. 

Karandikar and Schnoebelen
also showed that the two-variable fragment ^2(A^*,) is
decidable <cit.> and that it has an elementary complexity
upper bound <cit.>. Decidability extends to
the logic ^2(A^*,,R_1,R_2,…) 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 Σ_1 fragment but beyond
deciding validity, we are interested in computing sets of solutions: a
formula like φ_2 can be seen as a conjunctive set of
constraints, “x 
x 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
Σ_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 φ_1 but not like φ_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,[This is a common situation,
shared with, e.g., (A^*,·) and (,<).]
see <cit.>. However this requires
some universal quantification (even when defining the empty word)  that are not allowed when restricting to the
Σ_1 fragment. So this avenue is closed.



In
particular, it allows expressing bounded quantification. For example,
we usually write bounded quantifications like

    ∀ u∈^+^*: ⋯

instead of the equivalent

    ∀ u:
    ab u bbucbubau⋯

We note that any unary predicate u∈ L for L a piecewise testable
language (or a “PT language”, see definition in
Section <ref>) can be expressed as above by requiring and
forbidding some constant subwords. As a consequence, we shall freely
use membership in piecewise testable languages as abbreviations.





 §.§ Summary of results



Our first result is that, when constants are allowed, the
Σ_1 fragment of A is actually
undecidable. 

In fact the Σ_1 fragment of [W]A, where a single
constant W∈ A^* can be named, is undecidable unless W is too
simple.

These results hold as soon as A contains two distinct letters
and exhibit 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 Σ_1 constraints.




Our second result identifies a key factor influencing decidability: it
turns out that free variables ranging over a  “thin”
language like L=^+^*, are easier to handle than
variables ranging over a “wide”



language like L'=(+)^*.  The key difference is that a thin language
only allows a bounded number of letter changes (in L we have 's, then
's, then 's) while a wide language contains words with arbitrarily
many alternations between distinct letters.

These observations lead to a new descriptive complexity measure for
the formulas in A. The associated fragments, denoted ij
for i,j∈, consist of all Σ_i formulas where j variables, say
x_1,x_2,…,x_j can be used without any restrictions, while all the other
variables must be restricted with respect to letter alternations, say using
x∈ (^*_1^*_2⋯^*_n)^ℓ for some ℓ∈ and assuming that
_1,…,_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 12 fragment is decidable
while 13 is undecidable even for |A|=2.  The
20 fragment is decidable while 21 is not.  In
fact, when all variables are alternation bounded, the entire
first-order theory is decidable.






The computational complexity of all mentioned fragments is summarized
in <ref>. Note that, in this table, n denotes the
n-th level of the weak  hierarchy, which lies between  and
 <cit.>.





Finally, we offer a series of expressiveness results showing how various
predicates like concatenation or length function can, or cannot, be defined in
the ij fragments.  As demonstrated in the paper, expressiveness
results are crucial to obtain hardness results.  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 ^2(A^*,).  Because undecidability
appears so easily when reasoning about words, the focus is often on
restricted fragments, typically Σ_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., <cit.>.






 §.§ Outline of the paper


We provide in <Ref> the basic definitions and results
necessary for our later developments.  Then we show the undecidability of
the Σ_1 fragment 
(<Ref>) before focusing on the decidable fragments
(<Ref>). Finally, in <Ref>, we turn to
expressiveness questions. 
















§ SUBWORDS AND THEIR LOGICS





We consider finite words ,,... over a
given finite alphabet A of letters like ,,….
Concatenation of words is written multiplicatively, with the
empty word ϵ as unit.  We freely use regular expressions like
()^*+()^* to denote regular languages.

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

A word  is a factor of  if there exist words _1 and
_2 such that = _1 _2.  If furthermore _1=ϵ then
 is a prefix of ,
while if _2=ϵ then  is a suffix.





 §.§ Subwords.





We say that a word  is a subword (i.e., a subsequence) of
, written , when  is some _1⋯_n and 
can be written as _0 _1 _1 ⋯_n _n for some
_0,_1,…,_n∈ A^*, e.g., ϵ.
We write  for the
associated strict ordering, where ≠. Two words  and  are
incomparable (with respect to the subword relation), denoted ⊥, if  and .
Factors are a special case of subwords.

With any ∈ A^* we associate its upward closure , given by
{∈ A^*  | }.  For example,
ab=A^* A^* A^*. The definition of  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 <cit.>.

Among the several characterizations of PT languages, the most
convenient for our purposes is the following one: L⊆ A^* is
PT if, and only if, it is a boolean combination of languages of the
form  for some ∈ A^*. Thus the PT languages are exactly
the monadic predicates that can be defined by a boolean combination of
constraints of the form _i x and/or _jx, or
equivalently by a quantifier-free φ_L(x) formula in the
A logic. For example, the solutions of ϕ_2 (from
the introduction) form a PT language. 
In the following, we often write “x∈ L”, where L is a given PT
language, as an abbreviation for ϕ_L(x), with the understanding
that this is a Σ_0 formula.






 §.§ Logic of subwords





Let V be the set of variables with typical elements 
x,y,…,u,v,…. 
 For a
first-order logic formula φ over a structure with domain D, we denote
by φ⊆ D^V the set of satisfying
assignments, with typical elements α,β,….
If φ has only one free variable, say x, and there is no danger of
confusion, we sometimes write φ to mean {α(x) |α∈φ}.
Moreover, φ denotes the set of free variables in φ.

By A, we denote the first-order logic over the structure
A. In contrast, A is the first-order logic over the
structure A, where for each word ∈ A^*, the signature
provides a constant symbol. In the case of A and A,
assignments are members of (A^*)^V. We will sometimes write  to denote the
assignment that maps every variable to the word ∈ A^*.  Moreover,
(x↦) denotes the assignment in (A^*)^{x} that maps x to .






 §.§ Bounding alternations


We define a fragment of first-order logic over the relational structure A. Let A={_1,…,_n}.  The starting point for
introducing the fragments ij is the observation that if
every variable in a sentence φ is introduced by a restricted quantifier
of the form ∃ x∈(_1^*⋯_n^*)^ℓ or ∀
x∈(_1^*⋯_n^*)^ℓ for
some ℓ∈, then one can reduce the truth problem 
of φ to Presburger arithmetic. Note that the language (_1^*⋯_n^*)^ℓ is PT, implying that such restrictions, which we
call alternation bounds, can be imposed within A
and without any additional quantifiers. This raises
the question of how many variables without alternation bound one can allow
without losing decidability. 

In essence ij contains all formulas in the Σ_i
fragment with j
variables without alternation bound. A formalization of this for sentences
could just be a syntactic restriction: Every quantifier for all but at most j
variables must be relative to some (_1^*⋯_n^*)^ℓ. However, this
would not restrict free variables, which we need in order to build complex ij
formulas from predicates defined in ij.

Formally, a formula with alternation
bounds consists of a formula φ of A and a function
ℓ V→∪{∞}, which specifies the alternation bounds. This
means, the semantics (φ,ℓ) of (φ,ℓ) is
defined as φ̃, where φ̃ is defined
as follows.  First, we replace every quantifier 𝒬x
(𝒬∈{∃,∀}) in φ by the relativized 𝒬x∈ (_1^*⋯_n^*)^ℓ(x). Then we add the conjunction 
⋀_x∈φ, ℓ(x)<∞ x∈ (_1^*⋯_n^*)^ℓ(x) for the free variables.

The fragment ij consists of those formulas with alternation bounds
(φ,ℓ) where φ belongs to the Σ_i fragment of
A and has at most j variables x∈ V with ℓ(x)=∞.
We will always represent a formula in ij by its Σ_i formula
and the function ℓ will be clear from the context.
Variables x∈ V with ℓ(x)<∞ will be called alternation bounded,
the others alternation unbounded.
In order to permit a polynomial translation into an equivalent formula in
ordinary A, the alternation bounds are always encoded in unary.
The fragment ij is defined similarly, with Π_i instead of Σ_i.


Sometimes we define predicates that are satisfied for words with unbounded
alternations (such as “u∈{,}^*” when A={,,}), but want to use
the corresponding formula in a context where the variables are alternation
bounded (“u∈{,}^* ∧u”). In that situation, we
want to record the number of alternation unbounded variables we need for the
definition, disregarding the free variables. Hence, ij
denotes those formulas with alternation bound in Σ_i, where there are at
most j quantified variables without alternation bound.  The semantics
is defined as for ij.  The fragment ij is defined with
Π_i instead of Σ_i.

























§ UNDECIDABILITY




 §.§ The 13 fragment

We begin with our main result, the undecidability of the Σ_1 theory of
A for |A|≥ 2. In fact, we will even prove undecidability for
the 13 fragment.  We need a few ingredients. A word ∈ A^+ is
called primitive if there is no ∈ A^+, ||<||, with ∈^*.
The following is a well-known basic fact from word combinatorics (see e.g.
<cit.>)


If ∈ A^+ is primitive, then = is equivalent to ∈^*.


We also use the following version of the fact that Diophantine sets
are precisely the recursively enumerable sets <cit.>.

Let S⊆ be a recursively enumerable set. Then there is a finite set
of variables  {x_0,…,x_m} and a finite set E of equations, each of
the form

    x_i=x_j+x_k        x_i=x_j· x_k        x_i=1

with i,j,k∈ [0,m], such that 

    S={y_0 ∈|∃ y_1,…,y_m∈(y_0,…,y_m) satisfies E}.
 


We are now ready to prove our main result.


Let |A|≥ 2 and a∈ A. For each recursively enumerable set
S⊆, there is a 13 formula φ over the structure
A with one free variable such that φ={a^k
| k∈ S}. 





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.  Here, we always use u,v,w as the free variables of the formula we
currently construct.

Recall that for every PT language L⊆ A^*, we can express “u∈
L” in 00: we will use this silently, mainly for
languages of the form r a^* s where a is a letter and r,s are
two words.[That any language of the form ra^*s is PT is
easy to prove, e.g., using the characterization of <cit.>.]
Note also that, since “u∈(a+b)^*” can be expressed in 00 for a,b∈ A,
it suffices to prove the theorem in the case |A|=2.

  

  * We can express “|u|_a<|v|_a” in 10:
  
    ∃ x∈ a^* x v ∧ xu.

  

  * We can express “∃ n u=a^n ∧ v=a^n-1b” in 10.
  Clearly, it suffices to show that we can express
  “∃ n≥ 2 u=a^n ∧ v=a^n-1b”.
  Consider the formula:
  
    u∈ a a a^* ∧ v∈ a^*b∧∃ x∈ a^*b a a
       |v|_a<|u|_a ∧ vx ∧ u x.

  Suppose the formula is satisfied with u=a^n, x=a^ℓ b a a and v=a^m b.
  Then |v|_a<|u|_a implies m<n. By vx, we have ℓ<m and
  thus ℓ<m<n, hence ℓ+2≤ n.  On the other hand, u x implies
  n≤ℓ+2 and thus n=ℓ+2 and m=n-1.

  Conversely, if u=a^n and v=a^n-1b for some n≥ 2, then the formula is satisfied with
  x=a^n-2b a a.



  *  We can express “u,v∈ (a+b)^*b ∧ |u|_a=|v|_a” in 10:
  
    u,v∈ (a+b)^* 
     ∧ ∃ x ∈ a^*∃ y ∈ a^*b [ ∃ n x=a^n ∧ y=a^n-1b ] 
     ∧ 
       y u ∧  y v  ∧  xu ∧  xv.

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

  If u,v∈{a,b}^*b with |u|_a=|v|_a, then the formula is satisfied with n=|u|_a+1.
  

  * We can express “∃ n u=aaba^nb ∧ v=aba^n+1b∧ w=ba^n+2b” in 10:
  
    u∈ aaba^*b ∧ v∈ aba^*b∧ w∈ ba^*b 
     ∧ [u,v,w∈{a,b}^*b ∧ |u|_a=|v|_a=|w|_a].


  *  We can express “∃ n u=ba^nb∧ v=ba^n+1b” in 10. It suffices to show that we can
express “∃ n≥ 1 u=ba^nb∧ v=ba^n+1b”. Consider the formula:


    ∃ x ∈ aaba^*b, y ∈ aba^*b, z∈ ba^*b 
    [ ∃ m x=aaba^mb ∧ y=aba^m+1b ∧ z=ba^m+2b ] 
     ∧  u,v∈ ba^*b  ∧  u y  ∧  ux  ∧  v z ∧  vy.

Suppose the formula is satisfied for u=b a^kb and v=b a^ℓ b. Then
u y and ux imply k≤ m+1 and k>m, hence k=m+1.
Moreover, v z and vy imply ℓ≤ m+2 and
ℓ>m+1, hence ℓ=m+2. Hence, with n=m+1 we have u=b a^nb and
v=b a^n+1b and n≥ 1.

Conversely, if u=b a^nb and v=b a^n+1b for some  n≥ 1, then the formula is satisfied with m=n-1.


  *  We can express “∃ n u=a^n ∧ v=a^n+1” in 10. For this, it suffices to
express “∃ n≥ 1 u=a^n ∧ v=a^n+1”.
As in <ref>, one verifies correctness of the following:

    ∃ x,y,z[ ∃ m x=b a^mb ∧ y=b a^m+1b ∧ z=b a^m+2b ] 
    ∧ u,v∈ a^* ∧  u y ∧  ux  ∧  v z  ∧  vy.












  * We can express “v=a^|u|_a” in 10:
  
    ∃ x ∈ a^*[ ∃ n v=a^n ∧ x=a^n+1]
      ∧ v u ∧ xu.

  

  *  We can express “|u|_a=|v|_a” in 10:
  
    ∃ x x=a^|u|_a∧ x=a^|v|_a.

  

  *  For a b, we can express “u∈ a^* ∧ v=bu” in 10:
  
    u∈ a^* ∧ v∈ b a^* ∧ |v|_a=|u|_a.

  

  *  For a b, we can express “u∈ a^* ∧ v=ub” in 10:
  
    u∈ a^* ∧ v∈ a^*b ∧ |v|_a=|u|_a.

  

  *  We can express “|w|_a=|u|_a+|v|_a” for any a∈ A in 10.
Let b∈ A∖{a}:

    ∃ x,y∈ a^*∃ z∈ a^*b a^* x=a^|u|_a∧ y=a^|v|_a
    ∧ xb z ∧ xab z ∧ by z∧ byaz 
    ∧ |w|_a=|z|_a

Note that we can define xb, (xa)b and b(ya) thanks to <ref>.


The constraints in <ref> enforce that z=xby and hence |z|_a=|x|_a+|y|_a=|u|_a+|v|_a.




  * For k,n_0,…,n_k∈, a b, 
let r_a(a^n_0b a^n_1⋯
b a^n_k)=n_k, which defines a function r_a{a,b}^*→.
We can express “v=a^r_a(u)” in 10:

    v∈ a^* ∧ ∃ x∈ b^*a^* ∃ y∈ b^*a^* 
    
    |x|_b=|y|_b=|u|_b  ∧  |y|_a=|x|_a+1 
    ∧ x u ∧  yu ∧  |v|_a=|x|_a.

Note that |x|_b=|y|_b=|u|_b can be expressed according to
<ref> and |y|_a=|x|_a+1 can be expressed thanks to
<ref>.
Write u=a^n_0b a^n_1⋯ b a^n_k.

Suppose the formula is satisfied. Then |x|_b=|y|_b=|u|_b and |y|_a=|x|_a+1
imply that x=b^ka^m and y=b^ka^m+1 for some m∈. Moreover,
x u implies m≤ n_k and yu 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^ka^n_k and y=b^ka^n_k+1.



  *  For a∈ A, we can express “v∈ a^* ∧ w=uv” in 10. Let b a and consider the formula

    v∈ a^* ∧
    ∧     ∃ x∈ a^* ∃ y ∈ a^*   x=r_a(u)  ∧  y=r_a(w) 
    ∧      |w|_b=|u|_b ∧  u w
    ∧      |y|_a=|x|_a+|v|_a  ∧  |w|_a=|u|_a+|v|_a



To show correctness, suppose the formula is satisfied with 
u=a^n_0b a^n_1⋯ b a^n_k and w=a^m_0b a^m_1⋯ b a^m_ℓ.
The conditions in <ref>
imply that k=ℓ and w=a^m_0b a^m_1⋯ b a^m_k and n_i≤ m_i for i∈[0,k].
The conditions in <ref> then entail m_k=n_k+|v|_a and
∑_i=0^k m_i=∑_i=0^k n_i+|v|_a, which together is only possible if
m_i=n_i for i∈[0,k-1]. This means we have w=uv.
The converse is clear. 


  *  We can express “u is prefix of v” in 13:

    ⋀_a∈ A∃ x∃ y∈ a^* x=uy  ∧  x v  ∧  |x|_a=|v|_a.

Suppose the formula is satisfied. Then uy v for some y∈ A^*,
which implies u v.  Let p be the shortest prefix of v with
u p. Observe that whenever uw v, we also have pw
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∈ A with |p|_a>|u|_a. The formula
tells us that for some m∈, we have ua^m v and |u|_a+m=|v|_a.
Our observation yields pa^m v, and hence
|v|_a ≥ |p|_a + m > |u|_a+ m = |v|_a, a contradiction. The converse is clear.


  *  We can express “w=uv” in 13: Since expressibility is
preserved by mirroring, we can express prefix and suffix by
<ref>. Let  and  denote the prefix and suffix
relation, respectively. We can use the formula

    u w  ∧  v w  ∧ ⋀_a∈ A |w|_a=|u|_a+|v|_a.



  * For a,b∈ A, a b, we can express “u∈ (a b)^*” in
13: By <ref>, we can use the formula
∃ v v=uab ∧ v=abu,
which, according to <ref>, is equivalent to u∈ (a b)^*.







  * For a,b∈ A, a b, we can express “|u|_a=|v|_b” in 13 by using 
 
    ∃ x∈ (a b)^* |u|_a=|x|_a ∧ |v|_b=|x|_b.


 
  

  *  We can express “∃ m,n u=a^n ∧ v=a^m ∧ w=a^m· n” in 13:
  
    u,v,w∈ a^* 
     ∧ ∃ x  [∃ y,z  y=bu  ∧  z=yx  ∧  z=xy] 
     ∧  |x|_b = |v|_a  ∧  |w|_a=|x|_a.

The conditions in brackets require (bu)x=x(bu). Since bu∈ ba^*
is primitive, this is equivalent to x∈ (bu)^* (cf <ref>).









  * We use the fact that every recursively enumerable set of natural numbers
is Diophantine.  Applying <ref> to S yields a finite set E of
equations over the variables {x_0,…,x_m}.  The formula φ is of
the form

    φ≡∃ x_1, x_2, …, x_m ∈ a^*ψ,

where ψ is a conjunction of the following 13 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· x_k, we add a formula expressing x_i=a^|x_j|·|x_k|.
Then we clearly have φ={a^k | k∈ S}.



As an immediate consequence, one sees that the truth problem is also
undecidable for the Σ_1 fragment of the logic of subwords
without constants but enriched with predicates like “|u|_a=2” for
counting letter occurrences.

It can even be shown that there is a fixed word W∈{a,b}^* such
that the truth problem of 13 over [W]{a,b} is
undecidable.  
























In order to show undecidability with a single constant, we will need
the fact that each word of length at least 3 is determined by its
length and its strict subwords. For two words u,v∈ A^*, we write
u∼_n v if {u}∩ A^≤ n={v}∩ A^≤ n.

Let n≥ 2 and |u|=|v|=n+1. Then u=v if and only if u∼_n v.




  There is a word W∈{a,b}^* such that for every recursively
  enumerable set S⊆, there is a 13-formula
  τ over the structure [W]{a,b} such that
  
    τ={a^k | k∈ S}.

  In particular, the
  truth problem for the 13 fragment over
  [W]{a,b} is undecidable.


  In the proof of <ref>, we have constructed 13 formulas
  over A expressing successor, addition, and
  multiplication, more precisely: expressing “∃ n≥ 0
  u=a^n∧ v=a^n+1” and “∃ m,n≥ 0 u=a^m∧
  v=a^n∧ w=a^m+n” and “∃ m,n≥ 0 u=a^n∧
  v=a^m∧ w=a^m· n”. Let W_1,…,W_r∈{a,b}^* be
  the constants occurring in these three 13 formulas, plus
  ε. Let m the maximal length of any of these words, and
  let W=a^m+1b^m+2.

  Let S⊆ be recursively enumerable. Then, according to
  <ref> and by the choice of W_1,…,W_r, there is a
  13 formula φ that only uses constants from
  W_1,…,W_r and with φ={a^k | k∈ S}.
  We shall prove that using W, we can define all the words
  W_1,…,W_r. Consider the formula
  
    ∃ x_0,y_0,…,x_2m+3,y_2m+3       x_0⋯ x_2m+3 W∧ y_0⋯ y_2m+3 W  ∧
       ∃ x'_0,…,x'_m+1       x'_0⋯ x'_m+1 W ∧
       ∃ y'_0,…,y'_m+2       y'_0⋯ y'_m+2 W ∧
              x_1 y_1  ∧  x_1y'_m+2 ∧  y_1x'_m+1 ∧
       ∃ z_01       x'_1 z_01 ∧  x'_2z_01 ∧  y'_1 z_01 ∧ y'_2z_01 ∧
       ∃ z_10       x'_1 z_10 ∧  x'_2z_10 ∧  y'_1 z_10 ∧ y'_2z_10 ∧
              z_01 W  ∧  z_01 z_10

      If it is satisfied, then |x_i|=|y_i|=i for i∈[0,2m+3] and
      since x_1 y_1, we have {x_1,y_1}={a,b}. Since
      x_1y'_m+2 we get y'_i∈ y_1^* and thus
      y'_i=y_1^i for i∈[0,m+2], which is only possible with
      y_1=b. This implies x_1=a.  In particular, we get
      {z_01,z_10}={ab, ba}. Since z_01 W, we
      have z_01=ab and z_10=ba.  On the other hand, if |x_i|=|y_i|=i for i∈[0,2m+3],
      x_1=a, y_1=b,
      x'_i=a^i, y'_j=b^j for i∈[0,m+1], j∈[0,m+2], z_01=ab, and z_10=ba,
      then the formula is clearly satisfied.

      Hence, we can already define all words of length at most 2 and
      all words a^i and b^i for i∈[0,m+1]. This lets us define
      other predicates.
      
      
  * For each 0≤ℓ≤ m, we can express
        “|u|_a=ℓ” using the formula
        
    a^ℓ u  ∧ a^ℓ+1u

        Note that since ℓ+1≤ m+1, we can already define
        a^ℓ+1. The same way, we can express
        “|u|_b=ℓ”.
      
  * For each 0≤ℓ≤ m, we can express “|u|=ℓ”
        using the formula 
        
    ⋁_i+j=ℓ |u|_a=i
            ∧ |u|_b=j.

      
  * For each word w∈ A^≤ m, |w|>2, we can define
        w. We proceed by induction. For |w|≤ 2, we
        can already define w. Thus, suppose we can define
        every v∈ A^≤ n and let w∈
        A^n+1 with n+1≤ m. Consider the formula
        
    |u|=n+1  ∧ ⋀_v∈ A^≤ n, v w
            v u  ∧ ⋀_v∈ A^≤
                n, vw vu.

        Clearly, if u=w, then the formula is
        satisfied. On the other hand, suppose the formula is
        satisfied.  It expresses that {u}∩ A^≤ n={w}∩ A^≤ n.
        According to <ref>, this
        implies u=w.
      
      Note that all the variables we introduced to define the words in
      A^≤ m carry words of length at most 2m+3, meaning that
      we may assume that they are alternation bounded.  Thus, we can
      define all words in A^≤ m using forumlas in 10.
      Therefore, we can turn φ into a 13 formula
      τ that contains W as its only constant and satisfies
      τ=φ.

      It remains to show the second statement of the
      undecidable:single. Let S⊆ be
      recursively enumerable but undecidable and let k∈ be
      given. We choose the formula φ as above, but we
      modify it as follows. Let φ_0≡φ, and for
      i∈[1,k], let φ_i express
      
    ∃ yφ_i-1(y)∧∃ n x=a^n∧ y=a^n+1.
 
      Finally, let φ_k+1 be the formula ∃ xφ_k(x)∧ x=ε.  Note that by the choice of
      W_1,…,W_r, we may assume that φ_k+1 contains
      only the constants W_1,…,W_r. Note that φ_k+1
      has no free variables and is true if and only if k∈ S.  Now
      τ_k+1 is obtained from φ_k+1 just as τ is
      obtained from φ. It follows as above that τ_k+1
      is true if and only if k∈ S. This proves the second
      statement of the undecidable:single.



Here W must be complex enough: For instance, the Σ_1 fragment of
[ϵ]{a,b} and of [a]{a,b}, respectively, is decidable.

  The Σ_1-fragment of [ϵ,a]{a,b} is decidable.


  We may assume that the input formula is of the form

  φ≡∃ x_1,…,x_nψ, where ψ is a conjunction
  of literals of the following forms:
  
    c x        cx        x c            xc 
           x y            xy

   where c∈{ε, a} and x∈ X={x_1,…,x_n}. For each literal x c, we can
guess whether x=ϵ or x=a and hence assume that these do not occur. Literals of the form ϵ x are always satisfied, whereas ϵx is never satisfied. Hence, without loss of generality, these do not occur either and we may assume that all literals are of the form

    a x         ax           xϵ         xa 
           x y        xy.

Moreover xϵ is equivalent to xϵ and the literal ax is equivalent to x∈ b^*. We can therefore assume that all literals are of the form

    a x         x∈ b^*           xϵ         xa 
           x y        xy

Let L⊆ X be the set of those variables for
which we have a x∈ b^* literal. Clearly, x∈ b^* and xϵ together
mean x∈ b^+. In the same way, x∈ b^* and xa together mean x∈ b^+.
Furthermore, a x and x∈ b^* are mutually exclusive. Hence, we can rewrite our constraint system as follows: 


  * For each x∈ L, we have either a constraint x∈ b^* or x∈ b^+. 

  * For each x∈ X∖ L, we have a set of constraints of the form a x, xϵ, or xa.

  * We have constraints of the form x y and xy.

As a final reformulation step, note that every u∈{a,b}^*
satisfies either u∈ b^* or a u.  Therefore, we may
assume that for every x∈ X, we have either a constraint x∈ b^*
or x∈ b^+ (and hence x∈ L) or a x. Notice that if we
already have a x, then xϵ is redundant. Thus, we
have the following constraints:


  * For each x∈ L, we have either x∈ b^* or x∈ b^+.

  * For each x∈ X∖ L, we have a x and possibly xa.

  * A set of constraints of the form x y or xy.

We say that a partial order (X,≤) is compatible if 


  * L is downward closed and linearly ordered,

  * for each constraint x y (xy), we have x≤ y (x≰y).

We claim that φ is satisfied in
[ϵ,a]{a,b} if and only if there is a compatible
partial order on X. Since the latter is clearly decidable, this
implies the decidable-short.

Of course, if φ is satisfied, then the subword ordering
induces a compatible partial order on X. So let us prove the
converse and suppose (X,≤) is a compatible partial order and let
P=X∖ L. Then, (P,≤) is a partial order and we can find
some m≥ 0 such that (P,≤) embeds into the lattice {0,1}^m
of m-tuples over {0,1} with componentwise comparison. Consider
such an embedding with m≥ 2.  This embedding allows us to assign
to each x∈ P a word u_x∈ aβ_1⋯ aβ_m, where
β_1,…,β_m∈{ϵ,b} such that x≤ y if and
only if u_x u_y.

Now write L={ℓ_1,…,ℓ_k} with ℓ_1≤⋯≤ℓ_k. We now define a function
f X→{0,…,k}. Note
that for each x∈ P, the set {x}∩ L is a downward
closed subset of L and hence of the form {ℓ_1,…,ℓ_i} for
some i≥ 0. In this case, set f(x)=i.  Moreover, let

    P_i = {x∈ P |{x}∩ L={ℓ_1,…,ℓ_i}}.
 
This
allows us to construct an assignment of words v_x to variables
x. Let us explain the intuition.  In order ensure that
v_ℓ_1v_x for all x∈ P_0, we let v_x=u_x and
notice that then, the words v_x all contain at most m-many
b's. Hence, we set v_ℓ_i=b^m+1. Now, we have to make sure that
the words for v_x with x∈ P_1 all contain v_ℓ_1 as a
subword, so we pad the words u_x with b's on the left: We set
v_x=b^m+1u_x. Now, in turn, we need to make sure that v_ℓ_2
contains more than (m+1)+m-many b's, leading to
v_ℓ_2=b^2(m+1), and so on. Thus, we set:

    v_ℓ_i = b^i(m+1)       v_x = b^f(x)· (m+1) u_x

for i∈{1,…,k} and x∈ P. Let us show that this
assignment sastisfies our constraint system. 


  * Consider a constraint x y. We have x≤ y. 


  * If x,y∈ P, then {x}∩ L⊆{y}∩ L
  and thus f(x)≤ f(y). Since also u_x u_y, we have
  v_x v_y.

  * If y∈ L, then also x∈ L (since L is downward closed) and thus clearly v_x v_y.

  * If y∈ P and x∈ L. Suppose x=y_i and f(y)=j. By definition of f, we have i≤ j
and hence v_x=v_ℓ_i=b^i(m+1) b^j(m+1)u_y=v_y.


  * Consider a constraint xy. Then x≰y.


  * If x,y∈ P, then u_xu_y by choice of u_x and u_y. In particular, we have 
v_x=b^f(x)· (m+1) u_x b^f(y)· (m+1) u_y=v_y.

  * If x∈ P and y∈ L, then v_y∈ b^* and a v_x. Thus v_xv_y.

  * If x∈ L and y∈ P, say x=ℓ_i. Then x≰y means that ℓ_i∉{y}∩ L and hence f(y)<i.
Note that v_y=b^f(y)(m+1) u_y and that |u_y|_b≤ m. Therefore |v_y|_b≤ f(y)(m+1)+m<i(m+1) and hence 
v_x=v_ℓ_i=b^i(m+1)v_y.

  * If x,y∈ L, then x=y_i and y=y_j with j<i. Then clearly v_xv_y.


  * Constraints x∈ b^* or x∈ b^+ with x∈ L are of course satisfied.

  * Constraints xa with x∈ P are satisfied because |u_x|_a≥ m≥ 2 for every x∈ P.

This established our claim and thus the decidable-short.


This raises an interesting question: For which
sets {W_1,W_2,…}⊆ A^* of constants is the truth
problem for Σ_1 sentences over [W_1,W_2,…]A
decidable?





 §.§ The 21 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.


Let |A|≥ 2 and a∈ A. For each recursively enumerable set
S⊆, there is a 21 formula φ over the structure
A with one free variable such that φ={a^k
| k∈ S}. In particular, the truth problem for 21 is undecidable.




  * We can express “|u|_a≤ |v|_a” in 10:

    ∀ x∈ a^*  xu ∨ x v.

Hence, we can express “|u|_a=|v|_a” in 10.

  * We can express “|u|_a>|v|_a” in 10: This follows from the fact that
|u|_a≤|v|_a is expressible in 10.

  * We can express “|u|_a |v|_a” in 10 according to the previous item.

  * We can express “u∈ a^* ∧ v∈ (bu)^*” in 11. It clearly
suffices to express “u∈ a^* ∧ v∈ (bu)^+” in 11. Consider the formula

    v∈ b{a,b}^* 
     ∧ ∀ x∈ b^+a^*b^*[|x|_b |v|_b 
    ∨  (|x|_a>|u|_a∧ xv) 
     ∨  (|x|_a≤ |u|_a∧ x v) ].

Note that “v∈ b{a,b}^*” is expressible in 10 because
v∈ a{a,b}^* is expressible in 10 (see <ref> in
the proof of <ref>).

Moreover, notice that since b^*a^*b^*={a,b}^*∖a b a, the
language b^+a^*b^* = (b^*a^*b^*)∩ (b a∪ (b∖a))
is piecewise testable and thus definable in 00.

  * We can express “|u|_a=|v|_b” in 21:

    ∃ x∈ (a b)^*  |u|_a=|x|_a ∧ |v|_b=|x|_b.


  * We can express “∃ m,n u=a^m ∧ v=a^n ∧ w=a^m· n” in 21:

    u∈ a^*∧ v∈ a^*∧ w∈ a^*
     ∧∃ y∈ b^*∃ x∈ (bu)^*
    
    |x|_b=|y|_b ∧ |y|_b=|v|_a∧ |x|_a=|w|_a.

Note that we employ the variable y because directly expressing |x|_b=|v|_a
(using the previous item) would require an additional alternation unbounded
variable besides x, but we can only use one.

  * Recall that “|w|_a=|u|_a+|v|_a” is expressible in 10 (see
<ref> of <ref>) and hence “∃ m,n
u=a^m ∧ v=a^n∧ w=a^m+n” in 10.  Thus, we can implement
Diophantine equations as in the proof of <ref>.





 §.§ The Σ_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 Σ_2 fragment of A undecidable. We show
here that two letters suffice. Observe that if |A|=1, A can be
interpreted in (, <) and is thus decidable.

Let μ A^*→ A^* be a map. It is called a morphism if
μ(uv)=μ(u)μ(v) for all u,v∈ A^*.  It is an
anti-morphism if μ(uv)=μ(v)μ(u) for all u,v∈ A^*.
Finally, it is an automorphism of (A^*,) if for any
u,v∈ A^*, we have u v if and only if
μ(u)μ(v). 

Note that if we have no constants, we cannot define a language in
a^*, because all definable subsets are closed under automorphisms of
(A^*,). It will be useful for the next proof to
have a classification of all automorphisms of (A^*,).  The
following is shown implicitly by Kudinov et. al. <cit.>,
but we include a short proof for completeness.

  A map μ is an automorphism of (A^*,) if and only if
  
  
  * μ is either a morphism or an
    anti-morphism and
  
  * μ permutes A.
  


  Clearly, maps as described in the automorphisms are
  automorphisms.  Assume μ is an automorphism.  Since μ has to
  preserve the minimal element, we have
  μ(ε)=ε.  It also has to preserve the set of
  minimal elements of A^*∖{ε}, hence the set
  A. Repeating this argument yields that μ has to preserve
  length. Therefore, according to <ref>, if μ is
  identical on A^≤ n for n≥ 2, then it is the identity on
  A^≤ n+1. By induction, this implies that if an automorphism is
  identical on A^≤ 2, then it is the identity on A^*. Hence,
  if two automorphisms agree on A^≤ 2, then they are the
  same. It therefore suffices to show that every automorphism μ
  agrees on A^≤ 2 with a map as described in the
  automorphisms.

  Since μ preserves the set A, the map π=μ|_A is a
  permutation of A.  Moreover, for any a,b∈ A, we have
  μ(ab)=μ(a)μ(b) or μ(ab)=μ(b)μ(a).
  If μ(ab)=μ(a)μ(b), then we cannot have
  μ(bc)=μ(c)μ(b), because the two words ab and bc have
  only one common upper bound of length three (namely abc), whereas
  the words μ(a)μ(b) and μ(c)μ(b) have two, namely
  μ(c)μ(a)μ(b) and μ(a)μ(c)μ(b). Therefore, if
  μ(ab)=μ(a)μ(b), then μ(bc)=μ(b)μ(c). In particular,
  if μ(ab)=μ(a)μ(b), then we have μ(cd)=μ(c)μ(d) for
  all c,d∈ A. Hence on A^≤ 2, μ agrees with a map as
  decribed.















Let |A|≥ 2.  For each recursively enumerable set S⊆, there is a
Σ_2 formula τ over the structure A  that defines the language 

    τ={a^k| a∈ A, k∈ S}.

 In particular, the truth
problem for Σ_2 is undecidable.


Fix a letter a∈ A.  Let S⊆ be recursively enumerable, let
φ be the 13 formula provided by <ref>
with one free variable x and with φ={a^k | k∈
S}, and let w_1,…,w_m∈ A^* be the constants used in the formula
φ. 



It was shown in <cit.> that from w_1,…,w_m, one can construct
a Σ_2 formula ψ over A with free variables
V={x_1,…,x_m} such that for α∈ (A^*)^V, we have
α∈ψ if and only if there is an automorphism ·
A^*→ A^*  such that α(x_i)=w_i for every i∈[1,m].

Let φ' be the formula obtained from φ by replacing
every occurrence of w_i with x_i. Moreover, let τ≡∃
z_1,…,z_rψ∧φ'.

Then, τ is clearly a Σ_2 formula and has exactly one free variable, say x.
We claim that 

    τ={b^k | b∈ A,  k∈ S}.

If k∈ S, then a^k∈φ and hence clearly
b^k∈τ for each b∈ A.  Moreover, if
w∈τ, then for some α∈ψ,
we have α_wφ', where α_w denotes the
assignment with α_w|_V=α and α(x)=w. This means,
there is an automorphism · of (A^*,) such
that α(x_i)=w_i for i∈[1,m]. Therefore, there is
some w'∈ A^* that satisfies φ such that
w=w'. In particular, w'=a^k for some k∈ S and hence
w=b^k for some b∈ A. This proves <ref>. 

We can now proceed as
in <ref> to show undecidability of the truth
problem.



































§ COMPLEXITY

In this section, we study the complexity of the truth problem for the
ij fragments of A. 



 §.§ Complexity of i0

We begin with the case j=0.  In the
following, n denotes the n-th level of the weak 
hierarchy <cit.>.


If |A|≥ 2, then the truth problem for i0 is
-complete for i=1 and i-1-complete for i>1.

We provide a polynomial inter-reduction with the Σ_i
fragment of 
(,0,1,+,<), a.k.a.
Presburger Arithmetic (PA), for which Haase <cit.> has
recently proven i-1-completeness for i>1. The Σ_1 fragment of PA is -complete <cit.>.

The reduction from PA to
10 fixes a letter a∈ A and encodes every number k∈ by
a^k. Addition can then be expressed in 10 (<ref> of
<ref>). 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 A is just (,<), which has a -complete
truth problem <cit.>. Moreover, an
inspection of the proof of <ref> shows that an alternation
bound of ℓ=2 suffices to define addition, which is tight: if we only use a
bound of 1, we can also easily reduce to (,<).


The reduction from i0 to Presburger arithmetic encodes a word w
known to belong to (a_1^*⋯ a_n^*)^ℓ, i.e., of the form

    ∏_i=1^ℓ∏_j=1^n a_j^x_i,j,

by the vector
(x_1,1,…)∈^ℓ· n of exponents.
With this encoding, it suffices to show how to
express literals w w' (and also ww') by polynomial-size existential
Presburger formulas for w,w'∈ (a_1^*⋯ a_n^*)^ℓ.  For a vector
x=(x_1,1,…,x_ℓ,n) from ^ℓ· n, let
w_x =  ∏_i=1^ℓ∏_j=1^n a_j^x_i,j. 

There are existential Presburger formulas φ and ψ of size polynomial in n and ℓ such that

    φ (x_1,1,…,x_ℓ,n,y_1,1,…,y_ℓ,n)  w_x w_y, 
    ψ    (x_1,1,…,x_ℓ,n,y_1,1,…,y_ℓ,n)   w_xw_y.



Let us briefly describe these formulas. Let I=[1,ℓ]×[1,n] and order
 the pairs (i,j)∈ I 
lexicographically:  (i',j')<(i,j) if i'<i
or i=i' and j'<j. This captures  the order of
the a_j^x_i,j  factors in w_x. We now define
formulas τ_i,j and η_i,j where 
the t_i,j,k's and e_i,j,k's  are  extra free variables:

    τ_i,j      ⋀_1 ≤ k ≤ℓ t_i,j,k   = 
        0    if e_i',j',k'>0 for some
           (i',j')<(i,j)  and  k'>k 
    
        y_k,j  - ∑_i' = 1^i-1 e_i',j,k  otherwise
    η_i,j      ⋀_1 ≤ k ≤ℓ e_i,j,k   = min{ t_i,j,k ,  x_i,j-∑_r=1^k-1 e_i,j,r}

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 ℓ, we have polynomially many formulas of polynomial size. 

Define ξ=⋀_(i,j)∈ Iτ_i,j∧η_i,j and the formulas
φ,ψ as:

    φ[ ∃ t_1,1,1⋯∃ t_ℓ,n,ℓ; ∃ e_1,1,1⋯∃ e_ℓ,n,ℓ ]ξ∧⋀_(i,j)∈ I(x_i,j≤∑_k=1^ℓ e_i,j,k)
    
    ψ[ ∃ t_1,1,1⋯∃ t_ℓ,n,ℓ; ∃ e_1,1,1⋯∃ e_ℓ,n,ℓ ]ξ∧⋁_(i,j)∈ I(x_i,j>∑_k=1^ℓ e_i,j,k)

Since formulas τ_i,j and η_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, ψ is equivalent to the negation
of φ.  Moreover, φ expresses that there is enough room to embed
each factor a_j^x_i,j in w_y, i.e., that w_x w_y as claimed,
and both formulas are easily constructed in polynomial time.





 §.§ Complexity of 11



  
The truth problem for the 11 fragment is -complete.

Of course, hardness is inherited from 10.  Conversely,
-membership is shown by a reduction to the 10 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=∏_i=1^ka_i^ℓ_i with ℓ_i>0 and a_i≠ a_i+1 for all
i. By “an a-block of u” we mean an occurrence of a factor a_i^ℓ_i with a_i=a.
We note that requiring some bound in the number of blocks is equivalent to
bounding the number of alternations when it comes to defining the ij
fragments. However, counting blocks is more precise.



  Let t, x_1, …, x_n, y_1, …, y_m ∈ A^* such that:
  
  
  * for all i, x_i  t,
  
  * for all j, y_j t,
  
  * for all i and j, x_i and y_j have less than ℓ blocks,
  
  * t has k > (m+n)·ℓ + |A| blocks.
  
  Then there exists t' ∈ A^* such that:
  
  
  * for all i, x_i  t',
  
  * for all j, y_j t',
  
  * t' has either k-1 or k-2 blocks.
  



  Given u ∈ A^*, we write u for the image of the
  left-most embedding of u into t. This is a set of positions in t and, in case
  ut, these positions only account for the longest prefix of u
  that can be embedded in t. In particular, and since we assumed
x_i t and y_jt, then
| x_i|=|x_i| and | 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 ∉ t_1, one of the following holds:
    
    
  * there is  some i s.t. b_0 ∩ x_i≠∅ and t_1 ∩ x_i≠∅.
    
  * there is j s.t. b_0 ∩ y_j = ∅ and t_1 ∩ y_j ≠∅ and b_1 ∩ y_j ≠∅.
    
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)·ℓ irreducible blocks that are not right-most (and at most |A|
right-most blocks). Since k > (n+m)·ℓ + |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' = t_0 t_1 b_0 b_1 t_2. 


Claim: t' fulfills the requirements of
<Ref>.

     
Since b_1 is an a-block, b_0b_1 is now a block of t' and t' has less
than k blocks. Moreover, the only other possible block merge is in t_0t_1,
thus t' has at least k-2 blocks. We now show that  x_i t'
and y_jt' for all i,j.
  
  
  * Pick some i. Since x_i  t, there
    is a unique decomposition x_i = u_0 u_1 u_2 u_3 u_4 of x_i such that
    u_0 ⊆ t_0, u_1 ⊆ b_0, u_2 ⊆
    t_1, u_3 ⊆ b_1 and u_4 ⊆ t_2. 
Since b_0 is reducible one of u_1 or u_2 is empty.
Thus one of u_1 or u_2 is the empty word, allowing x_i t'.

  
  * Assume, by way of contradiction,  that for some j, y_j  t'.
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 ∩ z_1 = ∅. Otherwise, since a ∉ t_1,
  the left-most embedding of z_1 into t' = t_0 t_1 b_0 b_1 t_2 does not use
  t_1 at all and we would have y_j  t_0 b_0 b_1 t_2  t.

  * Secondly, t_1 ∩ z_1 is not empty. If it were, since b_0 is
  made of a's only and a ∉ 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  t_0 b_0 b_1 t_2  t.

  * Lastly, b_1 ∩ z_1 ≠∅. 





Otherwise, the already established fact b_0∩ z_1=∅
implies that y_j embeds not only in t' but in t_0t_1t_2, which is a subword of t.

  Since  b_0 is reducible, we conclude  that the original assumption that
  y_j t' does not hold, i.e., that y_jt' as required.

  
      



We now proceed to prove <Ref>.  Let φ be a
11 sentence, where t is the only variable which is not
alternation bounded.  As a first step of our  algorithm, we guess
the set of literals occurring in φ that is satisfied. After
guessing this subset, we check whether the formula would be satisfied
if exactly this subset were true (which essentially amounts to
evaluating a formula in propositional logic). If this is the
case, it remains to check whether it is possible to choose words for
all existential quantifiers of φ so that exactly this subset
of literals is true. This means, we are left with the task of checking
satisfiability of a formula φ of the form φ≡∃
tψ: Here, ψ begins with existential quantifiers for
alternation bounded variables, which are followed by a conjunction of
literals.

Every literal in ψ that involves t is of one of the following types:
  
  
  *  x  t, where x is an alternation bounded variable,
  
  *  y t, where x is an alternation bounded variable,
  
  *  t u, where u is an alternation bounded variable,
  
  *  t  z, where z is an alternation bounded variable,
  
  *  t  t,
  
  *  t t.
  
  Assertions of <ref> can be replaced by their truth
  value. If a literal t z of <ref> occurs in
  ψ, then φ is equivalent to ∃ t ∈ (a_1^* ⋯
  a_n^*)^ℓψ,
  where ℓ is the alternation bound of variable z.

  We can thus assume that only literals of <ref> occur in ψ. Let n
  be the number of variables x that occur in literals of <ref>, m the
  number of variables y that occur in literals of <ref>, ℓ the
  maximum alternation level of these variables, and k the maximum alternation
  bound of all variables u that appear in literals of <ref>.  Let 
  
    p = max{ (m+n)· (ℓ· |A|) + |A|,  k· |A| +3}.

  (here ℓ and k
  are multiplied by |A| to obtain a number of blocks from a maximum
  alternation). Then φ is equivalent to ∃ t ∈ (a_1^* ⋯
  a_n^*)^pψ. Indeed, if the restricted formula has a solution,
  it is a solution for ψ. Conversely, if ψ is satisfiable via some
  t∈ A^* having more than p blocks, then by <Ref>, one can
  also use a t having between k· |A| and p blocks. The fact that t
  has more than k· |A| blocks ensures that all literals t u
  are still satisfied.

  Finally, we can replace every ∃ t in φ by a bounded
  quantification and obtain an equivalent formula in 10 which proves
  <Ref>





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

    If PT languages are represented as boolean combinations of sets of the form
w with w∈ A^*, then their non-emptiness problem is -complete.
  
Membership in  follows from <ref>. For hardness, we can
reduce CNF-SAT as follows. We encode an assignment
α{x_1,…,x_n}→{0,1} as a word
b a^α(x_1)b a^α(x_2)⋯ b a^α(x_n). With literals
x_i and x_i, we associate the languages 
K_x_i=b^ia b^n-i and K_ x_i={a,b}^*∖b^ia b^n-i.  A clause C=L_1∨⋯∨ L_m is then translated to
K_C=K_L_1∪⋯∪ K_L_n and a conjunction of clauses  C_1∧⋯∧ C_k
is satisfiable if, and only if, the PT language (b(a+))^n∩ K_C_1∩⋯∩
K_C_k is nonempty.

In particular, given a finite
number of PT languages, the problem of deciding whether they intersect non-vacuously is
-complete. This is in contrast with general regular languages represented
by DFAs (or NFAs), for which the problem is well-known to be -complete <cit.>.

























 §.§ Complexity of 12



Our next result is an upper bound for the truth problem of 12.

The truth problem for 12 is in .

We prove <ref> in two steps.  The
first step of our decidability result is to transform a 12 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,…,a_n} and let V be a set of variables. A
constraint system is a set of constraints of the form x y,
xy, x=y, x∈(a_1^*⋯ a_n^*)^ℓ, or x=w, where
x,y∈ V, ℓ∈ and w∈ A^*. A constraint of the form x y,
xy, or x=y is also called (x,y)-constraint or
(y,x)-constraint.  Constraints of the form x∈ (a_1^*⋯
a_n^*)^ℓ are called alternation constraints.  The set of assignments
α∈ (A^*)^V that satisfy S is denoted by S.  For a
subset U⊆ 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
[U]S.

For a constraint system S over V, we define the graph Γ(S)=(V,E)
where {x,y}∈ E if and only if S contains an (x,y)-constraint.  We say
that S is tree-shaped if Γ(S)
is a forest. Furthermore, S is called alternation bounded if every
variable occurring in S also has an alternation constraint in S.


For any disjunction-free 12-formula φ, one can construct
polynomial-size constraint systems T and S over variables V'⊇φ such that 


  * T is tree-shaped,

  * S is alternation bounded, and

  * [φ]T∪ S=φ.



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 ∼⊆ V× V be an equivalence relation that
specifies which variables we want to identify with each other. Then we define
the quotient S/∼ as a constraint system over the variable
set V/∼ with the constraints

    S/∼ =     { [x]δ [y] |δ∈{,},  (xδ y)∈ S}. 
       ∪ {[x] = w |  (x=w)∈ S }
       ∪ {[x]∈ (a_1^*⋯ a_n^*)^ℓ| (x∈ (a_1^*⋯ a_n)^ℓ) ∈ 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' and
ψφ→ V' is an injective map. Then, via ψ, the
formula φ defines a set of assignments
[ψ]φ⊆ (A^*)^ψ.  We say that
φ and S are ψ-equivalent if
[ψ]S=[ψ]φ.

We may clearly assume that all literals are of the form
x y, xy, or x=w for w∈ A^* (and there are no
literals w x etc.).

We show the following stronger statement. Let B be the set of variables in
φ that are alternation bounded. For each disjunction-free
12-formula φ, there is a set of variables V', constraint
systems T and S over V', an injective map ψφ→ V' such that the following holds. If B'⊆ V'
denotes the set of variables for which there is an alternation bound in S,
then


  *  T is tree-shaped,

  *  S is alternation-bounded,

  *  T∪ S and φ are ψ-equivalent,

  *  for every x∈ B we have ψ(x)∈ B', and

  *  if |φ∖ B|=2 with φ∖ B={x,y}, then
ψ(x) and ψ(y) are either neighbors in Γ(T) or in distinct components.


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


  * Literals, i.e. x y, xy, 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.

  * Existentially quantified formulas ∃ xφ. Here, we
just reduce the set of free variables, so it suffices to adjust the map ψ.

  * Conjunctions φ≡φ_0∧φ_1. Suppose we have
constructed T_i,S_i,V'_i,ψ_i,B'_i as above for i=0,1. We may clearly
assume V_0∩ V_1=∅.  We construct T,S,V',ψ,B' as follows.  Let
∼⊆ (V'_0∪ V'_1)× (V'_0∪ V'_1) be the smallest
equivalence relation with ψ_0(x)∼ψ_1(x) for all
x∈φ∖ B. Then we take V'=(V'_0∪ V'_1)/∼
and define T=(T_0∪ T_1)/∼. Moreover, let

    S=S_0∪ S_1∪{[ψ_0(x)]=[ψ_1(x)] | x∈φ∩ B}.

Moreover, we choose ψφ→ V' so  that
ψ(x)=ψ_0(x) if x∈φ_0 and ψ(x)=ψ_1(x) if
x∉φ_0.

It is clear that <ref> above are
satisfied.  It remains to verify <ref>.


We distinguish the following cases.


  * |φ_i∖ B|≤ 1 for some i∈{0,1}. Then
there is at most one variable in V'_i that is identified with a variable in
V'_1-i by ∼. Hence, Γ(T) is obtained from Γ(T_0) and
Γ(T_1) either by disjoint union or by identifying one vertex from
Γ(T_0) with one vertex from Γ(T_1). In any case, Γ(T) is a
forest. Hence, <ref> is satisfied.

Let us now show <ref>. Hence, assume |φ∖
B|=2 with φ∖ B={x,y}.

Clearly, if φ_0∖ B and φ_1∖
B are disjoint, then no variables are identified and hence ψ(x) and
ψ(y) are in distinct components of Γ(T). Hence, we assume that
φ_0∖ B and φ_1∖ B have a
variable in common, say x.

Since |φ_0∖ B|≤ 1, this means
φ_1∖ B={x,y} and hence ψ_1(x) and ψ_1(y)
are neighbors in Γ(T_1) or they are in distinct components of Γ(T_1).

Γ(T) is obtained from Γ(T_0) and Γ(T_1) by identifying
ψ_0(x) and ψ_1(x).  Therefore, ψ(x) and ψ(y) are neighbors
in Γ(T) if and only if they are neighbors in Γ(T_1).  Moreover,
they are in disjoint components of Γ(T) if and only if they are in
disjoint components of Γ(T_1). This proves <ref>.




  * |φ_0|=|φ_1|=2. Write
φ_0∖ B=φ_1={x,y}. Note that
Γ(T) is obtained from Γ(T_0) and Γ(T_1) by identifying
ψ_0(x) with ψ_1(x) and identifying ψ_0(y) with ψ_1(y).
Since for each i∈{0,1} we know that ψ_i(x) and ψ_i(y) are
either neighbors in Γ(T_i) or in distinct components, this clearly
implies that Γ(T) is a forest. Hence, we have shown <ref>.

Moreover, if for some i∈{0,1}, ψ_i(x) and ψ_i(y) are neighbors
in Γ(T_i), then ψ(x) and ψ(y) are neighbors in Γ(T).
Otherwise, ψ(x) and ψ(y) are in disjoint components of Γ(T).
This proves <ref>.










 §.§ 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 <cit.>.  In terms of expressiveness,
these are equivalent to the classical reversal-bounded counter
automata <cit.>, 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 =(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⊆ Q× (A∪{})^V ×^C × Q
 
is the finite set of edges, q_0∈ Q is the
initial state, and F is a finite set of pairs
(q,φ), where q∈ Q and φ is an existential Presburger
formula with free variables in C.  A configuration of  is a tuple
(q,α,μ), where q∈ Q, α∈ (A^*)^V, μ∈^C. The step
relation is defined as follows. We have  
(q,α,μ)[] (q',α',μ')
iff there is an edge (q,β,ν,q')∈ E such that α'=αβ and μ'=μ+ν. 
A counter automaton accepts a set of assignments, namely

    ={α∈(A^*)^V |∃ (q,φ)∈ F 
      (q_0,,0)[] (q,α,μ),  μφ} .





























We call a subset R⊆ (A^*)^V a counter relation if there is a
counter automaton  with R=. If |V|=1, say V={x}, then
 defines a subset of A^*, namely the language {w∈ A^* | (x↦ w)∈}.  Languages of this form are called counter languages.

Suppose V_0,V_1 are sets of variables with |V_0∩ V_1|≤ 1. Let
_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∩ C_1=∅. Then a simple product construction
yields a counter automaton
_0⊗_1=(Q_0× Q_1,A,C_0∪ C_1,E,(q_0,0,q_0,1),F) over V_0∪ V_1
such that ((p_0,p_1), α, μ)[_0⊗_1] ((p'_0,p'_1),α',μ') iff 

    (p_i,α|_V_i, μ|_C_i) __i (p'_i,α'|_V_i,μ'|_C_i)

for i=0,1 and 

    F={((p_0,p_1), φ_0∧φ_1) |(p_i,φ_i)∈ F_i for i=0,1}.



Given a tree-shaped constraint system T, one can construct in exponential time
a counter automaton  with =T.







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∈ A^* or x∈(a_1^*⋯ a_n^*)^ℓ for some ℓ∈ and can easily
be imposed afterwards in the counter automaton.

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

Since Γ(T) is a forest, it contains a vertex x∈ V with at most one
neighbor. Let T' be the constraint system obtained from T by removing all
constraints involving x and suppose we have already constructed a counter
automaton ' with '=T'. 

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” be the set of all
(x,y)-constraints in T. Now note that if ” is a counter automaton
with ”=T”, then we have 

    '⊗” = T'∪ T”=T.

Therefore, it suffices to construct in polynomial time a counter automaton ”
with ”=T”.











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 y      (iii) y x      (iv) x 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 that last case, one can notice
that x y holds if either


  * |x|<|y| and xy or

  * |y|<|x| and yx or 
  * |x|=|y| and x 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 <ref> by taking the
constraint system provided by <ref> and
construct a counter automaton just for T using
<ref>.  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 <ref> 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
φ.  The  upper bound then follows from the fact that
non-emptiness for counter automata is -complete.


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

The non-emptiness problem for counter automata is -complete.


Given a counter automaton =(Q,A,C,E,q_0,F), and a state q∈ Q, we
can construct an existential Presburger formula θ_q with a free variable
for each edge in  that is satisfied for an assignment ν∈^E iff
there is a run from q_0 to q where each edge e∈ E occurs exactly
ν(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 <cit.>.

For each edge e=(p,α,μ,p'), define μ_e=μ.  Then the formula

    ⋁_(q,φ)∈ Fθ_q∧⋀_c∈ C c = μ_e(c)· e ∧φ

expresses precisely that there is an accepting run. The fact that the
satisfiability problem for existential Presburger arithmetic is
-complete <cit.> now gives us the upper bound as well as the
lower bound.






We are now ready to prove <ref>.

First we use <ref> to turn the formula
φ into constraint systems T and S such that T is tree-shaped, S
is alternation bounded, and [φ]T∪
S=φ. Then we use
<ref> to to obtain in exponential time a
counter automaton  with =T.

Let U={x_1,…,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 _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∈ U, w∈
A^*) by adding existential Presburger formulas that express subword
constraints as provided by <ref>.

We may clearly assume that whenever there is a variable x, an alternation
constraint x∈(a_1^*⋯ a_n^*)^ℓ, and a constraint x=w, then
w∈(a_1^*⋯ a_n^*)^ℓ: Otherwise, the system is not satisfiable and
clearly has an equivalent counter automaton.

Let A={a_1,…,a_n}.  Since S is alternation bounded, S contains an
alternation constraint x_i∈ (a_1^*⋯ a_n^*)^ℓ_i for each
i∈[1,m]. Let ℓ be the maximum of all these ℓ_i.  We will use the
counter variables c_i,j,k for each i∈ [1,m], j∈ [1,ℓ], and k∈
[1,n]. We set up the automaton _i over V_i={x_i} such that it has an
initial state q_0, a state q_1, and satisfies

    (q_0,,0) [_i] (q_1,α,μ)

if and only if α maps x_i to the word

    a_1^μ(c_i,1,1)⋯ a_n^μ(c_i,1,n)⋯ a_1^μ(c_i,ℓ_i,1)⋯ a_n^μ(c_i,ℓ_i,n).

This can clearly be done with n·ℓ states. Moreover, let
F_i={(q_1,⊤)}.  Note that _i has the counters c_i,j,k even for
j>ℓ_i although it never adds to them.  The reason we have the variables
c_i,j,k for j>ℓ_i is that this way, the formulas from
<ref> are applicable.

Note that since each V_i is a singleton, the automaton
=×_1⊗⋯⊗_m is defined. It satisfies
=S', where S' 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∈ U, w∈ A^*. Let
R⊆ S be the set of these remaining constraints. For each i and for
μ∈ (A^*)^V, let w_μ,i be the word in
<ref>. According to <ref>,
for each constraint r∈ R, we can construct a polynomial size existential
Presburger formula κ_r such that μκ_r if and only if
the constraint is satisfied for the assignment α with
α(x_i)=w_μ,i. Moreover, let κ=⋀_r∈ Rκ_r.

Suppose =(Q,A,C,E,q_0,F).
In the last step, we construct the counter automaton '=(Q,A,C,E,q_0,F'), where

    F'={(q,ψ∧κ) | (q,ψ)∈ F }.

Now ' clearly satisfies '=T∪ S.  Thus, if
we obtain ” from ' by projecting the input to those variables that
occur freely in φ, then
”=[φ]T∪ S. Moreover, ” can
clearly be constructed in exponential time.

The membership of the truth problem in  follows from the fact that
emptiness of counter automata is in  (<ref>).












§ EXPRESSIVENESS



































In this section, we shed some light on which predicates or languages are
definable in our fragments ij.



 §.§ Expressiveness of the 10 fragment

A language L definable in 10 always satisfies
L⊆ (a_1^*⋯ a_n^*)^ℓ for some ℓ∈. Hence, it can be
described by the set of vectors that contain the occurring exponents.  As can
be derived from results in <ref>, 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 ^V, we denote the set of mappings
V→.  By a partition of V, we mean a set P={V_1,…,V_n}
of subsets V_1,…,V_n⊆ V such that V_i∩ V_j=∅ for
i j and V_1∪⋯∪ V_n=V. If U∩ V=∅ and α∈^U, β∈^V, we write α×β for the map
γ∈^U∪ V such that γ|_U=α and γ|_V=β.
Furthermore, if S⊆^U, T⊆^V, then S×
T={α×β|α∈ S, β∈ T}.
A semilinear set S⊆^V is P-compatible if it has
a semilinear representation where each occurring period vector belongs
to ^V_i for some i∈[1,n].


Suppose L⊆ (a_1^*⋯ a_n^*)^ℓ.  Let V={x_i,j|
i∈[1,ℓ], j∈[1,n]} and consider the partition P={V_1,…,V_n}
where V_j={x_i,j| i∈[1,ℓ]} for j∈[1,n]. The language L is
definable in 10 if, and only if, the set

    {α∈^V | a_1^α(x_1,1)⋯ a_n^α(x_1,n)⋯ a_1^α(x_ℓ,1)⋯ a_n^α(x_ℓ,n)∈ L }

is a P-compatible semilinear set.

For example, this means we can define {a^nba^n | n∈}, but not
{a^nb^n| n∈}: A semilinear representation for the latter requires
a period that produces both a's and b's.

The proof of <ref> employs a characterization of
P-compatible sets in terms of Presburger arithmetic.  Let V be a set of
variables and φ be a Presburger formula whose variables are in V.
Let P={V_1,…,V_n} be a partition of V.  We say φ is
P-compatible if there is a set of variables V'⊇ V and a
partition P'={V'_1,…,V'_n} of V' such that 


  * V_j⊆ V'_j for each j∈[1,n] and

  * in each literal in φ, all variables belong to the same set V'_j
for some j∈[1,n].


The following is a simple observation.

Let P={V_1,…,V_n} be a partition of V. For sets S⊆^V,
the following conditions are equivalent:


  *  S is a P-compatible semilinear set.

  *  S=φ for some P-compatible existential
Presburger formula φ.

  *  S is a finite union of sets of the form A_1×⋯× A_n
where each A_j is a semilinear subset of ^V_j.



The directions partition:cartesianpartition:semilinear and
partition:semilinearpartition:formula are easy to see, so we show
partition:formulapartition:cartesian.

If a set satisfies the condition of <ref>, then projecting
to a subset of the coordinates yields again a set of this form. Therefore, it
suffices to consider the case where in φ, there are no quantifiers.
Now, bring φ into disjunctive normal form. Since each literal in
φ only mentions variables from V_j for some j∈[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

    φ≡⋁_i=1^k ⋀_j=1^n φ_i,j,

where φ_i,j only mentions variables from V_j. This implies

    φ = ⋃_i=1^k φ_1,j×⋯×φ_n,j,

which is the form required in <ref>.





We are now ready to prove <ref>.

If L is definable in 10, 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 <ref>.  Observe
that these formulas are P-compatible. This means that S is P-compatible.

For the converse, suppose S is P-compatible. According to
<ref><ref>, S is defined by a
P-compatible existential Presburger formula φ. Hence, φ has
free variables V={x_i,j| i∈ [1,ℓ], j∈[1,n]} and uses variables
V'⊇ V that are partitioned as V'=_j=1^n V'_j so that in
each literal, all occurring variables belong to the same V'_j.

In the first step, we turn φ into a 10 formula
φ̅ with the same number of free variables.  For each x∈ V', we
take a fresh variable x̅, which will hold words in a_j^*. More
precisely, we have our new variables V̅={x̅| x∈ V'} and a
mapping ι^V'→ (A^*)^V̅ defined by
ι(α)(x̅)=a_j^α(x), where j is the unique index with
x∈ V'_j. We want to construct φ̅ so that
φ̅=ι(φ).

We obtain φ̅ from φ as follows. For each literal x=y+z,
we know that there is a j∈[1,n] with x,y,z∈ V'_i, so we can replace
the literal with |x̅|_a_j=|y̅|_a_j+|z̅|_a_j, which is
expressible in 10 according to <ref> in the proof of
<ref> (note that in this case, we actually are in
10 because the variables x̅, y̅, and z̅ range
over a_j^* and are thus alternation bounded). Since we can clearly also
express |x̅|_a_j |y̅|_a_j in 10, we use this to
implement literals x y with x,y∈ V'_j.  Literals of the form x=k
with k∈ and x∈ V'_j can just be replaced by x̅=a_j^k.  Then we
clearly have φ̅=ι(φ).

In the second step, we construct the words

    a_1^α(x_1,1)⋯ a_n^α(x_1,n)⋯ a_1^α(x_ℓ,1)⋯ a_n^α(x_ℓ,n)

for α∈φ. This is possible thanks to
<ref> of the proof of <ref>. We can
express

    u=x̅_1,1⋯x̅_1,n⋯x̅_ℓ,1⋯x̅_ℓ,n

by applying <ref> exactly ℓ· n-1 times, once to
append each x_i,j to the word defined so far, using ℓ· n-1
additional variables. Of course, all these variables can be restricted to
(a_1^*⋯ a_n^*)^ℓ, which means the resulting formula belongs to
10. Moreover, it clearly defines L.






Our characterization of 10 is decidable.
We use a technique from <cit.>, 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.  

Given a semilinear subset S⊆^V and a partition P of V, it is
decidable whether S is P-compatible.


For α∈^V_i and γ∈^V, we write
γ[i/α] to be the element of ^V with

    γ[i/α](v)=α(v)    if v∈ V_i,
    γ(v)    otherwise.

For α,β∈^V_i, we write α∼_iβ if for every
γ∈^V, we have γ[i/α]∈ S if and only if
γ[i/β]∈ S. Moreover, for γ∈^V, we will use the norm
· as defined by γ=∑_v∈ Vγ(v). We claim that
S is P-compatible if and only if

    ∃ k∈⋀_i=1^n ∀α∈^V_i∃β∈^V_iβ≤ k, α∼_iβ.

Suppose <ref> holds. For each β∈^V_i, we define
S_i,β={α∈^V_i|α∼_iβ}.
Then S_i,β⊆^V_i is semilinear and we have

    S = ⋃_β_1∈^V_1,β_1≤ k⋯⋃_β_n∈^V_n,β_n≤ k S_1,β_1×⋯× S_n,β_n.

Hence, S is P-compatible.

Now assume S is P-compatible. Then we can write S=⋃_j=1^ℓ
A_j,1×⋯× A_j,n, where each A_j,i⊆^V_i is
semilinear. For each i∈[1,n], consider the function κ_i^V_i→{1,…,ℓ} with

    κ_i(α)={j∈[1,ℓ] |α∈ A_j,i}.

Observe that if κ_i(α)=κ_i(β), then α∼_iβ.
Since κ_i has a finite codomain, this means the equivalence relation
∼_i on ^V_i has finite index. This immediately implies
<ref>.

Since we can clearly formulate the condition <ref> 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,
<ref> generalizes the decidability of
recognizability.
Let M be a monoid. A subset S⊆ M is called recognizable if
there is a finite monoid F and a morphism φ M→ F such that
S=φ^-1(φ(S)).

Suppose P consists only of singletons. Then S⊆^V is
P-compatible if and only if it is recognizable.


Mezei's Theorem <cit.> states that if M_1,…,M_n are monoids,
then a subset of M_1×⋯× M_n is recognizable if and only if it
is a finite union of sets S_1×⋯× S_n such that S_i⊆
M_i is recognizable for i∈{1,…,n}.

Combined with the fact that a subset of  is semilinear if and only if it is
recognizable, the condition <ref> of
<ref> yields the result.








 §.§ Expressiveness of 10 vs. 11

It is obvious that
11 is strictly more expressive than 10, because it permits the definition of
languages with unbounded alternations, such as {a,b}^*. But is this the
only difference between the two fragments? In other words: Restricted to alternation
bounded languages, is 11 more expressive? The answer is no.

If L⊆ (a_1^*⋯ a_n^*)^ℓ, then L is definable in
11 if and only if it is definable in 10.


  Let φ be a 11 formula where the free variable is
  alternation bounded and the variable t is not alternation
  bounded. We can transform φ into a disjunction
  ⋁_i=1^k φ_i, where each φ_i belongs to
  11 and consists of a block of existential quantifiers
  followed by a conjunction of literals. Then, the proof of
  <ref> yields for each φ_i a (polynomial) bound
  p_i so that if we replace the quantifier ∃ t in
  φ_i by ∃ t∈ (a_1^*⋯ a_n^*)^p_i, the
  resulting 10 formula is equivalent.


This allows us to reason beyond alternation bounded languages. We have seen in
the proof of <ref> that one can express “|u|_a=|v|_b”
in 13, 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 11? We cannot:

The predicate “|u|_a=|u|_b” is not definable in 11.


Otherwise, we could define the set {a^nb^n |
n≥ 0} in 11, hence in 10, contradicting <ref>.






 §.§ Expressiveness of 12 vs. 13

We have seen in <ref> that 13 can express all
recursively enumerable unary languages. Moreover,
<ref> tells us that the languages
definable in 12 are always counter languages.

How do the fragments compare with respect to natural (binary) predicates on
words. We already know from <ref> in <ref>
that over two letters, the prefix relation is expressible in 13.  Note that the
following expressiveness:prefix does not follow directly from the
fact that for any 12 formula φ, the set
φ is a counter relation, as shown in <ref>.
This is because the prefix relation is a counter relation (and even rational). 

In 12, “u is a prefix of v” is not expressible.


Suppose the prefix relation were expressible using a 12 formula
φ. Then, by reversing all constants in φ, we obtain a formula
expressing the suffix relation.  Let  denote the prefix relation and
 the suffix relation. We can now express

    ∃ v∈{a,b}^* v u∧ v u ∧ |u|_a=2· |v|_a ∧ |u|_b=2· |v|_b,

which is equivalent to u∈ S, where S={vv | v∈{a,b}^*}.  Note
that |u|_a=2· |v|_a can be expressed by using |u|_a=|v|_a+· |v|_a,
which can be done in 10 according to <ref> in
<ref>.

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 <cit.>).  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 12 formula  φ,
the set φ is a counter relation, as shown in <ref>.








§ CONCLUSION




We have shown that the Σ_1 theory of the subword ordering is undecidable
(already for two letters), if all words are available as constants.  This
implies that the Σ_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, we introduced the fragments ij. We have completely
settled their decidability status. In terms of complexity, the only open case
is the 12 fragment.  We have an  lower bound and an 
upper bound. 

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











