Going Higher in First-Order Quantifier Alternation Hierarchies on Words

TL;DR

This paper studies the complexity of quantifier alternation hierarchies in first-order logic on finite words, providing decision procedures for certain levels based on separation problems.

Contribution

It introduces decision methods for membership in specific levels of the quantifier alternation hierarchy using separation techniques.

Findings

Decidable membership for ;2 and 3 levels.

Separation problems are key to analyzing hierarchy levels.

Framework extends understanding of logical definability in formal languages.

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.