First-order Logic Over the Sub-word Ordering

This talk reports on results concerning first-order logic over the subword ordering on finite words. It has been known since 2006 that the whole first-order logic over this structure is undecidable, whereas the Sigma_1 fragment is NP-complete. One might therefore expect that introducing each word as a constant would leave the Sigma_1 fragment decidable.  However, it was shown recently that in the presence of these constants, the \Sigma_1 theory becomes undecidable (already over two letters).

Regarding the decidability border, we will consider fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations.  Here, the second result is that when at most two variables are not alternation bounded, the \Sigma_1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded.  Concerning higher quantifier alternation depths, the \Sigma_2 fragment is undecidable already for one variable without alternation bound and that when all variables are alternation bounded, the entire first-order theory is decidable. If time permits, complexity aspects will be treated as well.

This is joint work with Simon Halfon and Philippe Schnoebelen (to be presented at LICS 2017).