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

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 Sigma1 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 Sigma1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the Sigma2 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.