论文标题
fo2中的嵌套否定无限单词
Nesting negations in FO2 over infinite words
论文作者
论文摘要
我们考虑在无限单词上考虑两变量的一阶逻辑fo2。限制嵌套否定的数量定义了无限的层次结构；它的水平通常称为FO2量词交替层次结构的半级别。对于这个层次结构的每个层次，我们都提供了有效的表征。对于较低的级别，这种特征是代数和拓扑特性的组合。对于较高的级别，代数特性就足够了。在两变量的一阶逻辑中，每个代数属性都是Omega-Terms的单个有序标识。拓扑特性与量化器交替层次结构的下半级相同，而没有两变量的限制（即cantor拓扑结构和字母拓扑）。 我们的结果概括了有限单词的相应结果。该证明使用新颖的技术，并基于对有序单体的Mal'Cev产品的改进。
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.
