稠密线性序的量词消去

形式陈述

语言固定为 $L=\{<\}$ ，等号作为逻辑符号，论域非空。无端点稠密线性序理论 $T_{\mathrm{DLO}}$ 由以下五类公理给出：

\begin{aligned} &\forall x\,\neg(x<x),\\ &\forall x\forall y\forall z\,((x<y\land y<z)\to x<z),\\ &\forall x\forall y\,(x<y\lor x=y\lor y<x),\\ &\forall x\forall y\,(x<y\to\exists z\,(x<z\land z<y)),\\ &\forall x\exists u\exists v\,(u<x\land x<v). \end{aligned}

前三条规定严格全序，第四条是稠密性，第五条排除最小元与最大元。 $(\mathbb Q,<)$ 和 $(\mathbb R,<)$ 都是模型。

量词消去定理。 $T_{\mathrm{DLO}}$ 有有效的量词消去。其中最主要的一步是： $\Gamma$ 不含 $x$ ，而所有 $l_i,u_j,e_k$ 都是不同于 $x$ 的参数变量时，

\exists x\left[ \Gamma\land\bigwedge_{i=1}^{m}l_i<x \land\bigwedge_{j=1}^{n}x<u_j \land\bigwedge_{k=1}^{r}x\ne e_k \right] \quad\longleftrightarrow\quad \Gamma\land\bigwedge_{i=1}^{m}\bigwedge_{j=1}^{n}l_i<u_j

在全部 DLO 模型、全部参数赋值下成立。这里“参数变量”可以获得相同的值，并不要求各个界彼此不同。空合取记为 $\top$ ；若任一侧无界，右边的交叉比较部分就是 $\top$ ，但 $\Gamma$ 仍须保留。

直觉

下界把见证向右推，上界把它向左推。有限多个界真正留下的是最大下界与最小上界之间的空隙：只要每个下界都小于每个上界，就有空隙；稠密性保证空隙里还能继续插点。因此排除有限多个特定元素不会耗尽可选位置。

“最大下界”和“最小上界”只是证明时从有限参数表中选出一个元素，没有往语言里添加 $\max$ 或 $\min$ 。最终公式用全部交叉比较表达条件，因而不用预先知道哪些参数恰好最大、最小，也适用于没有加法和除法的抽象序。

例子与边界

五个参数的一次完整消去

考虑

\Phi(a,b,c,d,e)= \exists x\,(a<x\land c<x\land x<b\land x<d\land x\ne e).

它的无量词结果是

\Psi(a,b,c,d,e)=a<b\land a<d\land c<b\land c<d.

任何见证都通过传递性给出这四条比较。反过来，四比较成立时，令 $L=\max\{a,c\}$ 、 $U=\min\{b,d\}$ ，便有 $L<U$ 。先在两者之间取 $s$ ，再分别在 $(L,s)$ 、 $(s,U)$ 中取 $p,q$ 。三个点 $p,s,q$ 两两不同，至少两个不等于 $e$ ，任选一个即可。输出中 $e$ 消失，表示这一个禁点不影响存在性，并非输入时忽略了它。

在有理数模型取 $a=0,c=1,b=3,d=2,e=3/2$ ，四比较为 $0<3,0<2,1<3,1<2$ ，全部成立。取 $x=5/4$ 后，原式逐项成为 $0<5/4$ 、 $1<5/4$ 、 $5/4<3$ 、 $5/4<2$ 、 $5/4\ne3/2$ 。若改成 $c=d=2$ ，输出中的 $c<d$ 为假；原式相应要求 $2<x<2$ ，确实无见证。数值用于指定赋值，语言本身没有这些数字常元。

四条交叉比较保证 $L<U$ ；在图示赋值下，有效区间为 $(1,2)$ 。叉号排除 $e=3/2$ ，实心点给出仍然可取的见证 $x=5/4$ ，两端空心点表示严格不等式不含端点。

析取与等式分支

现在消去

\exists x\,[a<x\land x<b\land x\ne c\land(x<d\lor x=e)].

将括号内析取分配成两支。第一支要求 $a<x$ 、 $x<b$ 、 $x<d$ 且避开 $c$ ，得到 $a<b\land a<d$ 。第二支的 $x=e$ 指定唯一候选，把它代入整个合取，得到 $a<e\land e<b\land e\ne c$ 。所以最后结果为

(a<b\land a<d) \ \lor\ (a<e\land e<b\land e\ne c).

等式分支没有自由选点的余地，因此这一支不能丢掉 $e\ne c$ 。例如 $a=0,b=3,d=0,e=2,c=1$ 时第一支失败，第二支由 $x=2$ 成立；再把 $c$ 改为 $2$ ，两支都失败。

两项假设分别在哪里失效

在 $(\mathbb Z,<)$ 中，取五参数例的 $a=c=0,b=d=1,e=2$ 。四条交叉比较都真，但没有整数 $0<x<1$ 。这精确指出双侧界的构造需要稠密性。

