完全性定理

庫爾特·哥德爾（KurtGödel）在其1929年的博士論文（以及1930年發表的一篇文章的改寫版本）中給出的 哥德爾完備性定理的證明今天並不容易理解。它使用了不再使用的概念和形式以及常常是模糊的術語。下面給出的版本試圖忠實地代表證明中的所有步驟和所有重要的思想，同時用數學邏輯的現代語言重申證明。這個大綱不應該被認為是一個嚴格的定理證明。

1929年哥德爾首先證明了這一點。1947年，當萊昂·亨金（Leon Henkin）在他的博士學位上觀察的時候，它被簡化了。論證了證明的難點可以作為模型存在定理（1949年出版）。1953年，吉斯伯特·哈森賈格（Gisbert Hasenjaeger）簡化了亨金的證明。

哥德爾完全性定理最為熟知的形式聲稱 在一階謂詞演算中所有邏輯上有效的公式都是可以證明的。

上述詞語“可證明的”意味著有著這個公式的形式演繹。這種形式演繹是步驟的有限列表，其中每個步驟要麼涉及公理要麼通過基本推理規則從前面的步驟獲得。給定這樣一種演繹，它的每個步驟的正確性可以在演演算法上檢驗（比如通過計算機或手工）。

如果一個公式在這個公式的語言的所有模型中都為真，它就被稱為“邏輯上有效”的。為了形式的陳述哥德爾完全性定理，你必須定義這個上下文中詞語“模型”的意義。這是模型論的基本定義。

在另一個方向上，哥德爾完全性定理聲稱一階謂詞演算的推理規則是“完全的”，在不需要額外的推理規則來證明所有邏輯上有效的公式的意義上。完全性的逆命題是“可靠性”。一階謂詞演算的實情是可靠的，就是說，只有邏輯上有效的陳述可以在一階邏輯中證明，這是可靠性定理斷言的。

處理在不同的模型中什麼為真的數理邏輯分支叫做模型論。研究在特定形式系統中什麼為可以形式證明的分支叫做證明論。完全性定理建立了在這兩個分支之間的基本聯繫。給出了在語義和語形之間的連接。但完全性定理不應當被誤解為消除了在這兩個概念之間的區別；事實上另一個著名的結果哥德爾不完全性定理，證實了對“在數學中什麼是形式證明可以完成的”有著固有的限制。不完備定理的名聲與另一種意義的“完全”有關。

更一般版本的哥德爾完全性定理成立。它聲稱對於任何一階理論T和在這個理論中的任何句子S，有一個S的自T的形式演繹，當且僅當S被T的所有模型滿足。這個更一般的定理被隱含使用，例如，在一個句子被證實可以用群論的公理證明的時候，通過考慮一個任意的群並證實這個句子被這個群所滿足。完全性定理是一階邏輯的中心性質，不在所有邏輯中成立。比如二階邏輯就沒有完全性定理。

完全性定理等價於超濾子引理，它是弱形式的選擇公理，在不帶有選擇公理的策梅洛-弗蘭克爾集合論中有著等價的可證明性。

哥德爾對定理的原始證明是通過將問題簡化為特定語法形式的公式的特例，然後用特別的論證來處理這種形式。在現代的邏輯文本中，哥德爾的完備性定理通常用Henkin的證明來證明，而不是用哥德爾的原始證明。亨金的證明直接構造了任何一致的一階理論的術語模型。James Margetson利用Isabelle定理證明書開發了一個計算機化的形式證明。其他的證明也是已知的。

Henkin定理是最簡單的證明中最完整的定理的最直接的版本。

根據Henkin定理，完備性定理的證明如下： 是有效的，那麼 沒有模型。那麼，通過與Henkin的對立 是一個不一致的公式。但是，由一致性的定義，如果 是不一致的，那麼有可能建立一個證明 。

哥德爾不完備性定理是另一個著名的結果，表明數學中的形式證明可以實現的內在固有的局限性。對於不完備性定理名指的是另一種意義完整。

它表明，在任何一致的、有效的理論T含有皮亞諾算術（PA），式表達的一致性T不能證明內T。

對這個結果應用完備性定理給出了T模型的存在，其中公式是假的。這樣的模型（恰恰是它所包含的“自然數”集合）必然是非標準的，因為它包含了T的矛盾證明的代碼數。但從外部看，T是一致的。因此，這個T 的矛盾證明的代碼編號必須是非標準編號。

事實上，任何包含PA的理論模型都是通過系統建構的算術模型存在定理而得到的，它總是不規範的，用非等價的可證析謂詞和非等價的方法來解釋自己的構造，所以這種構造是非遞歸的（因為遞歸定義是明確的）。