FCT

We consider two-variable first-order logic $\mathop{\mathrm{FO}}^2$ over infinite words. Restricting the number of nested negations defines an infinite hierarchy; its levels are often called the half-levels of the $\mathop{\mathrm{FO}}^2$ quantifier alternation hierarchy. The full levels are the Boolean closures of the half-levels. For every level of this hierarchy, we give an effective characterization. For the lower levels, this characterization is a combination of an algebraic and a topological property. For the higher levels, algebraic properties turn out to be sufficient. Within two-variable first-order logic, each algebraic property is a single ordered identity of omega-terms. The topological properties are the same as for the lower half-levels of the quantifier alternation hierarchy without the two-variable restriction (i.e., the Cantor topology and the alphabetic topology). Our result generalizes the corresponding results for finite words.
This is joint work with Aaron Boussidan and Viktor Henriksson.