可靠性定理

概述

可靠性定理（Soundness Theorem）：如果一个论证的所有前提都为真，则其结论不可能为假——这正是有效论证形式的定义。在形式系统的层面，可靠性定理断言：凡是用推论规则能证明的论证，在语义上都是有效的。它保证了形式证明系统不会”证明”无效的论证。

定理陈述

形式化陈述

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

语义层面（有效性的定义）： 论证 $\Gamma ⊢C$ 是有效的，当且仅当不可能 $\Gamma$ 中所有命题为真而 $C$ 为假。

语法-语义层面（形式系统的可靠性）： 如果 $\Gamma ⊢C$（即存在一个从 $\Gamma$ 到 $C$ 的形式证明），则 $\Gamma \models C$（即 $\Gamma$ 语义蕴涵 $C$）。

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

各项说明：

• $⊢$：语法推导关系（syntactic entailment），表示存在使用推论规则的形式证明
• $\models$：语义蕴涵关系（semantic entailment），表示在所有使前提为真的解释下结论也为真
• 可靠性定理的逆命题是完备性定理：若 $\models$ 则 $⊢$

证明概要

证明思路（有效论证形式的定义 + 推论规则的有效性验证）

核心思想

可靠性定理的证明需要验证两件事：（1）每个基本推论规则本身都是有效的；（2）有效的推理步骤的组合仍然是有效的。

详细步骤

第一步：验证基本推论规则的有效性

自然演绎系统中的每个基本推论规则（如肯定前件、假言三段论、析取三段论等）都可以通过真值表验证其有效性。例如：

• 肯定前件（$P\to Q,P⊢Q$）：当 $P\to Q=T$ 且 $P=T$ 时，由蕴涵的真值表定义，$Q$ 必然为 $T$。
• 否定后件（$P\to Q,\neg Q⊢\neg P$）：当 $P\to Q=T$ 且 $\neg Q=T$（即 $Q=F$）时，若 $P=T$ 则 $P\to Q=F$，矛盾，故 $P=F$，即 $\neg P=T$。

第二步：证明推理步骤的保真性

设论证的形式证明由 $n$ 个步骤组成，每个步骤要么是前提，要么是通过某个推论规则从前面步骤推出的。

• 基础情况：前提为真的假设直接给出。
• 归纳步骤：假设到第 $k$ 步为止所有已推出的命题在前提为真时都为真。第 $k+1$ 步通过某个有效推论规则从前面已建立的命题推出。由于该规则本身是有效的（第一步已验证），且其前提（前面步骤的命题）在前提为真时都为真（归纳假设），故第 $k+1$ 步的结论在前提为真时也为真。

第三步：得出结论

由数学归纳法，形式证明的最后一个步骤（即结论 $C$）在前提为真时必然为真。因此，如果 $\Gamma ⊢C$，则 $\Gamma \models C$。

证毕。$■$

关键推论

• 推论1（一致性保证）：如果形式系统可以推出矛盾（$⊢P\wedge \neg P$），则该系统是不可靠的。因此可靠性定理保证了：如果前提是一致的（不包含矛盾），则形式证明不会引入矛盾。
• 推论2（与完备性的互补关系）：可靠性定理（$⊢\Rightarrow \models$）与完备性定理（$\models \Rightarrow ⊢$）合在一起，建立了语法推导与语义蕴涵的完全等价性：$⊢\iff \models$。这意味着形式证明系统”恰好足够强”——不会多证明也不会少证明任何有效论证。
• 推论3（有效性与真实性的区分）：可靠性定理处理的是论证形式的有效性，而非前提和结论的实际真假。一个论证可以形式上有效但前提为假（此时结论可为真可假），也可以前提为真且结论为真但论证形式无效。

应用场景

1. 形式系统的设计验证：在设计逻辑推理系统时，可靠性定理是必须验证的基本性质，确保系统不会推导出语义上无效的结论。
2. 自动定理证明：在自动化推理系统中，可靠性保证了程序输出的证明在语义上是正确的。
3. 逻辑教学：可靠性定理帮助学生理解形式证明与语义有效性之间的关系，是连接语法和语义的桥梁。
4. 哲学逻辑：在非经典逻辑（如直觉主义逻辑、多值逻辑）中，可靠性定理的成立与否是评估该逻辑系统合理性的重要标准。

参见

• 有效性 — 有效性的语义定义
• 推论规则 — 可靠性定理验证的基本对象
• 自然演绎 — 形式证明系统的具体实现
• 可靠性 — 可靠性概念的详细讨论
• 演绎论证 — 可靠性与演绎论证的关系