完全性定理(completeness theorem)，也称哥德尔完全性定理,是数理逻辑中重要的定理，是建立之间的对应语义真理和句法可证明在一阶逻辑，在1929年由库尔特·哥德尔首先证明。完备性定理说，如果一个公式在逻辑上是有效的，那么这个公式就有一个有限的推论（形式证明）。

库尔特·哥德尔（KurtGödel）在其1929年的博士论文（以及1930年发表的一篇文章的改写版本）中给出的哥德尔完备性定理的证明今天并不容易理解。它使用了不再使用的概念和形式以及常常是模糊的术语。下面给出的版本试图忠实地代表证明中的所有步骤和所有重要的思想，同时用数学逻辑的现代语言重申证明。这个大纲不应该被认为是一个严格的定理证明。

1929年哥德尔首先证明了这一点。1947年，当莱昂·亨金（Leon Henkin）在他的博士学位上观察的时候，它被简化了。论证了证明的难点可以作为模型存在定理（1949年出版）。1953年，吉斯伯特·哈森贾格（Gisbert Hasenjaeger）简化了亨金的证明。

1.定理的原始配方

哥德尔完全性定理最为熟知的形式声称在一阶谓词演算中所有逻辑上有效的公式都是可以证明的。

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

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

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

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

2.更一般的形式

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

完全性定理等价于超滤子引理，它是弱形式的选择公理，在不带有选择公理的策梅洛-弗兰克尔集合论中有着等价的可证明性。

哥德尔对定理的原始证明是通过将问题简化为特定语法形式的公式的特例，然后用特别的论证来处理这种形式。在现代的逻辑文本中，哥德尔的完备性定理通常用Henkin的证明来证明，而不是用哥德尔的原始证明。亨金的证明直接构造了任何一致的一阶理论的术语模型。James Margetson利用Isabelle定理证明书开发了一个计算机化的形式证明。其他的证明也是已知的。

Henkin定理是最简单的证明中最完整的定理的最直接的版本。

根据Henkin定理，完备性定理的证明如下： 是有效的，那么 没有模型。那么，通过与Henkin的对立 是一个不一致的公式。但是，由一致性的定义，如果 是不一致的，那么有可能建立一个证明 。

与不完备性定理的关系

哥德尔不完备性定理是另一个着名的结果，表明数学中的形式证明可以实现的内在固有的局限性。对于不完备性定理名指的是另一种意义完整。

它表明，在任何一致的、有效的理论 含有皮亚诺算术（PA），式 表达的一致性 不能证明内 。

对这个结果应用完备性定理给出了 模型的存在，其中公式 是假的。这样的模型（恰恰是它所包含的“自然数”集合）必然是非标准的，因为它包含了 的矛盾证明的代码数。但从外部看， 是一致的。因此，这个 的矛盾证明的代码编号必须是非标准编号。

事实上，任何包含PA的理论模型都是通过系统建构的算术模型存在定理而得到的，它总是不规范的，用非等价的可证析谓词和非等价的方法来解释自己的构造，所以这种构造是非递归的（因为递归定义是明确的）。