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量词的非一元版本会导致不可判定理论。