哥德尔完备性定理

折叠 编辑本段 定理

上述词语"可证明的"意味着有着这个公式的形式演绎。这种形式演绎是步骤的有限列表，其中每个步骤要么涉及公理要么通过基本推理规则从前面的步骤获得。给定这样一种演绎，它的每个步骤的正确性可以在算法上检验(比如通过计算机或手工)。

一个公式被称为"逻辑上有效"的，如果它在这个公式的语言的所有模型中都为真。为了形式化地陈述哥德尔完备性定理，你必须定义这个上下文中词语"模型"的意义。这是模型论的基本定义。

在另一方面上，哥德尔完备性定理声称，在不需要额外的推理规则来证明所有逻辑上有效的公式的意义上，一阶谓词演算的推理规则是"完备的"。完备性的逆命题是"可靠性"。一阶谓词演算的确是可靠的，就是说，只有逻辑上有效的陈述可以在一阶逻辑中证明，这是可靠性定理断言的。

处理在不同的模型中什么为真的数理逻辑分支叫做模型论。研究在特定形式系统中什么为可以形式证明的分支叫做证明论。完备性定理建立了在这两个分支之间的基本联系。给出了在语义和语法之间的连接。但完备性定理不应当被误解为消除了在这两个概念之间的区别;事实上另一个著名的结果哥德尔不完备性定理，证实了对"在数学中什么是形式证明可以完成的"有着固有的限制。不完备定理的名字与另一种意义的"完备"有关，参见模型论。

更一般版本的哥德尔完备性定理成立。它声称对于任何一阶理论T和在这个理论中的任何句子S，有一个S的自T的形式演绎，当且仅当S被T的所有模型满足。这个更一般的定理被隐含使用，例如，在一个句子被证实可以用群论的公理证明的时候，通过考虑一个任意的群并证实这个句子被这个群所满足。完备性定理是一阶逻辑的中心性质，不在所有逻辑中成立。比如二阶逻辑就没有完备性定理。

完备性定理等价于超滤子引理，它是弱形式的选择公理，在不带有选择公理的Zermelo–Fraenkel集合论中有着等价的可证明性。

折叠 编辑本段 证明

对定理的最初证明的解释请参见哥德尔完备性定理的最初证明。

在现代逻辑课本中，哥德尔完备性定理通常使用Leon Henkin的证明而不是哥德尔最初的证明。

折叠 编辑本段 深入阅读

Kurt Gödel, "Über die Vollständigkeit des Logikkalküls", doctoral dissertation, University Of Vienna, 1929. This dissertation is the original source of the proof of the completeness theorem.

Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionen-kalküls", Monatshefte für Mathematik und Physik 37 (1930), 349-360. This article contains the same material as the doctoral dissertation, in a rewritten and shortened form. The proofs are more brief, the explanations more succinct, and the lengthy introduction has been omitted.

折叠 编辑本段 参考

Vilnis Detlovs and Karlis Podnieks, "Introduction to mathematical logic",