Decidability in the logic of subsequences and supersequences

Abstract

We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Σ_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO2 theory is decidable while the FO3 theory is undecidable.

Cited by in corpus (1)

• Defining Recursive Predicates in Graph Orders