形式陈述
固定一阶语言 和一个一阶理论公理库一阶理论First-order theory同一一阶语言中一组句子及其模型类所构成的理论。 。称 有量词消去，若对每个 -公式 ，存在无量词的 -公式 ，使
这是一项相对于 的逻辑等价公理库逻辑等价Logical equivalence两个公式在指定语义类的每个结构与赋值下具有相同真值。要求。也就是说，对每个 和每个参数元组 ，两式在赋值 下同真同假。输出不能引入新的自由参数；有些原参数可以因公式化简而不再出现。若要求自由变量集合在字面上完全相同，可补入 这样的恒真合取。
本页允许逻辑真值常量 ，分别总真、总假，以便没有自由变量时也能写出无量词结果。这一点在没有任何常元符号的语言中尤其必要：没有闭项，就未必能拿某个闭项等式充当恒真句。
定义只断言等价式存在。有效量词消去程序进一步要求一个算法：输入公式后有限步输出这样的无量词式。两者都依赖指定的语言和理论；扩充语言后得到的无量词表达式，不能直接算作原语言中的消去结果。
直觉
存在量词把“选哪一个见证”隐藏起来，只留下“是否有合适见证”。例如 问两个参数之间能否插入一个元素。在无端点稠密线性序中，答案恰好由 决定；在整数序中， 却没有中间整数。能否消去，取决于理论提供了怎样的见证保证。
把带参数公式看成一个集合的定义， 就是在问：给定 后，是否有一个 与它共同满足约束。消去量词将这个投影后的集合重新写成无量词条件。参数仍然是输入，只是不必再遍历结构中的全部候选见证。
例子与边界
从一个存在量词推广到全部公式
证明量词消去时，只需解决
其中每个 是原子公式或原子公式的否定。理由是对公式构造作归纳：布尔联结词直接作用于已经消去的子公式；处理 时，先把无量词的 化成析取范式公理库析取范式Disjunctive normal form · DNF由文字的合取形成项，再对这些项取析取得到的命题公式形状。，再使用
每支 都是上述有限合取，分别消去后再取析取即可。全称量词用 处理。按语法树由内向外操作便覆盖任意嵌套，无须先改变所有量词的排列。
参数条件必须一路保留。若某支是 ，即使已经证明 总真，整支也只化成 。例如在稠密无端点序中， 等价于 ，而非 。稠密线性序的消去公理库稠密线性序的量词消去Quantifier elimination for dense linear orders · DLO 量词消去在无端点稠密线性序中，以所有下界小于所有上界消去存在量词，并构造避开有限禁点的见证。给出这套归纳接口的完整实现，包括等式代入和避开有限禁点。
Presburger 算术公理库Presburger 算术Presburger arithmetic · 加法算术 · 线性整数算术在加法与序的整数约束中，通过系数统一和有限余数检验消去量词，并判定自然数加法算术。给出离散情形的另一种实现：整数见证须满足线性上下界和固定模数的余数条件，统一系数后只需在最大下界之后检查一个共同周期。原来的加法、序语言不能无量词地定义偶数；加入同余谓词后才有这里的消去。因此“整数也能消去”同时改变了见证构造方法和所用语言。
量词消去不自动决定全部句子
取语言 ，对每个 加入“存在 个两两不同元素”的公理；所得理论只要求论域无限，不规定常元 是否相等。它有量词消去：等式约束通过代入消去；若 只需避开有限多个项，无限论域保证可选；剩下的参数约束照常保留。然而 在某些模型为真，在另一些模型为假，所以理论不完备。这是一个无量词句本身就还未被理论决定的例子。
即使已有有效消去，也要能决定消去后无量词句的后承，才能决定一般句子的后承。尤其对不完备理论，不能把“检查每个原子句是否被蕴涵”直接当作任意布尔组合的判定器：理论不蕴涵 ，也不蕴涵 ，却蕴涵它们的析取。
推论与应用
若 可满足、有量词消去，且决定每个无量词句，那么 完备：把任意句子换成无量词句，再读取其固定真值。若消去过程有效，并且无量词句的 -后承可判定，则一般句子的 -后承也可判定。完备性说明模型之间意见一致；可判定性说明存在终止的计算过程，这两个结论使用的条件不同。
量词消去还给出检查初等嵌入公理库初等嵌入Elementary embedding保持所有一阶公式真值的结构间单射。的捷径。设 ，且 是结构嵌入。嵌入保持原子公式及其否定，因而保持无量词公式；任意 又在两个模型中都等价于同一个无量词 ，于是 保持 的真值。这说明有量词消去的理论是模型完备的，即其模型之间的每个嵌入都初等。这里的“模型完备”也不等于“理论决定全部句子”。
参考资料
