2026-07-22T13:50:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15817 2024-03-06T10:56:15Z ddc:004 open_access

Existential Definability over the Subword Ordering Baumann, Pascal Ganardi, Moses Thinniyam, Ramanathan S. Zetzsche, Georg subword subsequence definability expressiveness first order logic existential fragment quantifier alternation 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 Σ₁ (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| ≥ 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| ≥ 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 ≥ 2 of the pure logic, where the words of A^* are not available as constants. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pascal Baumann and Moses Ganardi and Ramanathan S. Thinniyam and Georg Zetzsche 2022 Is Part Of LIPIcs, Volume 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2022.7 urn:nbn:de:0030-drops-158178 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2022.7 eng https://creativecommons.org/licenses/by/4.0/legalcode