We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the ``biregular graph method''. In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

翻译：本文研究了在二变量逻辑中扩展量化器的方法，该量化器指出公式成立的元素数量应属于给定的终极周期集合。我们证明该逻辑的可满足性及有限可满足性均为可判定的，并进一步表明任何语句的谱均可通过普雷斯伯格算术进行定义。在此过程中，我们对“双正则图方法”进行了若干改进。该方法将关于二变量逻辑的可判定性问题，归约为与分区图关联的整数向量的普雷斯伯格可定义性问题，其中分区中的节点需满足关于其入度和出度的特定约束。