带有一元未解释谓词的Presburger算术全称片段是不可判定的

自然数上加法的一阶理论，即Presburger算术，在双指数时间内是可判定的。在该语言中加入一个未解释的一元谓词会导致理论不可判定。我们锐化了已知可判定与不可判定之间的边界，证明了该扩展理论的纯全称片段已经是不可判定的。我们的证明基于将双计数器机的停机问题归约到不使用存在量词的Presburger算术扩展语言中句子的不可满足性。另一方面，我们论证了单个 $\forall\exists$ 量词交替会将该扩展语言的可满足句子集合转变为 $\Sigma^1_1$-完全集。上述部分结果可以转移到有序实数上的线性算术领域。这涉及纯全称片段的不可判定性，以及具有至少一次量词交替的句子的 $\Sigma^1_1$-困难性。最后，我们讨论了这些结果与验证的相关性。特别地，我们推导出了分离逻辑的量词片段、数组理论，以及未解释函数上的等词理论与受限形式整数算术组合的不可判定性结果。在某些情况下，我们的结果甚至意味着不存在可靠且完备的演绎演算。