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