$([0,1],<)$ 有稠密性，却有端点。DLO 中单侧式 $\exists x(a<x)$ 消去为 $\top$ ；在这个区间模型取 $a=1$ 就为假。因此只有单侧界时仍然需要无端点条件，不能仅检查序是否稠密。

推论与应用

从任意无量词式到区间约束

先把否定推到原子式。三歧性给出

\neg(s<t)\leftrightarrow(s=t\lor t<s),\qquad s\ne t\leftrightarrow(s<t\lor t<s).

用这些规则和分配律得到有限析取范式，存在量词逐支处理。也可保留 $x\ne e$ ，直接使用本页带禁点的规则以减少分支。不含 $x$ 的合取记为 $\Gamma$ ； $x<x$ 或 $x\ne x$ 使整支为假， $x=x$ 则可删去。先用等号的对称性将 $y=x$ 改写为 $x=y$ ，将 $e\ne x$ 改写为 $x\ne e$ 。若有 $x=y$ 且 $y$ 是不同于 $x$ 的变量，就将 $y$ 代入整支，包括其他等式、不等式和禁点条件。

没有剩余等式时，只需证明形式陈述中的区间规则。必要性由传递性立即得到。充分性分三种情形：双侧界存在时，取最大下界 $L$ 和最小上界 $U$ ，交叉比较保证 $L<U$ ；只有下界时，无端点性给最大下界右侧的一个点，二者之间形成可用开区间，上界单侧同理；两侧都没有时，非空性先给一个元素，再由无端点性得到含它的开区间。不断用稠密性在可用区间插点，可取得 $r+1$ 个不同候选；至多 $r$ 个禁点不能将它们全部排除。整个构造同时说明如何在给定模型里恢复见证，而等价式本身只涉及原参数。

每一步处理有限公式，逐个消去最内层量词，便得到有效程序。析取范式展开可能大幅增加公式长度，因此有效并不意味着高效；这里证明的是终止与正确性，没有给出多项式时间保证。

完备、可判定与有理数的初等包含

在纯序语言 $\{<\}$ 中，没有常元和函数，所以没有闭项。加入逻辑常量 $\top,\bot$ 的约定后，无量词句只能是它们的布尔组合，可以机械化简为二者之一。任意句子经消去后因此在全部 DLO 模型中具有同一真值；再由 $(\mathbb Q,<)$ 确认理论有模型，得到理论完备性。有效消去与布尔化简也给出句子判定算法。这个论证使用了纯序语言；一般有量词消去的理论仍可能留下未被决定的无量词句。

包含映射 $j:(\mathbb Q,<)\hookrightarrow(\mathbb R,<)$ 保持有理数参数间的 $<$ 与 $=$ ，故保持任意无量词公式。对任意公式 $\varphi(\bar y)$ ，选择 DLO 上等价的无量词 $\psi(\bar y)$ ，则对 $\bar a\in\mathbb Q^n$ ，

\mathbb Q\models\varphi(\bar a) \iff\mathbb Q\models\psi(\bar a) \iff\mathbb R\models\psi(\bar a) \iff\mathbb R\models\varphi(\bar a).

这就验证了初等嵌入，比仅比较无参数句子更强。在扩充语言 $\{<,\cdot\}$ 中，带参数公式 $\exists x(x\cdot x=y)$ 在 $y=2$ 时会区分有理数与实数，因此纯序语言中的初等包含结论不能直接转移到扩充语言。

这里证明的理论完备性是“所有模型对每个句子一致”。上面的无量词保持论证也适用于任意两个 DLO 模型之间的嵌入，因而这个理论还具有模型完备性，即“模型间嵌入初等”。一阶逻辑完备性定理则说语义后承都有形式证明，是第三个不同命题。

量词消去还让一个无理割决定它在有理数参数上的全部公式真值，从而给出唯一的完全参数类型。这个类型的每个有限片段在有理数中可满足，整个类型却被有理数省略、在实数中实现；它展示初等包含如何保留每条一阶公式，同时允许扩张实现新的无限条件清单。

参考资料

James Worrell，Logic and Proof — Decidable Theories (I)，Hilary 2026，§2，Theorem 2，pp.2–3：DLO 公理、等式代入、上下界交叉比较及完备性、可判定性。
Philipp Schlicht，Introduction to Mathematical Logic，2022-02-01，§5.1，Example 5.1.4、Definition 5.1.5、Lemma 5.1.6，pp.65–66：否定原子的转换和真值常量约定。
Anand Pillay，Lecture Notes — Model Theory (Math 411)，2002，Example 1.39、Definition 2.2、Remark 2.3：DLO 的完备性与量词消去的参数语义。本文两组参数消去及数值核对为自行展开的算例。

形式陈述 ​

五个参数的一次完整消去 ​

析取与等式分支 ​

两项假设分别在哪里失效 ​

从任意无量词式到区间约束 ​

完备、可判定与有理数的初等包含 ​

反向链接