English

Existential Definability over the Subword Ordering

Logic in Computer Science 2024-02-14 v4 Formal Languages and Automata Theory

Abstract

We study first-order logic (FO) over the structure consisting of finite words over some alphabet AA, 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\Sigma_1 (i.e., existential) fragment is undecidable, already for binary alphabets AA. 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 A3|A|\ge 3, then a relation is definable in the existential fragment over AA with constants if and only if it is recursively enumerable. This implies characterizations for all fragments Σi\Sigma_i: If A3|A|\ge 3, then a relation is definable in Σi\Sigma_i if and only if it belongs to the ii-th level of the arithmetical hierarchy. In addition, our result yields an analogous complete description of the Σi\Sigma_i-fragments for i2i\ge 2 of the pure logic, where the words of AA^* are not available as constants.

Keywords

Cite

@article{arxiv.2210.15642,
  title  = {Existential Definability over the Subword Ordering},
  author = {Pascal Baumann and Moses Ganardi and Ramanathan S. Thinniyam and Georg Zetzsche},
  journal= {arXiv preprint arXiv:2210.15642},
  year   = {2024}
}
R2 v1 2026-06-28T04:39:56.849Z