哥德尔完备性定理

哥德尔完备性定理是逻辑学中的一项基本结果，它表明，经典逻辑的一阶逻辑标准演绎演算能够证明在前提的所有解释下都成立的每个后承。该定理将语义上的真与形式上的可推导性联系起来：如果一个句子在某个理论的每个模型中都为真，那么它就能由该理论通过有限的证明推导出来。库尔特·哥德尔在1929年的博士论文中确立了这一结果，并于1930年发表了修订后的证明。(www3.cs.stonybrook.edu)

形式表述

设 $T$ 为一阶句子的集合， $\varphi$ 为同一语言中的一个句子。记号 $T\models\varphi$ 表示，每个满足 $T$ 中所有句子的结构也都满足 $\varphi$ 。记号 $T\vdash\varphi$ 表示，在指定的演绎演算中，存在一个以 $T$ 中的句子为假设、证明 $\varphi$ 的形式证明。完备性断言：

T\models\varphi\quad\Longrightarrow\quad T\vdash\varphi.

其逆命题是可靠性定理，它保证推导保持真值。两者合在一起便得到：

T\models\varphi\quad\Longleftrightarrow\quad T\vdash\varphi.

这体现了句法与语义学之间的对应关系：前者研究以符号方式定义的推导，后者研究解释与满足关系。(math.umd.edu)

在没有前提的情况下，该定理表明，每个具有逻辑有效性的句子，即在每个结构中都为真的句子，都可以仅凭逻辑公理得到证明。如果允许任意的、可能无限的前提集合，就得到通常称为强完备性的表述。与之等价的模型存在性表述是：每个在句法上一致的一阶理论都有模型。这里的一致性是指无法推导出矛盾，并不意味着该理论正确描述了某个特定的预期结构。(math.umd.edu)

历史背景与演绎系统

哥德尔的结果将命题逻辑的完备性研究推广到了谓词逻辑；在谓词逻辑中，量词的取值范围是个体对象。他最初的论证采用希尔伯特式演算：由逻辑公理和推理规则生成有限的推导。其他表述则采用自然演绎或相继式演算。完备性针对的是一种演算及其语义，并不保证任意选取的一组推理规则都能涵盖所有有效论证。(academic.oup.com)

莱昂·亨金在1947年的博士论文中提出了另一种影响深远的证明，并于1949年发表。他的方法不是直接将有效公式转化为推导，而是从一致的句子集合出发构造模型。这种模型构造的视角，使证明论与模型论之间的关系格外清晰。(www3.cs.stonybrook.edu)

亨金证明的思路

证明首先通过加入新的常元来扩充语言，使这些常元充当存在性陈述的见证。对于每个适当的公式 $\psi(x)$ ，引入一个形如

\exists x\,\psi(x)\rightarrow\psi(c)

的句子，其中 $c$ 是一个新常元。扩充过程经过安排，既保持一致性，也为构造过程中出现的存在公式提供见证。随后，将所得理论扩充为一个极大一致集；对于每个句子，该集合都包含它或它的否定。(math.umd.edu)

接着构造一个项模型。模型中的对象由闭项构成；如果扩充后的理论能证明两个闭项相等，就将它们视为同一对象。因此，可证的相等关系定义了一个等价关系，模型的论域由该关系的等价类构成。函数符号通过构成项来解释，关系符号则根据相应原子句子是否属于极大一致集来解释。对公式结构进行归纳，可以证明真值引理：一个句子在该模型中成立，当且仅当它属于这个集合。存在性见证为处理量词的关键步骤提供了依据。(pi.math.cornell.edu)

最后，假设 $T\models\varphi$ ，但 $T\not\vdash\varphi$ 。那么 $T\cup\{\neg\varphi\}$ 是一致的，因此上述构造给出一个满足 $T$ 却使 $\varphi$ 为假的模型。这与所假设的语义后承关系矛盾，从而证明了完备性。(pi.math.cornell.edu)

对模型的推论

由于每个形式证明都只使用有限多个前提，紧致性定理可由此推出。如果 $T$ 的每个有限子集都有模型，那么由可靠性可知，任何有限子集都不可能推导出矛盾。因此， $T$ 是一致的，而完备性保证整个理论存在模型。等价地说， $T$ 的任何语义后承都已经是 $T$ 的某个有限子集的语义后承。(math.umd.edu)

对于符号集合为可数集的语言，亨金构造会产生一个论域至多可数的模型。这给出了勒文海姆—斯科伦定理的一种模型存在性表述。但这并不意味着所有模型都是可数的，也不意味着所构造的模型就是这些公理的预期解释。(pi.math.cornell.edu)

完备性、不完备性与可判定性

该定理与哥德尔不完备定理并不冲突。逻辑的完备性是指能够推导出在给定前提的所有模型中都为真的句子。理论的完备性则是指，对于每个句子，该理论都能证明它或它的否定，从而判定该句子。一个一致、可有效公理化且足以表达算术的理论，例如基于皮亚诺公理的一阶算术，即使使用完备的逻辑演算，也可能是不完备的。在这种情况下，一个独立句子及其否定会分别在该理论的不同模型中成立。(pi.math.cornell.edu)

完备性也不意味着存在一种能对每个逻辑问题都终止的算法。如果语言和演算具有有效的表示方式，就可以枚举证明，因此搜索最终能找到任何有效句子的证明。但对于无效句子，这种搜索未必会终止。一般的一阶逻辑有效性问题是不可判定的。(courses.grainger.illinois.edu)

对于二阶逻辑，所采用的语义同样至关重要。在完全语义下，关系变量的取值范围包括相应元数的所有关系，不存在能够证明所有有效句子的有效且可靠的演算。在亨金语义下，这些变量只在指定的关系集合中取值，此时便可建立相应的完备性定理。(ps.uni-saarland.de)