On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

技术摘要：关于 Presburger 算术的变量有界非线性扩张

问题陈述
Presburger 算术（带有加法和序的整数的一阶理论）是可判定的。然而，通过非线性谓词（例如完全平方数集 $Z^2$ 或一般多项式像）对其进行的扩张，在一般情况下已知是不可判定的。这种不可判定性源于在这些理论中编码乘法的能力。尽管此类扩张的存在片段的可判定性仍是一个主要的未解决问题（例如关于完全平方数的 Büchi 猜想），但本文探讨了一条恢复可判定性的不同途径：限制变量的数量。

作者关注带有单变量多项式谓词族的 Presburger 算术的变量有界扩张。具体而言，他们考察了不同变量数量被常数 $k$ 限制的片段（记为 $FO_k$、$\exists FO_k$ 和 $SMT_k$）。核心挑战在于，即使对于单个变量（$k=1$），判定两个多项式谓词是否相交（例如 $f(u) = g(v)$）的可判定性，也是希尔伯特第十问题的一个极度受限的特例，而该问题在一般情况下尚未解决。

方法论
本文结合数论、代数几何和测度论技术，分析了这些变量有界片段中约束的解集。

1. 预处理与归约：判定过程始于将任意语句归约为涉及约束合取的可满足性问题。这些约束包括线性不等式（$x > c$）、模运算（$x \equiv_m c$）以及形式为 $R(ax+b)$或其否定$\neg R(ax+b)$ 的多项式谓词。作者利用中国剩余定理整合模约束，并通过案例分析消除有界区间，将问题归约为确定无界域上约束的可满足性。
2. 处理正约束：方法论的核心在于刻画正多项式约束系统的解集。
   • 对于固定幂次（例如 $Z_k = \{n^k\}$），作者利用超椭圆丢番图方程的结果。他们表明，两个此类约束的交集产生一个有限集（如果次数足够高），或者如果次数为 2，则产生一个由线性递推序列（LRS）参数化的集合。
   • 对于次数不超过 3 的一般多项式，分析依赖于所得代数曲线的亏格。涉及三次多项式的系统通常导致亏格为 1（椭圆曲线）或更高的曲线，根据 Siegel 定理或 Baker 界限，这些曲线仅有有限个整数点。涉及二次多项式的系统与佩尔方程相关，其解构成可逆的线性递推序列。
3. 处理负约束（密度论证）：一个关键见解是，当正约束的解集为无限集时，违反负约束（即满足被否定谓词的正向版本）的解集在原解集中具有相对密度零。
   • 对于多项式像，像的增长率是多项式级的，而“禁止”集（如果源于不同的多项式）通常以不同的速率增长或是稀疏的。
   • 在解集为线性递推序列的情况下，作者证明了“禁止”解的索引构成算术级数。这使得能够进行有效检查，以确定在排除零密度子集后是否仍有解存在。
4. 冗余与合并：作者定义了“冗余”和“相似”约束的概念。冗余约束可以被丢弃，而相似约束可以利用 $p$-进赋值和中国剩余定理合并为单个约束，从而在应用密度论证之前简化系统。

主要贡献与结果

本文确立了单变量理论（$k=1$）的两项主要可判定性结果：

1. 固定幂次的可判定性：理论 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$ 是可判定的。该结果依赖于超椭圆丢番图方程（$w^k - nz^j = N$）的可解性，以及此类方程组仅有有限个解或由线性递推序列参数化的解这一事实。
2. 低次多项式的可判定性：理论 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$ 是可判定的，其中每个 $R_i$ 对应于一个次数不超过 3 的整值多项式的像。该结果利用了相关代数曲线的低亏格（亏格 0 或 1）以及联立佩尔方程解的结构。

不可判定性结果
为了划定这些正面结果的边界，本文在变量限制被解除或特定谓词被组合时提供了不可判定性证明：

• 存在片段 $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$ 是不可判定的。这是通过编码 Büchi 猜想的否定来证明的，该编码允许使用有限数量的变量定义乘法。
• 利用 Jones 的通用丢番图方程和 Xiao 关于 Büchi 猜想的最新证明，作者确立了具有显著更高变量计数（例如带有 $Z^2$ 的 $SMT_{600}$ 或 $SMT_{2200}$）的理论是不可判定的。

意义
本文的意义在于确定了在 Presburger 算术的非线性扩张中可恢复可判定性的精确边界。通过将变量数量限制为一个，作者证明了来自丢番图几何的深刻结果（例如亏格 $\ge 2$ 的曲线上整数点的有限性）以及线性递推序列理论足以构建判定过程。

这项工作突显了一种二分法：虽然一般的非线性扩张是不可判定的，甚至带有两个变量和完全平方数的存在片段也是不可判定的，但对于广泛的谓词族，单变量情况仍然是可处理的。作者指出，将这些结果扩展到两个或三个变量会受到著名未解决问题的阻碍，例如完美欧拉砖的存在性（需要 3 个变量和 $Z^2$）以及三立方和问题（需要 2 个变量和 $Z^3$）。因此，本文为理解受变量界限约束的算术理论的计算复杂性提供了严格的框架。