The FO2 alternation hierarchy is decidable

Abstract

We consider the two-variable fragment FO2[<] of first-order
logic over finite words. Numerous characterizations of this class are
known. Therien and Wilke have shown that it is decidable whether a
given regular language is definable in FO2[<].  From a practical
point of view, as shown by Weis, FO2[<] is interesting since its
satisfiability problem is in NP. Restricting the number of
quantifier alternations yields an infinite hierarchy inside the class
of FO2[<]-definable languages. We show that each level of this
hierarchy is decidable.  For this purpose, we relate each level of the
hierarchy with a decidable variety of finite monoids.

Our result implies that there are many different ways of climbing up
the FO2[<]-quantifier alternation hierarchy: deterministic and
co-deterministic products, Mal'cev products with definite and reverse
definite semigroups, iterated block products with J-trivial
monoids, and some inductively defined omega-term identities. A
combinatorial tool in the process of ascension is that of condensed
rankers, a refinement of the rankers of Weis and Immerman and the
turtle programs of Schwentick, Therien, and Vollmer.