2017/01/25 by Halfon, Simon, Schnoebelen, Philippe, Zetzsche, Georg
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1701.07470
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the Σ1 theory is undecidable (already over two letters). We investigate the decidability border by considering 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. We prove that when at most two variables are not alternation bounded, the Σ1 fragment is decidable, and that it becomes undecidable when three variables are not alternation bounded. Regarding higher quantifier alternation depths, we prove that the Σ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.