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

## TL;DR

This paper explores the decidability and complexity of first-order logic over the subword ordering of finite words, identifying precise boundaries where the logic transitions from decidable to undecidable.

## Contribution

It establishes new decidability results for fragments of the first-order theory over subword ordering based on variable bounds and alternation constraints.

## Key findings

- The $oldsymbol{ ext{Sigma}_1}$ theory is undecidable over two-letter alphabets.
- Decidability is achieved when at most two variables are not alternation bounded.
- The entire first-order theory is decidable when all variables are alternation bounded.

## 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.