一阶逻辑完备性定理

左边的 $\models$ 量化所有模型：“在每一个满足 $\mathrm{\Gamma }$ 的结构里，$\phi$ 都真。”右边的 $⊢$ 只要求一份有限形式推导。完备性把这两个看似相距很远的要求连起来：凡是所有模型都无法避开的结论，都能由有限多个前提、经过有限步规则推出。

有限推导何时又是可机械核验的证书，需要有效性条件。语言符号和规则必须能有效编码、检查，所用前提属于 $\mathrm{\Gamma }$ 也要有可核验的依据。若公理可判定，可直接检查；若只可递归枚举，可以给每条公理附上它在枚举中出现的有限运行见证。对任意前提集或不可数签名，完备性仍断言有限推导存在，却没有自动提供这样的统一算法。

Henkin 构造说明模型如何从语法中产生：若一套假设推不出矛盾，就把它要求存在的对象逐一命名，再用闭项及其等价类搭出模型。这解释了为什么“语法一致”能推出“有模型”。它与 Gödel 不完备性定理不冲突：完备性针对逻辑演算捕获语义后果的能力；不完备性针对足够强、一致且可有效公理化的算术理论，说明有些句子及其否定都不是该理论的可证结论。

正面例子：设 $\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有无限模型的一阶理论在适当基数上存在较小或较大的模型。。在可有效处理的语言和演算中，公平枚举证明给出有效性的半判定程序；对于一般不可判定的签名，无效输入上的证明搜索可能永不停机。受限片段若有判定方法，则还利用了额外结构。本库可先沿形式系统理路形式系统Formal system · Formal calculus由符号、形成规则、公理与推导规则组成的精确定义系统。、语法可导性理路句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。和语义蕴涵理解三个对象，再进入紧致性与模型构造。