6
$\begingroup$

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?

| cite | improve this question | |
$\endgroup$
  • $\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$ – Emil Jeřábek Oct 11 '16 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 Oct 11 '16 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$ – gigabytes Oct 11 '16 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$ – gigabytes Oct 11 '16 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 Oct 11 '16 at 14:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.