相关笔记: 8.10 逻辑等价 | 10.1 谓词逻辑概览

概览

第9章是命题逻辑的核心应用篇章,系统引入了形式证明(自然演绎)方法。全章从形式证明的基本概念出发(9.1 有效性的形式证明),引入9条基本推论规则(9.2 基本的有效论证形式),通过示例与策略讲解逐步深入(9.3 有效性形式证明示例9.4 有效性形式证明的构造9.5 构造更复杂的形式证明),然后扩展至10条替换规则(9.6 扩展推论规则:替换规则),讨论19条规则的完备性与冗余性(9.7 自然演绎系统),展示综合运用(9.8 运用19个推论规则构建形式证明),再介绍简化真值表方法作为补充验证工具(9.9 简化的真值表方法),最后讨论不相容性(9.10 不相容性)、条件证明(9.11 条件证明)、间接证明(9.12 间接证明),并以可靠性论证与笃证性论证的辨别收束全章(9.13 可靠性论证与笃证性论证的辨别)。


一、全章知识框架

graph TB
    CH["第09章 命题逻辑Ⅱ:演绎方法"]

    CH --> A["形式证明基础<br/>9.1-9.5"]
    CH --> B["扩展规则与系统<br/>9.6-9.9"]
    CH --> C["高级证明技术<br/>9.10-9.13"]

    A --> A1["9.1 形式证明概念"]
    A --> A2["9.2 九条基本规则"]
    A --> A3["9.3 证明示例"]
    A --> A4["9.4 证明构造策略"]
    A --> A5["9.5 复杂证明"]

    B --> B1["9.6 十条替换规则"]
    B --> B2["9.7 自然演绎系统"]
    B --> B3["9.8 综合运用"]
    B --> B4["9.9 简化真值表"]

    C --> C1["9.10 不相容性"]
    C --> C2["9.11 条件证明CP"]
    C --> C3["9.12 间接证明IP"]
    C --> C4["9.13 可靠性vs笃证性"]

    A1 --> A1a["自然演绎<br/>Gentzen系统"]
    A1 --> A1b["推论规则定义"]
    A1 --> A1c["代入例"]
    A1 --> A1d["陈述列+理由列"]

    A2 --> A2a["MP·MT·HS·CD"]
    A2 --> A2b["Simp·Add·Conj·Com·Abs"]

    B1 --> B1a["De M·Com·Assoc·Dist"]
    B1 --> B1b["DN·Trans·Impl·Equiv"]
    B1 --> B1c["Exp·Taut"]
    B1 --> B1d["关键区别:替换规则<br/>可应用于子表达式"]

    B2 --> B2a["完备性:所有有效论证<br/>都能被证明"]
    B2 --> B2b["冗余性:某些规则<br/>可从其他规则推出"]
    B2 --> B2c["能行性:存在机械<br/>程序验证证明"]

    C2 --> C2a["假设前件→推导后件→消去"]
    C2 --> C2b["嵌套CP"]
    C2 --> C2c["证明重言式"]

    C3 --> C3a["假设结论否定→推导矛盾"]
    C3 --> C3b["IP可从CP推出(冗余)"]
    C3 --> C3c["IP vs CP选择策略"]

二、核心知识点汇总

2.1 十九条推论规则完整表

规则分类记忆

9条基本论证规则用于从整行推出新行;10条替换规则用于在子表达式层面做等价替换。两类规则配合使用,构成完整的自然演绎系统。

9条基本论证规则(只能应用于整行):

编号名称缩写形式直觉
1肯定前件式M.P.肯定前件→肯定后件
2否定后件式M.T.否定后件→否定前件
3假言三段论H.S.蕴涵的传递性
4析取三段论D.S.否定一支→肯定另一支
5构造性二难式C.D.两条路都通
6简化律Simp.从合取中取出一个合取支
7合取律Conj.将两个真陈述合取
8附加律Add.附加一个析取支
9交换律Com.交换合取支/析取支顺序

10条替换规则(可应用于子表达式):

编号名称缩写形式
10De Morgan律De M.
11交换律Com.
12结合律Assoc.
13分配律Dist.
14双重否定律D.N.
15易位律Trans.
16实质蕴涵律Impl.
17实质等值律Equiv.
18输出律Exp.
19重言律Taut.

2.2 基本规则 vs 替换规则的关键区别

维度基本论证规则(1-9)替换规则(10-19)
逻辑性质有效论证形式逻辑等价式(重言双条件)
应用范围只能应用于整行可应用于整行或子表达式
推理方向单向(从前提推出结论)双向(等价替换)
典型用途从已知行推出新行变换已有行的形式

常见错误

不能从 中用简化律推出 ,因为 不是该行的整个陈述,而是蕴涵前件的一部分。简化律只能应用于”整行就是合取陈述”的情况。

2.3 条件证明(CP)与间接证明(IP)

CP与IP的核心思想

  • CP:要证明 ,==假设 ,推导 ,然后消去假设==得到
  • IP:要证明 ,==假设 ,推导矛盾,然后消去假设==得到
  • IP 可以从 CP 推导出来,因此 IP 是冗余的,但使用 IP 更方便
维度条件证明 CP间接证明 IP
目标证明条件陈述 证明任意陈述
假设假设前件 假设结论的否定
推导目标推导后件 推导矛盾
消去得到 得到
辖域假设内推导的陈述不能在辖域外使用同左
嵌套支持嵌套(多重条件证明)支持嵌套
冗余性基本规则(不可从其他规则推出)可从CP推出(冗余)

2.4 简化真值表方法(STTT)

步骤操作
1假设论证无效(前提全T,结论F)
2从结论F出发,强制赋值相关变元
3将赋值传播到前提,检查是否一致
4若所有前提都能为T → 论证无效;若某前提必须为F → 论证有效

