条件证明 vs 间接证明

概述

条件证明（CP）和间接证明（IP/RAA）是第9章引入的两种高级证明技术。CP通过假设条件陈述的前件来证明条件陈述，IP通过假设结论的否定来推导矛盾。两者都使用”假设-推导-消去”的模式，都受辖域限制，都支持嵌套。关键区别在于：CP的目标是证明条件陈述，IP的目标是证明任意陈述。

共同点

• 都使用”假设-推导-消去”的三步模式
• 都引入临时假设，受辖域线限制
• 都支持嵌套使用
• 都可以在无前提前提下证明重言式
• 都可以大幅缩短证明长度

关键区别

维度	条件证明 CP	间接证明 IP/RAA
目标	证明条件陈述 $p\supset q$	证明任意陈述 $q$
假设	假设前件 $p$	假设结论的否定 $\sim q$
推导目标	推导后件 $q$	推导矛盾 $r\cdot \sim r$
消去结果	得到 $p\supset q$	得到 $q$
理论基础	演绎定理（输出律）	爆炸原理 + DN
冗余性	基本技术（不可从其他规则推出）	可从CP推出（冗余）
最佳适用场景	结论是条件陈述	结论是否定陈述或难以直接证明

深层联系

IP可以从CP推导

IP在理论上是冗余的——它可以完全用CP来表达。要证明 $q$：

1. 用CP假设 $\sim q$
2. 在假设下推导出矛盾 $r\cdot \sim r$
3. 因为 $r\cdot \sim r$ 蕴涵任何陈述（包括 $\sim q\supset q$），所以通过CP得到 $\sim q\supset q$
4. $\sim q\supset q$ 逻辑等价于 $q\vee q$，即 $q$（重言律）

因此，IP不需要作为独立的基本规则，但保留IP使许多证明更简洁直观。

选择策略

• 结论是条件陈述 → 优先使用CP
• 结论是否定陈述 → 优先使用IP
• 结论是析取陈述 → 先等价变换为条件陈述，再用CP
• 两种方法都尝试，选择更短的那个

参见

• 条件证明 — CP规则的完整概念页
• 间接证明 — IP/RAA规则的完整概念页
• 自然演绎 — CP和IP所属的形式证明系统
• 推论规则 — 19条基本推论规则
• 有效性 — CP和IP共同服务的目标