形式陈述

固定一个标准命题逻辑证明系统。可靠性与完备性合并为

$$ \Gamma\vdash\varphi \quad\Longleftrightarrow\quad \Gamma\models\varphi. $$$$\mathrm{\Gamma }⊢\phi ⟺\mathrm{\Gamma }\models \phi .$$

可靠性对推导归纳，证明每个公理永真且推理规则保持语义后承。完备性对任意前提集可通过极大一致集构造反赋值；在有限前提情形，也可直接使用真值表或规范范式。若 $\varphi$$\phi$ 不是语义后果，则存在满足 $\Gamma$$\mathrm{\Gamma }$ 而否定 $\varphi$$\phi$ 的赋值；反之没有反赋值时存在只使用有限多个前提的形式证明。具体公理和规则可以不同，但必须分别验证这两个方向。

直觉

形式演算既不会证明语义错误的结论，也不会漏掉任何由命题真值结构强制的结论；句法与语义因此精确对齐。

例子与边界

因为 $\{p,p\to q\}\models q$$\{p,p\to q\}\models q$，完备性保证在完整演算中可推出 $q$$q$；因为 $p\lor q\not\models p$$p\vee q⊭p$，可靠性保证不能从前者合法推出后者。一个只允许重复前提的弱系统可能可靠却不完备；加入“从任意式推出任意式”的规则则会不可靠。定理针对指定演算，不是所有写成符号规则的系统自动成立。

推论与应用

该定理证明命题逻辑推理的可信性与充分性，支持证明搜索、自动验证和等价变换。由于命题变量有限时真值表终止，它也与命题逻辑可判定性一致。

参考资料

• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Chs. IV–V, sequent calculus and completeness; propositional fragment。
• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, 2000，Chs. 2–3, natural-deduction, Hilbert, and Gentzen systems。