2017/07/15 by Place, Thomas, Zeitoun, Marc
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1707.05696
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 BΣ2 (finite boolean combinations of formulas having only one alternation) and Σ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.