<p>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.</p>

<p>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$?</p>

<p>I've found a lot of papers and surveys about the <em>expressibility</em> 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 <em>validity</em>/<em>satisfiability</em> problem. I'm feeling like I'm missing something very trivial or commonly known.</p>

<p>Can you give me any reference?</p>

CC BY-SA 3.0
2016-10-11T12:07:31.770Z
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.
Emil Jeřábek
CC BY-SA 3.0
2016-10-11T12:59:17.557Z
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.
Sylvain
CC BY-SA 3.0
2016-10-11T13:08:00.837Z
@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.
Nicola Gigante
CC BY-SA 3.0
2016-10-11T13:10:41.120Z
@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?
Nicola Gigante
CC BY-SA 3.0
2016-10-11T14:30:05.053Z
@gigabytes No, $\forall$ is defined as the dual of $\exists$; it introduces a negation and quantifier alternation impacts the complexity.
Sylvain
CC BY-SA 3.0
2016-10-11T14:36:58.757Z
@Sylvain oops, yes, of course. So the point is the number of negations that happen to contain some quantifiers. In other words: it is the negation of an existential that causes the blowup, not just any negation. This means that if I fix the quantifier alternation, then the number of negations inside the unquantified part do not cause other blowups.
Nicola Gigante
<lo.logic><complexity>
Complexity of validity of first-order logic over finite words with bounded quantifier alternation?
Nicola Gigante
# Complexity of validity of first-order logic over finite words with bounded quantifier alternation?

(Asked by: username_0 on 2016-10-11)

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?

**Tags:** lo.logic, complexity
> **Comments:**
> **username_1**: 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.  
> **username_2**: 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.  
> **username_0**: @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.  
> **username_0**: @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?  
> **username_2**: @gigabytes No, $\forall$ is defined as the dual of $\exists$; it introduces a negation and quantifier alternation impacts the complexity.  
> **username_0**: @Sylvain oops, yes, of course. So the point is the number of negations that happen to contain some quantifiers. In other words: it is the negation of an existential that causes the blowup, not just any negation. This means that if I fix the quantifier alternation, then the number of negations inside the unquantified part do not cause other blowups.  

---

## 0 answers

