Decidability in the logic of subsequences and supersequences

TL;DR

This paper investigates the decidability of various logical fragments over sequences ordered by subsequence embedding, revealing undecidability of certain theories and decidability of others with bounded variables.

Contribution

It establishes the undecidability of the  theory and the FO3 fragment, while proving the FO2 fragment's decidability in the logic of subsequences.

Findings

 theory is undecidable

FO2 theory is decidable

FO3 theory is undecidable

Abstract

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 FO2 theory is decidable while the FO3 theory is undecidable.