数理逻辑 第26章§7 命题演算推理形式系统P 王捍贫 北京大学信息科学技术学院软件研究所
26 §7 P ✁✂ ✄☎✆✝✞✟✠✝✡☛✝☞✌✍✎✏✑
复习—命题演算推理形式系统N ●N中推理的每个式子都由前提和结论组成,接近 于实际推理,又称为自然推理形式系统。 第一个给出自然推理形式系统的是德国数学家甘 岑(G. Gentzen,1909-1945),所以又称N为 甘岑系统.* ●N由符号库、公式、公理和规则四部分组成。 ●N中形式推理:「卜a ●形式化思想和方法正是计算机科学所需要的 计算机逻辑时代。 甘岑的另一个主要贡献是他用 Hilbert的超限归纳法证明了数论的一致 性,使形式主义避免了彻底的失败
—✒✓✔✕✖✗✘✙✚✛N • N ✜✢ ✢✣✤ • ✥ ✣ (G. Gentzen, 1909–1945) ✢N . ∗ • N ✜✦✦✤ • N ✧Γ ` α. • — ✤ ∗★✩✪ ✫✭✬ ✮✯✰✱✲✳✴✵Hilbert✪✶✷✸✹✺✻✼✽✾✿✪✬ ❀ ❁❂❃❄✯❅❆❇❈✽❉❊✪❋●❍ 1
7命题演算推理形式系统P 命题演算形式系统N的“缺点”: 符号太多:{,→}就已经是联结词的完全集 ●公式复杂 公理和规则太多:10条 推理麻烦:又是前提又是结论. 命题演算推理系统尸是一个“简洁”的形式系统
§7 P N ■❏ ✧ • : {¬, →} ❑. • . • : 10 • ✧. ▲P ▼◆❖ ▲P 2
P的符号库 p1,P2, (可数个命题符号) (2个联结词符号) (3)) (2个辅助符号)
P (1) p 1, p 2, . . . ( ) (2) ¬, → (2 ) (3) ), ( (2 ) 3
P的公式 归纳定义如下 (1)命题符号都是公式; (2)若a是公式,则(-a)也是公式; (3)若a、β是公式,则(α→)也都是公式; (4)每个公式都是有限次使用(1)、(2)或(3)得到的
P ✧ (1) ; (2) α ✢(¬α) ◗ (3) α ✦β ✢(α → β) ◗ (4) (1) ✦(2) (3) . 4
P的公理 (A1)(a→(B→a)) (A2)(a→(3→)→(a→8)→(a→) (A3)((-a)→(/)→(→a)
P (A1) (α→(β→α)) (A2) (α→(β→γ))→((α→β)→(α→γ))! (A3) (((¬ α)→(¬ β))→(β→α)) 5
P的推理规则 分离规则:由a、(α→β)可得到3 (M) 分离规则( Modus ponens)又记为(MP
P ✧✜α ✦(α→β) β. (M). (Modus Ponens) (MP). 6
注记 形式系统P又称为希尔伯特型(D. Hilbert)系统* 分清P的定义中的元语言与对象语言。 P的形式语言是N的形式语言子语言。 关于N的注记同样适用于P,如括号省略规则。 关于形式系统的多样性请参见 1.王宪钧,数理逻辑引论,北大出版社,1982 2.沈百英,数理逻辑,国防工业出版社,1991
• P (D.Hilbert) ∗ • P ✤ • P N ✤ • N P ✢✤ ∗❘❙❄❅❚❯✪❱❲❁❳❨❩: 1. ❬❭❪❂❫❴❵❛❜❝, ❞❡❢❣❤❂1982 2. ✐❥❦❂❫❴❵❛❂❧♠♥♦❢❣❤❂1991 7
P的公理的简写 (A1)a→(B→a (A2)(a→(→)→(→6)→(a→7) (A3)((=a)→(=)→(→a)
P (A1) α→(β→α) (A2) (α→(β→γ))→((α→β)→(α→γ)) (A3) ((¬ α)→(¬ β))→(β→α) 8
在形式系统P中可以做什么 例20 (1)a→(→a) (A1) (2)(a→(→a)→ (→)→(a→a)(42) (3)(a→6)→(a→a) (M)(1)(2)
P ? 20 (1) α→(β→α) (A1) (2) (α→(β→α))→ ((α→β)→(α→α)) (A2) (3) (α→β)→(α→α) (M)(1)(2) 9
