Going higher in the First-order Quantifier Alternation Hierarchy on Words

TL;DR

This paper studies the quantifier alternation hierarchy in first-order logic on finite words, providing decision procedures for membership in certain levels by solving related separation problems.

Contribution

It introduces decision algorithms for membership in the  and  levels of the hierarchy, advancing understanding of logical definability on words.

Findings

Decidable membership for  (boolean combinations with one alternation)

Decidable membership for  (formulas with two alternations starting with existential)

Separation problems are key to determining hierarchy levels

Abstract

We investigate the quantifier alternation hierarchy in first-order logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels $\mathcal{B}\Sigma_2$ (boolean combination of formulas having only 1 alternation) and $\Sigma_3$ (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.