形式陈述

固定经典一阶逻辑的一个标准、可靠的有限证明演算，例如 Hilbert 系统或自然演绎。Gödel 完备性定理断言

$$ \Gamma\models\varphi\quad\Longrightarrow\quad\Gamma\vdash\varphi. $$$$\mathrm{\Gamma }\models \phi ⟹\mathrm{\Gamma }⊢\phi .$$

结合可靠性得到 $\Gamma\models\varphi$$\mathrm{\Gamma }\models \phi$ 当且仅当 $\Gamma\vdash\varphi$$\mathrm{\Gamma }⊢\phi$；这里“完备”正是定理结论，不能预先把演算称为“充分”来代替证明。该形式允许 $\Gamma$$\mathrm{\Gamma }$ 为无限集合。由于每个形式证明只使用有限多个前提，完备性进一步推出紧致性：若 $\Gamma$$\mathrm{\Gamma }$ 的每个有限子集都有模型，则 $\Gamma$$\mathrm{\Gamma }$ 整体有模型。典型证明把语法一致集扩充为完备的 Henkin 理论，再以闭项等价类构造模型。

直觉

一阶语义中所有不可避免的结论，都能被有限的符号证明捕获；虽然模型可能无限，见证一条逻辑后果的证明仍是有限对象。

例子与边界

若 $\Gamma\models\varphi$$\mathrm{\Gamma }\models \phi$，则 $\Gamma\cup\{\neg\varphi\}$$\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ 不可满足；完备性把这种语义不可满足转成形式矛盾，进而产生 $\varphi$$\phi$ 的证明。定理不意味着一阶有效性可判定：证明可以被枚举，但对无效公式，搜索可能永不停止。二阶逻辑采用标准语义时不存在同时有效、可递归枚举且完备的演算。

推论与应用

完备性支撑紧致性、Löwenheim–Skolem 定理和模型构造，也解释一阶有效式为何可识别。它是“语法一致性可产生模型”的核心桥梁，并允许把模型论问题转写为证明论问题。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§2.5, completeness theorem and Henkin construction。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Ch. III, completeness and compactness。