The FO^2 alternation hierarchy is decidable

TL;DR

This paper proves that each level of the FO^2[<] quantifier alternation hierarchy over finite words is decidable, connecting it with various algebraic structures and introducing condensed rankers as a key tool.

Contribution

It establishes the decidability of all levels of the FO^2[<] hierarchy by relating them to decidable varieties of finite monoids and introduces condensed rankers for analysis.

Findings

Each hierarchy level is decidable.

Multiple algebraic characterizations of hierarchy levels.

Introduction of condensed rankers as a new combinatorial tool.

Abstract

We consider the two-variable fragment FO^2[<] of first-order logic over finite words. Numerous characterizations of this class are known. Th\'erien and Wilke have shown that it is decidable whether a given regular language is definable in FO^2[<]. From a practical point of view, as shown by Weis, FO^2[<] is interesting since its satisfiability problem is in NP. Restricting the number of quantifier alternations yields an infinite hierarchy inside the class of FO^2[<]-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 FO^2[<]-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, Th\'erien, and Vollmer.