形式陈述

固定一个一阶语言、语义以及证明演算。可靠性定理断言，对任意句子集 $\Gamma$$\mathrm{\Gamma }$ 和公式 $\varphi$$\phi$，

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

若允许公式带自由变量，右侧表示：每个使 $\Gamma$$\mathrm{\Gamma }$ 中全部公式为真的结构与变量赋值，也使 $\varphi$$\phi$ 为真。证明对形式推导长度归纳：逻辑公理在所有解释下有效，非逻辑公理由满足 $\Gamma$$\mathrm{\Gamma }$ 的模型满足，而每条推理规则都保持真值。定理依赖所选演算；“可靠”不是纯语法系统自动具有的性质。

直觉

形式证明不能从真前提出发推出语义上的假结论。每个证明步骤都像一个局部保真变换，有限串联后仍然保真。

例子与边界

从 $\forall x(P(x)\to Q(x))$$\mathrm{\forall }x(P(x)\to Q(x))$ 与 $P(a)$$P(a)$ 推出 $Q(a)$$Q(a)$，在任意同时满足两前提的结构中都成立。若 $\Gamma$$\mathrm{\Gamma }$ 有模型而演算可靠，则不可能同时推出 $\psi$$\psi$ 与 $\neg\psi$$\mathrm{\neg }\psi$，所以语义可满足性蕴含语法一致性。反之，可靠性本身不保证所有语义后果都可证明；一个只含少数规则的演算可能可靠却严重不完备。

推论与应用

可靠性把证明检查连接到模型语义，是程序验证、自动定理证明和形式化数学可信性的最低要求。它还允许用一个反模型否定可推导性：若存在 $\mathcal M\models\Gamma$$\mathcal{M}\models \mathrm{\Gamma }$ 但 $\mathcal M\not\models\varphi$$\mathcal{M}⊭\phi$，则可靠性立即给出 $\Gamma\nvdash\varphi$$\mathrm{\Gamma }⊬\phi$。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001，§2.2, soundness of first-order deduction。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Ch. II, soundness theorem for predicate logic。