On FO2 quantifier alternation over words
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.
Cite
@article{arxiv.0904.2894,
title = {On FO2 quantifier alternation over words},
author = {Manfred Kufleitner and Pascal Weil},
journal= {arXiv preprint arXiv:0904.2894},
year = {2015}
}