I'm concerned with the validity problem for sentences of first-order logic over finite words, i.e. $FO[\le]$ interpreted over finite subsets of $\mathbb{N}$. AFAIK it should be nonelementary.

However, I'm looking at the complexity of the levels of the alternation hierarchy, i.e., $\Sigma_n$ and $\Pi_n$ fragments of $FO[\le]$. For example, the satisfiability problem for Bernays-Schönfinkel formulae, those of the form $\exists^*\forall^*\phi$, a.k.a. $\Sigma_2$-formulae, is in general $\mathsf{NEXPTIME}$-complete, and this should hold also on words, is this correct? But then what is the complexity of satisfiability/validity for $\Sigma_n$-formulae for a fixed $n$?

I've found a lot of papers and surveys about the expressibility problem for these fragments, that is, to decide whether a given language can be expressed in a given fragment, but nothing on the computational complexity of the validity/satisfiability problem. I'm feeling like I'm missing something very trivial or commonly known.

Can you give me any reference?

  • $\begingroup$ It’s not very clear to me from the notation what you mean by “words”, but in general, satisfiability of $\forall_2$ sentences and validity of $\exists_2$ sentences (i.e., any levels outside the Bernays–Schönfinkel class) are undecidable. $\endgroup$ Commented Oct 11, 2016 at 12:07
  • 5
    $\begingroup$ Over finite words, I think it's a kind of folklore result that you get the exponential hierarchy. The upper bound goes through automata, with one exponential blow-up per nested negation, and presumably the lower bound of Stockmeyer matches this. See for instance Chapter 13 by Klaus Reinhardt in LNCS 2500; I do not know of a publication where the exact complexity is given, though. $\endgroup$
    – Sylvain
    Commented Oct 11, 2016 at 12:59
  • $\begingroup$ @EmilJeřábek My meaning of "words" is that from formal languages theory, i.e. elements of $\Sigma^*$ for some alphabet $\Sigma$. In a logical context, each word corresponds to a structure over $\langle \le, \{P_\sigma\}_{\sigma\in\Sigma} \rangle$ vocabulary, with natural numbers as the intended domain, or subsets of $\mathbb{N}$ as in the case of finite words. $\endgroup$ Commented Oct 11, 2016 at 13:08
  • $\begingroup$ @Sylvain Right, in the translation to automata, the exponentials come from the negations, not from quantifiers. That would mean that limiting the quantifier alternation should not change the complexity at all, if I still allow any propositional depth inside the quantifier-free part, right? $\endgroup$ Commented Oct 11, 2016 at 13:10
  • 2
    $\begingroup$ @gigabytes No, $\forall$ is defined as the dual of $\exists$; it introduces a negation and quantifier alternation impacts the complexity. $\endgroup$
    – Sylvain
    Commented Oct 11, 2016 at 14:30


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.