Presburger 算术的子类与弱 EXP 层级

本文证明，对于任意固定的 $i>0$，Presburger 算术的 $\Sigma_{i+1}$ 片段，即其限制为以存在量词开头的 $i+1$ 次量词交替的部分，对于 $\mathsf{\Sigma}^{\mathsf{EXP}}_{i}$（弱 EXP 层级的第 $i$ 层，一个位于 $\mathsf{NEXP}$ 与 $\mathsf{EXPSPACE}$ 之间且类似于多项式时间层级的类比）是完备的。这一结果完善了 Presburger 算术的计算复杂性图景，该研究路线可追溯至 Fischer & Rabin 于 1974 年的开创性工作。此外，我们应用了在证明下界时开发的一些技术，以确立 Presburger 算术 $\Sigma_1$ 片段中可定义的自然数集的界限：给定一个 $\Sigma_1$ 公式 $\Phi(x)$，证明其非负解集是一个最终周期集，其周期至多为双指数级，且该界限是紧致的。