量词消去

存在量词把“选哪一个见证”隐藏起来，只留下“是否有合适见证”。例如 $\mathrm{\exists }x(a<x\wedge x<b)$ 问两个参数之间能否插入一个元素。在无端点稠密线性序中，答案恰好由 $a<b$ 决定；在整数序中，$0<1$ 却没有中间整数。能否消去，取决于理论提供了怎样的见证保证。

把带参数公式看成一个集合的定义，$\mathrm{\exists }x\theta (x,\overline{y})$ 就是在问：给定 $\overline{y}$ 后，是否有一个 $x$ 与它共同满足约束。消去量词将这个投影后的集合重新写成无量词条件。参数仍然是输入，只是不必再遍历结构中的全部候选见证。

从一个存在量词推广到全部公式 ​

证明量词消去时，只需解决

其中每个 ${\ell }_i$ 是原子公式或原子公式的否定。理由是对公式构造作归纳：布尔联结词直接作用于已经消去的子公式；处理 $\mathrm{\exists }x\theta$ 时，先把无量词的 $\theta$ 化成析取范式，再使用

每支 $C_j$ 都是上述有限合取，分别消去后再取析取即可。全称量词用 $\mathrm{\forall }x\theta \equiv \mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }\theta$ 处理。按语法树由内向外操作便覆盖任意嵌套，无须先改变所有量词的排列。

参数条件必须一路保留。若某支是 $\mathrm{\Gamma }(\overline{y})\wedge \mathrm{\Delta }(x,\overline{y})$，即使已经证明 $\mathrm{\exists }x\mathrm{\Delta }$ 总真，整支也只化成 $\mathrm{\Gamma }$。例如在稠密无端点序中，$\mathrm{\exists }x(a<b\wedge c<x)$ 等价于 $a<b$，而非 $\mathrm{\top }$。稠密线性序的消去公理库稠密线性序的量词消去Quantifier elimination for dense linear orders · DLO 量词消去在无端点稠密线性序中，以所有下界小于所有上界消去存在量词，并构造避开有限禁点的见证。给出这套归纳接口的完整实现，包括等式代入和避开有限禁点。

量词消去不自动决定全部句子 ​

取语言 $\{=,c,d\}$，对每个 $n\ge 1$ 加入“存在 $n$ 个两两不同元素”的公理；所得理论只要求论域无限，不规定常元 $c,d$ 是否相等。它有量词消去：等式约束通过代入消去；若 $x$ 只需避开有限多个项，无限论域保证可选；剩下的参数约束照常保留。然而 $c=d$ 在某些模型为真，在另一些模型为假，所以理论不完备。这是一个无量词句本身就还未被理论决定的例子。

即使已有有效消去，也要能决定消去后无量词句的后承，才能决定一般句子的后承。尤其对不完备理论，不能把“检查每个原子句是否被蕴涵”直接当作任意布尔组合的判定器：理论不蕴涵 $c=d$，也不蕴涵 $c\ne d$，却蕴涵它们的析取。

若 $T$ 可满足、有量词消去，且决定每个无量词句，那么 $T$ 完备：把任意句子换成无量词句，再读取其固定真值。若消去过程有效，并且无量词句的 $T$-后承可判定，则一般句子的 $T$-后承也可判定。完备性说明模型之间意见一致；可判定性说明存在终止的计算过程，这两个结论使用的条件不同。

量词消去还给出检查初等嵌入公理库初等嵌入Elementary embedding保持所有一阶公式真值的结构间单射。的捷径。设 $\mathcal{M},\mathcal{N}\models T$，且 $j:\mathcal{M}\to \mathcal{N}$ 是结构嵌入。嵌入保持原子公式及其否定，因而保持无量词公式；任意 $\phi$ 又在两个模型中都等价于同一个无量词 $\psi$，于是 $j$ 保持 $\phi$ 的真值。这说明有量词消去的理论是模型完备的，即其模型之间的每个嵌入都初等。这里的“模型完备”也不等于“理论决定全部句子”。