北京大学：《离散数学》系列课程之三《数理逻辑》第26章 命题逻辑（26.6）命题演算自然推理形式系统N

数理逻辑 第26章§6 命题演算自然推理形式系统N 王捍贫 北京大学信息科学技术学院软件研究所

26 §6 N ￾✁✂ ✄☎✆✝✞✟✠✝✡☛✝☞✌✍✎✏✑

6命题演算的自然推理形式系统N 怎么在计算机上实现如下有效推理: {p→q,q→r}+p→r 识别符号p,q,r, 别公式p→q,q→r, ●推理方法

§6 N ✒ {p → q, q → r} ` p → r • p, q, r, . . . • p → q, q → r, . . . • 1

计算机上实现有效推理需要建立: 字母表(符号库)一非空集合 ●公式集合一字母表中符号的有限序列 ●公理集合一公式集合的子集 规则集合一公式集合的部分多元运算

✓ • ✔✕— • — • — • — 2

形式系统 符号库(字母表) ·(形式)公式 推理 (形式)公理 (形式)推理规则 符号库和形式公式统称为形式语言。 形式公理和形式推理规则统称为形式推理。 命题演算的自然推理形式系统N

• ✔✕ • ( ) • ( ) • ( ) ✖ ✖ ✗✘N 3

N的符号库 p1,P2, (可数个命题符号) V,∧ (5个联结词符号) (3)) (2个辅助符号)

N (1) p1, p2, . . . ( ) (2) ¬, ∨, ∧, →, ↔ (5 ) (3) ), ( (2 ) 4

N的公式 归纳定义如下 (1)命题符号都是公式; (2)若a是公式,则(a)也是公式; (3)若a,β是公式,则(a∨3),(a∧B),(a→B), (a台6)也都是公式; (4)每个公式都是有限次使用(1)、(2)或(3)得到的

N ✒ (1) ; (2) α ✙(¬α) ✚ (3) α, β ✙(α ∨ β), (α ∧ β), (α → β), (α ↔ β) ✚ (4) (1) ✛(2) (3) . 5

N的公理 公理集合为空集

N 6

N的推理规则 包含律: 若a∈「, 则「a ∈ 消去律 若「U{(a)}B,「U{(a)}+(), 则厂卜

N : α ∈ Γ ✙ Γ ` α. (∈) ¬ : Γ ∪ {(¬α)} ` β, Γ ∪ {(¬α)} ` (¬β), Γ ` α. (¬−) 7

N的推理规则(续一 →消去律 若「(a→),「a, →引入律 若「U{a}FB, 则厂a→ (→+)

N ( ✜ ) → : Γ ` (α → β), Γ ` α, Γ ` β. (→ −) → : Γ ∪ {α} ` β, Γ ` α → β. (→ +) 8

N的推理规则(续二) ∨消去律 若「U{a}+?,「U{}m, 则「U{(a6)}y ∨引入律: 若「十a, 则+(aV),「+(Va) (V+)

N ( ) ∨ : Γ ∪ {α} ` γ, Γ ∪ {β} ` γ, Γ ∪ {(α ∨ β)} ` γ. (∨−) ∨ : Γ ` α, Γ ` (α ∨ β), Γ ` (β ∨ α). (∨+) 9