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

arXiv: https://arxiv.org/abs/1701.07470 · HTML: https://mlsanity.com/paper/1701.07470/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Jan 2017.

## Built on by (most cited first, 2 of 2)

- [Scattered Factor Universality -- The Power of the Remainder](https://mlsanity.com/paper/2104.09063/) (2021)
- [Directed Regular and Context-Free Languages](https://mlsanity.com/paper/2401.07106/) (2024)

## Abstract (arXiv)

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.