量詞消去- 维基百科，自由的百科全书

量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。

我們稱一個理論 T {\displaystyle T} T 可消去量詞，若且唯若對每個公式 ϕ {\displaystyle \phi } \phi ... 量詞消去 語言 監視 編輯 量詞消去是數理邏輯、模型論與計算機科學中的一類技巧。

我們稱一個理論 T {\displaystyleT} 可消去量詞，若且唯若對每個公式 ϕ {\displaystyle\phi} 皆存在另一個不帶量詞的公式 ψ {\displaystyle\psi} ，使得兩者在該理論中等價，即： T ⊨ ϕ ↔ ψ {\displaystyleT\models\phi\leftrightarrow\psi} 。

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

一個理論的量詞消去演算法係將一個帶量詞的公式轉成一個等價但不帶量詞的公式。

利用這個演算法，我們能將任一句子（不帶自由變量的公式）轉成一個不帶變量的句子，後者通常可藉簡單的計算判定。

因此，量詞消去演算法的存在性蘊含該理論的可判定性。

若干例子編輯 以下是若干可消去量詞的理論： Presburger算術 實封閉域 代數封閉域 無原子的布爾代數 項代數 稠密全序 特徵樹以及它們之間的許多組合，如帶Presburger算術的布爾代數等等。

量詞消去也可用以證明「合併」某些可判定理論可得到新的可判定理論，類似的建構包括有Feferman-Vaught定理及項冪。

基本想法編輯 如欲建構地證明一個理論可消去量詞，僅須處理一個存在量詞配上若干個文字合取的情形；換言之，即證明每個形如 ∃ x . ⋀ i = 1 n L i {\displaystyle\existsx.\bigwedge_{i=1}^{n}L_{i}}  （其中每個 L i {\displaystyleL_{i}}  都是文字） 的公式都在該理論中等價於一個無量詞的公式——誠然，假設已知如何對一串公式的合取消去量詞，則若 F {\displaystyleF}  是個公式，可將其寫作析取範式： ⊢ F ↔ ⋁ j = 1 m ⋀ i = 1 n L i j {\displaystyle\vdashF\leftrightarrow\bigvee_{j=1}^{m}\bigwedge_{i=1}^{n}L_{ij}}  並運用 ∃ x . ⋁ j = 1 m ⋀ i = 1 n L i j {\displaystyle\existsx.\bigvee_{j=1}^{m}\bigwedge_{i=1}^{n}L_{ij}}  等價於 ⋁ j = 1 m ∃ x . ⋀ i = 1 n L i j {\displaystyle\bigvee_{j=1}^{m}\existsx.\bigwedge_{i=1}^{n}L_{ij}}  此一性質。

最後，為了消去全稱量詞 ∀ x . F {\displaystyle\forallx.F}  ，其中 F {\displaystyleF}  不帶量詞，我們將 ¬ F {\displaystyle\lnotF}  寫作析取範式，並運用 ∀ x . F {\displaystyle\forallx.F}  等價於 ¬ ∃ x . ¬ F {\displaystyle\lnot\existsx.\lnotF}  一性質，遂證得原斷言。

文獻編輯 WilfridHodges."ModelTheory".CambridgeUniversityPress.1993. ViktorKuncakandMartinRinard."StructuralSubtypingofNon-RecursiveTypesisDecidable".InEighteenthAnnualIEEESymposiumonLogicinComputerScience,2003. 這是一篇關於數學的小作品。

你可以透過編輯或修訂擴充其內容。

閱論編 取自「https://zh.wikipedia.org/w/index.php?title=量詞消去&oldid=25452944」