Nesting negations in FO2 over infinite words

TL;DR

This paper characterizes the hierarchy of two-variable first-order logic over infinite words based on nested negations, providing effective algebraic and topological descriptions for each level, extending finite word results.

Contribution

It offers a comprehensive, effective characterization of each level of the nested negation hierarchy in FO2 over infinite words, using algebraic and topological methods.

Findings

Effective algebraic and topological characterizations for all hierarchy levels.

Lower levels characterized by combined algebraic and topological properties.

Higher levels characterized solely by algebraic properties.

Abstract

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.