Decidability in the Logic of Subsequences and Supersequences
Prateek Karandikar, Philippe Schnoebelen · arXiv (Cornell University) · 2015
We consider first-order logics of sequences ordered by the subsequence ordering, aka sequence embedding. We show that the Sigma_2 theory is undecidable, answering a question left open by Kuske. Regarding fragments with a bounded number of variables, we show that the FO^2 theory is decidable while the FO^3 theory is undecidable.