FO2 quantifier alternation over infinite words

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.

Date and Venue

Start Date
Online Zoom meeting
End Date


Manfred Kufleitner

Speaker's Institution

University of Stuttgart



Semigroups, Automata and Languages