量詞消去

维基百科,自由的百科全书
跳转至: 导航搜索

量詞消去數理邏輯模型論計算機科學中的一類技巧。我們稱一個理論T可消去量詞,若且唯若對每個公式\phi皆存在另一個不帶量詞的公式\psi,使得兩者在該理論中等價,即:T \models \phi \leftrightarrow \psi

量詞消去在模型論有多種刻劃;即使一個理論可消去量詞,也不保證存在一個相應的演算法

一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。利用這個演算法,我們能將任一句子(不帶自由變量的公式)轉成一個不帶變量的句子,後者通常可藉簡單的計算判定。因此,量詞消去演算法的存在性蘊含該理論的可判定性。

若干例子[编辑]

以下是若干可消去量詞的理論:

以及它們之間的許多組合,如帶 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.