量詞消去

量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論$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.