We consider a first-order logic for the integers with addition. This logic extends classical first-order logic by modulo-counting, threshold-counting and exact-counting quantifiers, all applied to tuples of variables (here, residues are given as terms while moduli and thresholds are given explicitly). Our main result shows that satisfaction for this logic is decidable in two-fold exponential space. If only threshold- and exact-counting quantifiers are allowed, we prove an upper bound of alternating two-fold exponential time with linearly many alternations. This latter result almost matches Berman's exact complexity of first-order logic without counting quantifiers. To obtain these results, we first translate threshold- and exact-counting quantifiers into classical first-order logic in polynomial time (which already proves the second result). To handle the remaining modulo-counting quantifiers for tuples, we first reduce them in doubly exponential time to modulo-counting quantifiers for single elements. For these quantifiers, we provide a quantifier elimination procedure similar to Reddy and Loveland's procedure for first-order logic and analyse the growth of coefficients, constants, and moduli appearing in this process. The bounds obtained this way allow to restrict quantification in the original formula to integers of bounded size which then implies the first result mentioned above. Our logic is incomparable with the logic considered by Chistikov et al. in 2022. They allow more general counting operations in quantifiers, but only unary quantifiers. The move from unary to non-unary quantifiers is non-trivial, since, e.g., the non-unary version of the H\"artig quantifier results in an undecidable theory.

翻译：我们考虑一种带加法的一阶整数逻辑。该逻辑通过模计数、阈值计数和精确计数量词扩展了经典一阶逻辑，这些量词均应用于变量元组（此处，余数以项的形式给出，而模数和阈值则显式给出）。我们的主要结果表明，该逻辑的可满足性可在双重指数空间内判定。若仅允许阈值计数和精确计数量词，我们证明其具有交替双重指数时间上界（线性多次交替）。后一结果几乎匹配了Berman关于无计数量词一阶逻辑的精确复杂性。为获得这些结果，我们首先在多项式时间内将阈值计数和精确计数量词翻译为经典一阶逻辑（这已证明第二个结果）。为处理剩余的元组模计数量词，我们首先在双重指数时间内将其归约为单个元素的模计数量词。针对这些量词，我们提出了一种类似于Reddy和Loveland一阶逻辑程序的量词消去过程，并分析了该过程中系数、常数和模数的增长。通过这种方式获得的界允许将原始公式中的量化限制在有界大小的整数上，从而得出上述第一个结果。我们的逻辑与Chistikov等人2022年研究的逻辑不可比较：他们允许量词中更一般的计数操作，但仅限于一元量词。从一元量词到非一元量词的迁移并非平凡，例如，Härtig量词的非一元版本会导致不可判定理论。