Existential Definability over the Subword Ordering
Pascal Baumann, Moses Ganardi, Ramanathan S. Thinniyam, Georg Zetzsche
TL;DR
This work analyzes first-order logic over the subword order on words, focusing on quantifier-alternation fragments. For alphabets with $|A|\ge 3$, the existential fragment with constants defines exactly the recursively enumerable relations, and more generally each $\Sigma_i$-fragment coincides with the $i$-th level of the arithmetical hierarchy $\Sigma_i^0$. The authors develop a constructive approach using rational transductions and a generator language $G=\{a^nb^n\mid n\ge 0\}^*$ to realize all RE relations, and then extend from two-letter alphabets to arbitrary $A$ via projections, with a single constant $W$ sufficing in a strengthened variant. These results yield a precise level-by-level correspondence for $\Sigma_i$-definability (both with constants and in the pure logic modulo automorphism-invariance) and establish undecidability of the existential fragment in the appropriate setting, all without relying on Diophantine equations. Altogether, the paper clarifies the expressive power of subword FO fragments and maps their capabilities directly onto the arithmetical hierarchy, providing a solid foundation for future work on the remaining binary alphabet case and related logics.
Abstract
We study first-order logic (FO) over the structure consisting of finite words over some alphabet $A$, together with the (non-contiguous) subword ordering. In terms of decidability of quantifier alternation fragments, this logic is well-understood: If every word is available as a constant, then even the $Σ_1$ (i.e., existential) fragment is undecidable, already for binary alphabets $A$. However, up to now, little is known about the expressiveness of the quantifier alternation fragments: For example, the undecidability proof for the existential fragment relies on Diophantine equations and only shows that recursively enumerable languages over a singleton alphabet (and some auxiliary predicates) are definable. We show that if $|A|\ge 3$, then a relation is definable in the existential fragment over $A$ with constants if and only if it is recursively enumerable. This implies characterizations for all fragments $Σ_i$: If $|A|\ge 3$, then a relation is definable in $Σ_i$ if and only if it belongs to the $i$-th level of the arithmetical hierarchy. In addition, our result yields an analogous complete description of the $Σ_i$-fragments for $i\ge 2$ of the pure logic, where the words of $A^*$ are not available as constants.