Pascal Baumann ; Moses Ganardi ; Ramanathan S. Thinniyam ; Georg Zetzsche - Existential Definability over the Subword Ordering

lmcs:10219 - Logical Methods in Computer Science, December 21, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:35)2023
Existential Definability over the Subword OrderingArticle

Authors: Pascal Baumann ; Moses Ganardi ; Ramanathan S. Thinniyam ; Georg Zetzsche

    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 $\Sigma_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 $\Sigma_i$: If $|A|\ge 3$, then a relation is definable in $\Sigma_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 $\Sigma_i$-fragments for $i\ge 2$ of the pure logic, where the words of $A^*$ are not available as constants.


    Volume: Volume 19, Issue 4
    Published on: December 21, 2023
    Accepted on: November 10, 2023
    Submitted on: October 28, 2022
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory

    Consultation statistics

    This page has been seen 544 times.
    This article's PDF has been downloaded 110 times.