2.5 不相容性与有效性

核心定理

如果一组前提是不相容的(不可能同时为真),那么任何结论都可以从这组前提中有效地推出。这就是 爆炸原理(Ex Contradictione Quodlibet)。

2.6 可靠性 vs 有效性 vs 笃证性

类型定义要求
有效不可能前提真结论假仅形式要求
可靠有效 + 所有前提实际为真形式 + 实质要求
笃证性前提相容 + 结论为偶真陈述前提相容 + 结论非重言非矛盾

三、学习脉络

全章的学习遵循一条清晰的递进路径:

形式证明概念(什么是自然演绎,为什么需要形式证明)
    ↓
九条基本规则(MP/MT/HS/DS/CD/Simp/Add/Conj/Com)
    ↓
证明示例与构造策略(从简单到复杂,正推与倒推)
    ↓
十条替换规则(De M/Com/Assoc/Dist/DN/Trans/Impl/Equiv/Exp/Taut)
    ↓
自然演绎系统(19条规则的完备性、冗余性、能行性)
    ↓
综合运用(两类规则配合使用)
    ↓
简化真值表方法(补充验证工具)
    ↓
不相容性(爆炸原理)
    ↓
条件证明CP(假设-推导-消去)
    ↓
间接证明IP(归谬法)
    ↓
可靠性论证与笃证性论证的辨别

学习建议

  • 9.1-9.5 是”基础层”:掌握9条基本规则和证明构造策略,务必熟记每条规则的符号形式
  • 9.6-9.9 是”扩展层”:掌握10条替换规则和两类规则的区别,务必理解"替换规则可应用于子表达式"
  • 9.10-9.13 是”高级层”:掌握CP和IP技术,务必理解假设辖域的限制和嵌套证明的方法

四、跨章关联

4.1 第9章与第8章的关系

维度第8章(命题逻辑Ⅰ)第9章(命题逻辑Ⅱ)
核心方法真值表方法(语义方法)形式证明方法(语法方法)
判定方式穷举所有真值指派构造有效推论序列
优势机械、直观适用于任意多变量的论证
局限变元增多时指数爆炸需要洞察力和策略

互补关系

真值表方法和形式证明方法是命题逻辑中两种互补的有效性判定方法。真值表是语义方法(基于真值指派),形式证明是语法方法(基于推论规则)。完备性定理保证:一个论证是有效的(语义),当且仅当它可以被形式证明(语法)。

4.2 具体关联映射

第9章概念关联章节关联说明
9条基本规则8.8 一些常见的论证形式MP/MT/HS/DS在第8章已通过真值表验证为有效
10条替换规则8.10 逻辑等价替换规则的理论基础是第8章的逻辑等价关系
De Morgan律8.10 逻辑等价第8章用真值表验证,第9章用作替换规则
实质蕴涵律8.4 条件陈述与实质蕴涵第8章定义了蕴涵的三种等价形式
形式证明8.7 根据真值表验证论证形式证明是真值表方法的替代方案
CP/IP8.9 陈述形式与实质等值CP的辩护依赖于论证有效⟺条件陈述为重言式
不相容性8.9 陈述形式与实质等值矛盾式(第8章)与不相容命题集(第9章)的关联
可靠性8.6 “无效”和”有效”的精确含义有效性(第8章定义)+ 前提为真 = 可靠性(第9章)

五、复习题

题1:综合运用基本规则与替换规则构造形式证明

题目

给定以下论证:

前提1: 前提2: 前提3:

(a) 使用19条推论规则构造该论证的有效性形式证明。 (b) 说明每一步使用了哪条规则。

题2:使用条件证明证明论证有效性

题目

给定以下论证:

前提1: 前提2:

(a) 使用条件证明(CP)证明该论证有效。 (b) 标注假设的辖域线。

解题思路提示

  1. 当结论是条件陈述时,优先考虑使用CP
  2. CP的关键是假设前件后,观察需要推导什么
  3. 从假设出发,尝试用附加律(Add.)”激活”前提中的析取/蕴涵结构
  4. 如果结论不是条件陈述,先考虑等价变换(如

六、笔记索引

节号笔记标题核心主题关键概念
9.19.1 有效性的形式证明形式证明的基本概念自然演绎;推论规则;代入例;陈述列+理由列
9.29.2 基本的有效论证形式九条基本推论规则MP/MT/HS/DS/CD/Simp/Add/Conj/Com
9.39.3 有效性形式证明示例证明示例解读逐步解读证明;行号引用规范;向前链与向后链
9.49.4 有效性形式证明的构造证明构造策略从结论倒推;从前提出发正推;双向夹击法
9.59.5 构造更复杂的形式证明复杂证明多步证明;自然语言符号化;反向回溯策略
9.69.6 扩展推论规则:替换规则十条替换规则De M/Com/Assoc/Dist/DN/Trans/Impl/Equiv/Exp/Taut;子表达式替换
9.79.7 自然演绎系统系统性质完备性;冗余性;能行性
9.89.8 运用19个推论规则构建形式证明综合运用两类规则配合;常见证明模式;四步法
9.99.9 简化的真值表方法STTT方法强制赋值vs非强制赋值;判定准则I-V;C序列vs P序列
9.109.10 不相容性不相容命题集爆炸原理;不相容性与有效性;判定方法
9.119.11 条件证明CP规则假设-推导-消去;辖域线;嵌套CP;证明重言式
9.129.12 间接证明IP/RAA规则假设否定→推导矛盾;IP冗余性;IP vs CP
9.139.13 可靠性论证与笃证性论证的辨别论证评估可靠性=有效+前提真;笃证性;三步评估法

参见 Wiki

章节汇总