一阶逻辑完备性定理

定理沟通的是两个先验上毫不相同的世界：左边的 $\models$ 量化所有模型——"在每一个满足 $\mathrm{\Gamma }$ 的结构里 $\phi$ 都真"，这是一条关于无限多、可能巨大无比的结构的断言；右边的 $⊢$ 只谈一个有限的符号串序列。完备性说，凡是语义上躲不掉的结论，总有一份有限的、可机械核验的证书。为什么可能？Henkin 构造给出的答案是：语法本身足以充当模型的原料——如果一套假设推不出矛盾，就把"它说存在的东西"逐一命名，用这些名字自己搭出一个模型来。于是"无矛盾"与"可实现"在一阶世界里是同一件事。值得强调这与 Gödel 不完备性定理并无冲突：完备性说的是逻辑演算捕获全部逻辑后果；不完备性说的是任何一致、可有效公理化且足以表达基本算术的理论，都有既不可证也不可反驳的句子——后者是 $\mathrm{\Gamma }$ 自身证明能力的局限，不是演算的失职。

正面例子：设 $\mathrm{\Gamma }$ 为群公理，$\phi$ 为"单位元唯一"。$\phi$ 在每个群中为真，故 $\mathrm{\Gamma }\models \phi$；完备性保证存在从群公理出发的形式证明，而我们熟知的代数推导（两个单位元相互吸收）正是它的非形式版本。反方向的用法同样典型：若 $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ 语法一致，则由模型存在形式它有模型，从而 $\mathrm{\Gamma }⊭\phi$——这是证明"某命题不可从公理导出"的标准途径。

边界之一：完备性不给出判定程序。对可有效编码的一阶语言，全体可证句子可以枚举（逐一生成证明），故有效式集可递归枚举，但 Church–Turing 的不可判定性结果表明它不可判定：对无效公式，证明搜索可能永不停机。边界之二：定理对逻辑本身成立，不担保具体理论完备——若Peano 算术公理库皮亚诺算术Peano arithmetic · PA用一阶语言公理化自然数的零、后继、加法、乘法与归纳模式的形式理论。一致，则它有不可判定句，见Gödel 第一不完备性定理公理库哥德尔第一不完备定理Gödel's first incompleteness theorem足够强、有效公理化且一致的算术理论存在既不可证也不可否证的句子。。边界之三：换成标准语义的二阶逻辑后定理失效——不存在同时可靠、完备且可递归枚举的演算，这是一阶逻辑独享的性质。若改在 ZF 或构造性基础中追踪定理强度，则必须同时固定语言的集合大小、语义和完备性版本；面向所有集合大小语言的若干经典完备性、紧致性表述与 Boolean Prime Ideal Theorem 等弱选择原则相关，不能只说“需要某种弱选择”。

完备性是模型论与证明论之间的桥梁，两侧的搬运都富有成果。由"证明只用有限多前提"立即得到紧致性定理公理库一阶逻辑紧致性定理First-order compactness theorem · Compactness theorem一阶理论可满足，当且仅当它的每个有限子理论都可满足。：有限可满足的理论整体可满足——非标准分析的无穷小模型、图着色的从有限到无限的提升都由此而来。Henkin 构造顺带给出可数语言的可数模型，通往 Löwenheim–Skolem 定理公理库Löwenheim–Skolem 定理Löwenheim–Skolem theorem有无限模型的一阶理论在适当基数上存在较小或较大的模型。。实践层面，对可有效编码的一阶语言，完备性是自动定理证明的理论执照：有效性虽不可判定，但可半判定，饱和式的归结证明器正是在枚举 $⊢$ 的世界里搜索 $\models$ 的真理。在本库链条中，它上承形式系统公理库形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。与语法可导性公理库句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。的定义，下接紧致性、模型构造与不完备性诸定理，是"语法与语义等价"这一主题的中心结果。