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.

翻译：我们认为,在无限的单词上,有两种可变第一阶逻辑FO2 。限制嵌入式否定的数量可以定义无限的等级;它的等级通常被称为FO2量化的交替等级的半等级。对于这个等级的每个等级,我们给出一个有效的定性。对于较低等级,这种定性是代数和地形属性的组合。对于较高等级,代数属性就足够了。在两个可变第一阶逻辑中,每个代数属性是omega-terms的单一定序特性。其地形特性与量化的变换等级的较低半等级相同,没有两种可变的限制(如Cantor表层学和字母表层学)。我们的结果概括了限定词的相应结果。在两种可变第一阶逻辑中,证据使用新技术,并以对订购单体的 Mal'cev 产品进行精细化为基础。