量词消去

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

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

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

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

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

并运用 ${\displaystyle \exists x.\bigvee _{j=1}^{m}\bigwedge _{i=1}^{n}L_{ij}}$ 等价于${\displaystyle \bigvee _{j=1}^{m}\exists x.\bigwedge _{i=1}^{n}L_{ij}}$ 此一性质。最后，为了消去全称量词 ${\displaystyle \forall x.F}$ ，其中${\displaystyle F}$ 不带量词，我们将${\displaystyle \lnot F}$ 写作析取范式，并运用${\displaystyle \forall x.F}$ 等价于${\displaystyle \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.