Going Higher in First-Order Quantifier Alternation Hierarchies on Words

Abstract

We investigate quantifier alternation hierarchies in first-order logic on finite words. Levels in these hierarchies are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language in the levels $\mathcal{B}{\Sigma }_2$ (finite boolean combinations of formulas having only one alternation) and ${\Sigma }_3$ (formulas having only two alternations and beginning with an existential block). Our proofs work by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.

arXiv admin note: text overlap with arXiv:1404.6832