Presburger 算术

整数中的空隙不能用稠密性填补：$0<x<1$ 没有整数解。加法约束还会留下奇偶性等周期条件。因此，见证必须同时满足两类要求：落在允许区间里，且落在允许的余数类里。

核心观察是：如果所有周期条件以 $M$ 为共同周期，那么从某个下界开始，只须检查连续 $M$ 个整数。任何更远的见证都可减去若干个 $M$，退回这段区间；余数条件不变，已有上界也不会被破坏。系数统一先把 $2x$、$3x$ 之类的约束改写到同一个新变量上，再用额外的整除条件记住这个新变量确实来自原来的整数 $x$。

一个模六算例 ​

在 $\mathbb{Z}$ 中消去

令 $z=2x$。必须同时保留 $2\mid z$ 与 $6\mid z-2$；后者已经蕴含前者，因此约束化为

不小于 $y$ 的第一个合格余数代表是 $y+\delta$，其中 $\delta$ 是 $2-y$ 模六的最小非负余数。它落在区间中恰好当 $\delta \le 3$：

所以无量词结果为

例如 $y=3$ 给出区间 $[3,6]$，其中没有模六余二的数；$y=5$ 则可取 $z=8$，恢复 $x=4$。当参数 $y\ge 0$ 时，这个算例的见证也自动非负，因此同一结果适用于自然数版本。

扩充语言与乘法的边界 ​

原来的加法、序语言没有量词消去。公式 $\mathrm{\exists }x(y=x+x)$ 定义偶数，而一元无量词线性等式、不等式的有限布尔组合，在足够大的正整数上必定真值恒定：每个线性原子最终恒真或恒假。偶数集合却永远交替。加入固定模数的同余谓词，才使这种投影结果能够无量词地表达。

即使允许所有固定模数，变量乘法仍不可定义。消去后的每个一元公式只含有限多个线性不等式与同余条件；在足够大的数上，不等式真值固定，同余部分以各模数的公倍数为周期。因此每个一元可定义集合最终周期。若乘法可定义，平方数集合也可定义；但给定正周期 $p$，选足够大的 $n$ 使 $n^2$ 越过周期起点且 $2n+1>p$，则 $n^2+p$ 严格介于 $n^2$ 与 $(n+1{)}^2$ 之间，违背周期性。这给出了表达力的具体界限。

统一系数并保留参数条件 ​

先把存在量词内的无量词公式写成有限析取范式。整数上的严格不等式可改为非严格界，例如 $s<t$ 等价于 $s\le t-1$；否定不等式反向并移动一单位；等式拆成两个非严格不等式，不等式 $s\ne t$ 拆成 $s<t\vee t<s$。整除原子及其否定可以原样保留。因此，只需处理一支由线性非严格不等式和整除文字组成的合取。不含待消变量 $x$ 的全部条件记为 $\mathrm{\Gamma }(\overline{y})$，随后始终保留。

设这一支中 $x$ 的非零系数绝对值的最小公倍数为 $L$；若没有非零系数，取 $L=1$。对每个系数 $a\ne 0$，令正整数 $d=L/|a|$。不等式两边同乘 $d$ 不改变真值。整除文字则使用

其否定也同样等价。这里模数和整个表达式必须同时乘 $d$；只缩放其中一方会改变解集。

现在置 $z=Lx$，并加入 $D_L(z)$，才能保证每个候选 $z$ 可恢复为整数 $x=z/L$。即使原公式只有不等式，这一项也不能漏掉。缩放后 $z$ 的系数只有 $1$ 或 $-1$，所以不等式可整理成下界 $a_i(\overline{y})\le z$ 或上界 $z\le b_j(\overline{y})$。把全部整除文字连同 $D_L(z)$ 合为 $R(z,\overline{y})$，得到

$a_i,b_j$ 都是整数线性参数项；这里没有引入取整函数。若 $M$ 是 $R$ 中各正模数的最小公倍数，包括 $L$，则

正整除文字和否定整除文字都具有这个周期。$M$ 由公式的常数系数决定，不依赖参数赋值。

有下界时只查一个周期 ​

先假设已有一个最大的下界 $a$。对固定参数，

右向左直接取 $z=a+r$。左向右，给定见证 $z$，对非负整数 $z-a$ 作带余除法：$z-a=qM+r$，其中 $q\ge 0$、$0\le r<M$。于是 $a\le a+r\le z$，故新候选仍满足所有上界；又因它与原见证相差 $qM$，周期条件也保持。即使没有上界，这个证明仍然成立。

算法事先不知道哪个参数项最大，因此要枚举下界的索引。$k>0$ 时，整支准确化为

每个分支内的全部比较 $a_{\ell }\le a_i$ 确保被选项确为最大下界。若多个项并列最大，可以有多支成立；析取不要求分支互斥。

无下界时向负方向选见证 ​

$k=0$ 时，整支的结果是

必要性来自对任一整数见证取模 $M$ 的余数。反过来，若 $R(r,\overline{y})$ 成立，选足够大的非负整数 $q$，让 $z=r-qM$ 同时不超过有限多个上界 $b_j$；周期性保持 $R$。没有上界时可直接取 $q=0$。这一分支依赖整数向负方向无界，不能照搬到自然数论域。

从单步消去到判定与自然数版本 ​

对有限析取范式的每支应用上述规则，再取析取，就消去一个存在量词。所有索引与余数枚举都有限；输出仍由线性不等式、固定模数整除条件及布尔联结词组成。于是可以沿公式语法树由内向外继续，遇到全称量词用 $\mathrm{\forall }x\theta \equiv \mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\theta$。每步消去一个量词，整个过程终止；闭公式最终只剩可直接计算的整数比较与整除检验。这证明可判定性，没有给出多项式时间保证，析取范式展开本身就可能很大。

自然数公式先翻译到整数中：将 $\mathrm{\exists }x\theta$ 改成 $\mathrm{\exists }x(0\le x\wedge \theta )$，将 $\mathrm{\forall }x\theta$ 改成 $\mathrm{\forall }x(0\le x\to \theta )$，递归处理每个量词，且只考察非负的自由参数赋值。新增的下界阻止算法用负数充当自然数见证。消去后，把含负系数的项移到等号或不等号另一侧，把 $D_m(u-v)$ 写成二元同余 $u\equiv v(\mathrm{mod}m)$，便回到扩充同余谓词的自然数语言。

这使含量词的线性整数可满足性、计数下标边界以及固定步长约束成为可计算的问题。它也说明Peano 算术公理库皮亚诺算术Peano arithmetic · PA用一阶语言公理化自然数的零、后继、加法、乘法与归纳模式的形式理论。与加法算术之间的差别不能仅用“都有归纳”概括：前者有变量乘法，归纳实例也允许使用乘法公式。Presburger 算术不具备第一不完备定理公理库哥德尔第一不完备定理Gödel's first incompleteness theorem足够强、有效公理化且一致的算术理论存在既不可证也不可否证的句子。所要求的算术表达能力，因而其有效公理化与完备性并不冲突。完备、可判定仍不意味着模型唯一；一阶紧致性照样允许非标准模型。