2020/12/02 by Viktor Henriksson, Henriksson, Viktor, Manfred Kufleitner +1
Computer Science · #03D05 #68Q45 #68Q70 #Advanced Algebra and Logic #F.4.1 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2012.01309
openalex publication_date 2020/12/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We consider two-variable first-order logic FO2 over infinite words. Restricting the number of nested negations defines an infinite hierarchy; its levels are often called the half-levels of the FO2 quantifier alternation hierarchy. 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 result for finite words. The proof uses novel techniques and is based on a refinement of Mal'cev products for ordered monoids.