On FO2 quantifier alternation over words

TL;DR

This paper proves that each level of the quantifier alternation hierarchy in FO^2[<] is a language variety and introduces a decidable hierarchy using condensed rankers, enabling effective quantifier complexity analysis.

Contribution

It establishes the hierarchy as a variety of languages and introduces a decidable hierarchy using condensed rankers, linking it with the quantifier alternation hierarchy in FO^2[<].

Findings

Each level of the hierarchy is a language variety.

Decidable hierarchy of varieties is constructed using condensed rankers.

Effective computation of quantifier alternation bounds for formulas.

Abstract

We show that each level of the quantifier alternation hierarchy within FO^2[<] -- the 2-variable fragment of the first order logic of order on words -- is a variety of languages. We then use the notion of condensed rankers, a refinement of the rankers defined by Weis and Immerman, to produce a decidable hierarchy of varieties which is interwoven with the quantifier alternation hierarchy -- and conjecturally equal to it. It follows that the latter hierarchy is decidable within one unit: given a formula alpha in FO^2[<], one can effectively compute an integer m such that alpha is equivalent to a formula with at most m+1 alternating blocks of quantifiers, but not to a formula with only m-1 blocks. This is a much more precise result than what is known about the quantifier alternation hierarchy within FO[<], where no decidability result is known beyond the very first levels.