命题逻辑可靠性与完备性定理

形式陈述 ​

本页在 ZFC 中取一个集合大小的命题变量集，固定标准经典 Hilbert 式命题逻辑理路命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。演算，并用 $⊢$ 表示句法可推导理路句法可推导关系Syntactic derivability · Provability relation用有限形式证明把前提集与可由它推出的公式联系起来的元关系。。演算包含经典否定原则，以肯定前件为推理规则。可靠性与完备性合并为

可靠性对推导归纳，逐条检查公理永真且肯定前件保持语义后承。完备性可用逆否命题证明。假设 $\mathrm{\Gamma }⊬\phi$，则 $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ 一致：否则由演绎定理理路演绎定理Deduction theorem在适当证明系统中，把一个临时前提移入蕴含式前件。得到 $\mathrm{\Gamma }⊢\mathrm{\neg }\phi \to \mathrm{\perp }$，再用经典双重否定消去便有 $\mathrm{\Gamma }⊢\phi$，矛盾。

把包含这个集合的一致公式集按包含排序。非空链的并仍一致，因为任何矛盾证明只用有限多个前提，它们必已同时落在链的某一个成员中；空链则以起始一致集 $\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}$ 为上界。公式全体是集合，所以可用Zorn 引理理路佐恩引理Zorn's lemma若偏序集中每条链都有上界，则该偏序集存在极大元。取得极大一致集 $\mathrm{\Delta }$。它对推导封闭：添入已经从 $\mathrm{\Delta }$ 推出的公式不会产生新的矛盾，否则把该公式的原推导接入，就已能从 $\mathrm{\Delta }$ 推出矛盾；极大性因此迫使这个公式属于 $\mathrm{\Delta }$。此外，$\mathrm{\Delta }$ 对每个公式 $\psi$ 恰好包含 $\psi ,\mathrm{\neg }\psi$ 中的一个：两者不能同时出现；若 $\psi \notin \mathrm{\Delta }$，极大性使 $\mathrm{\Delta }\cup \{\psi \}$ 不一致，演绎定理就给出 $\mathrm{\neg }\psi \in \mathrm{\Delta }$。

定义赋值 $v(p)=1$ 当且仅当 $p\in \mathrm{\Delta }$。经典演算的联结词规则保证

其余联结词按相同方式处理；对公式结构归纳，得到真值引理 $v\models \psi ⟺\psi \in \mathrm{\Delta }$。于是 $v$ 满足 $\mathrm{\Gamma }$，却因 $\mathrm{\neg }\phi \in \mathrm{\Delta }$ 而否定 $\phi$，这就是所需反赋值。反之，没有反赋值就必有形式证明，而每份证明只使用有限多个前提。

有限前提的后承还可用真值表理路真值表Truth table按命题变元的全部赋值逐行计算复合公式真值的有限表格模型。直接检查：列出前提与结论中实际出现的有限变量，对每一行寻找“前提全真、结论假”。这样的行是反赋值；若所有行都排除了它，完备性便保证存在推导。