量词消去

量词消去是数理逻辑、模型论与计算机科学中的一类技巧。我们称一个理论$T$可消去量词，当且仅当对每个公式$\phi$皆存在另一个不带量词的公式$\psi$，使得两者在该理论中等价，即：$T\models \phi \leftrightarrow \psi$。

量词消去在模型论有多种刻划；即使一个理论可消去量词，也不保证存在一个相应的算法。

一个理论的量词消去算法系将一个带量词的公式转成一个等价但不带量词的公式。利用这个算法，我们能将任一句子（不带自由变量的公式）转成一个不带变量的句子，后者通常可藉简单的计算判定。因此，量词消去算法的存在性蕴含该理论的可判定性。

若干例子

以下是若干可消去量词的理论：

• Presburger 算术
• 实封闭域
• 代数封闭域
• 无原子的布尔代数
• 项代数
• 稠密全序
• 特征树

以及它们之间的许多组合，如带 Presburger 算术的布尔代数等等。量词消去也可用以证明“合并”某些可判定理论可得到新的可判定理论，类似的建构包括有 Feferman-Vaught 定理及项幂。

基本想法

如欲建构地证明一个理论可消去量词，仅须处理一个存在量词配上若干个文字合取的情形；换言之，即证明每个形如$\exists x.\bigwedge _{i=1}^{n}L_{i}$ （其中每个$L_{i}$都是文字） 的公式都在该理论中等价于一个无量词的公式——诚然，假设已知如何对一串公式的合取消去量词，则若$F$是个公式，可将其写作析取范式：

$\vdash F\leftrightarrow \bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}$

并运用 $\exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}$等价于$\bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}$此一性质。最后，为了消去全称量词 $\forall x.F$，其中$F$不带量词，我们将$\lnot F$写作析取范式，并运用$\forall x.F$等价于$\lnot \exists x.\lnot F$一性质，遂证得原断言。

文献

• Wilfrid Hodges. "Model Theory". Cambridge University Press. 1993.
• Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003.