完备性定理

概述

完备性定理（Completeness Theorem）：在命题逻辑中，每一个语义上有效的论证都可以通过19个推论规则给出形式证明。换言之，真值表方法能判定的所有有效论证，形式证明系统也都能证明。完备性定理与可靠性定理合在一起，确立了语法推导与语义蕴涵的完全等价性。

定理陈述

形式化陈述

定理（命题逻辑完备性定理）：设 $\Gamma$ 为一组命题（前提），$C$ 为一个命题（结论）。则：

如果 $\Gamma \models C$（即 $\Gamma$ 语义蕴涵 $C$，在所有使 $\Gamma$ 为真的解释下 $C$ 也为真），则 $\Gamma ⊢C$（即存在一个使用19个推论规则从 $\Gamma$ 到 $C$ 的形式证明）。

用符号表示：若 $\models$ 则 $⊢$。

特别地，对于不含前提的情形：如果 $C$ 是重言式（$\models C$），则 $C$ 是可证明的（$⊢C$）。

各项说明：

• 19个推论规则包括：9个基本有效论证形式（如肯定前件、否定后件、假言三段论等）和10个替换规则（如 De Morgan 定律、双重否定律等）
• 完备性定理的逆命题是可靠性定理：若 $⊢$ 则 $\models$
• 本定理是命题逻辑的完备性；谓词逻辑的完备性由哥德尔完备性定理（1929）建立

证明概要

证明思路（通过真值表构造形式证明）

核心思想

对于任何有效的论证，其条件式 $(P_1\wedge \cdots \wedge P_n)\to C$ 是重言式。我们可以利用完备真值表的信息，系统性地构造一个形式证明。

详细步骤

第一步：将有效性问题转化为重言式问题

论证 $\{P_1,\dots ,P_n\}⊢C$ 有效，当且仅当条件式 $(P_1\wedge \cdots \wedge P_n)\to C$ 是重言式。因此只需证明：每个重言式都是可证明的。

第二步：利用简化真值表方法

对于重言式，简化真值表方法（假设结论为假、前提为真，反推矛盾）必然导致矛盾。这个反推过程可以转化为形式证明的构造。

第三步：构造性证明策略

对于重言式 $S$，按以下策略构造证明：

1. 如果 $S$ 是某个推论规则的直接实例，则一步即可证明。
2. 如果 $S$ 可以通过替换规则从已知重言式得到，则先证明已知重言式，再应用替换。
3. 对于一般情况，利用条件证明和间接证明将问题分解为子目标，递归构造证明。

第四步：归纳论证

对命题的复杂度（联结词的个数）进行归纳：

• 基础情况：不含联结词的命题变项本身不是重言式（除非在退化情况下），无需处理。
• 归纳步骤：假设所有复杂度小于 $k$ 的重言式都是可证明的。对于复杂度为 $k$ 的重言式 $S$：
  • 若 $S$ 的主联结词是 $\to$，则 $S=A\to B$。由于 $S$ 是重言式，$A\models B$。由归纳假设和推论规则的组合，可以构造从 $A$ 到 $B$ 的证明，再用条件证明得到 $A\to B$。
  • 若 $S$ 的主联结词是 $\wedge$、$\vee$、$\neg$，类似地利用相应的推论规则和替换规则处理。

证毕。$■$

关键推论

• 推论1（语法与语义的等价性）：可靠性（$⊢\Rightarrow \models$）和完备性（$\models \Rightarrow ⊢$）合在一起给出 $⊢\iff \models$。这意味着命题逻辑的形式证明系统是”完备的”——它足以证明所有语义上有效的论证。
• 推论2（可判定性）：由于完备性定理，命题逻辑的有效性可以通过两种方式判定：（1）语义方法——真值表；（2）语法方法——形式证明搜索。虽然形式证明搜索在最坏情况下不如真值表方法高效，但完备性保证了它最终一定能找到证明（如果论证有效的话）。
• 推论3（紧致性定理）：作为完备性定理的推论，命题逻辑满足紧致性：如果 $\Gamma \models C$，则存在 $\Gamma$ 的有限子集 ${\Gamma }_0$ 使得 ${\Gamma }_0\models C$。这是因为形式证明只使用有限多个前提。

应用场景

1. 形式系统的充分性验证：完备性定理保证了19个推论规则构成的形式系统”足够强大”，能够证明所有有效论证。这是对形式证明系统设计的重要肯定。
2. 定理证明器的理论基础：在自动定理证明中，完备性定理保证了搜索算法的完备性——如果论证有效，搜索过程最终一定能找到证明。
3. 逻辑系统的比较：不同逻辑系统（如直觉主义命题逻辑）的完备性定理是否成立，是评估该系统表达力的重要标准。
4. 元逻辑研究：完备性定理是数理逻辑中最深刻的元定理之一，它揭示了形式证明与语义真值之间的深刻联系。

参见

• 推论规则 — 完备性定理所涉及的19个推论规则
• 自然演绎 — 形式证明系统的具体实现
• 有效性 — 语义有效性的定义
• 真值表 — 语义判定的基本方法