量詞消去方法

量詞消去方法(method of elimination of quan-tifiers)研究判定問題的一種方法一般用它來證明一些數學理論的可判定性，也是證明數學理論可判定性的最早的方法。

基本介紹

• 中文名：量詞消去方法
• 外文名：method of elimination of quan-tifiers
• 領域：數學

簡介

量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。我們稱一個理論可消去量詞，若且唯若對每個公式皆存在另一個不帶量詞的公式，使得兩者在該理論中等價，即：。

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

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

若干例子

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

• Presburger 算術
  
• 實封閉域
  
• 代數封閉域
  
• 無原子的布爾代數
  
• 項代數
  
• 稠密全序
  
• 特徵樹
  

以及它們之間的許多組合，如帶 Presburger 算術的布爾代數等等。量詞消去也可用以證明“合併”某些可判定理論可得到新的可判定理論，類似的建構包括有 Feferman-Vaught 定理及項冪。

基本想法

如欲建構地證明一個理論可消去量詞，僅須處理一個存在量詞配上若干個文字合取的情形；換言之，即證明每個形如（其中每個都是文字） 的公式都在該理論中等價於一個無量詞的公式——誠然，假設已知如何對一串公式的合取消去量詞，則若是個公式，可將其寫作析取範式：

並運用等價於此一性質。最後，為了消去全稱量詞，其中不帶量詞，我們將寫作析取範式，並運用等價於一性質，遂證得原斷言。