Download presentation
Presentation is loading. Please wait.
1
离散数学(5) 陈斌
2
目录 数理逻辑 集合论 图论 抽象代数
3
数理逻辑 命题演算 谓词演算 命题与联结词 重言式 范式 命题演算形式系统 个体、谓词和量词 谓词演算永真式 谓词公式的前束范式
一阶谓词演算形式系统
4
上次我们讲到…… 个体、谓词和量词 谓词公式和永真式 谓词演算形式系统FC
5
谓词演算:自然推理系统ND FC和PC一样,证明和演绎过程都过于复杂 人们常常在推理中使用各种假设
追求简洁,只用两个联结词、一个量词和一条推理规则 如果能够引入更多的联结词、量词、推理规则,那么证明和演绎过程会显得更自然 人们常常在推理中使用各种假设 为了证明A→B,常假设A成立,如果能够证明B成立,则完成了A→B的证明; 为了证明A,常假设¬A,如果导出矛盾(假命题f),则A成立; 已知A∨B,要证明C,常假设A和B成立分别证明C,如果都能成功,则完成C的证明
6
谓词演算:自然推理系统ND 人们常常在推理中使用各种假设 自然推理系统(Natural Deduction)
已知vA(v),要证明与v无关的C,常假设A(v0),如果能够证明C,则完成C的证明 在形式系统中引入带假设的推理规则,能够使推理过程更加接近人的思维,更加高效和便捷 自然推理系统(Natural Deduction) 采用5个联结词,2个量词 少数公理,更多的规则,引入假设 用推理规则体现人的推理手段
7
谓词演算:自然推理系统ND ND的符号系统 ND的公理 ND的推理规则(18个) 引入5个联结词、2个量词 Γ; A┠A(Γ是公式集合)
假设引入规则 Γ┠B Γ; A┠B(源于重言式B→(A→B))
8
谓词演算:自然推理系统ND ND的推理规则(18个) 假设消除规则 ∨引入规则 ∨引入规则(加强形式) Γ; A┠B,Γ; ¬A┠B
Γ┠B(源于重言式¬A→(A→B)) 推理中的分情况证明 ∨引入规则 Γ┠A Γ┠A∨B(源于重言式A→(A∨B)) ∨引入规则(加强形式) Γ; ¬B┠A Γ┠A∨B(源于重言式(¬B→A)↔(B∨A))
9
谓词演算:自然推理系统ND ND的推理规则 ∨消除规则 ∧引入规则 ∧消除规则 Γ; A┠C,Γ; B┠C,Γ┠A∨B
Γ┠C(源于重言式(A∨B)∧(A→C)∧(B→C)→C) ∧引入规则 Γ┠A,Γ┠B Γ┠A∧B ∧消除规则 Γ┠A
10
谓词演算:自然推理系统ND ND的推理规则 →引入规则 →消除规则 ¬引入规则 ¬引入规则(2) Γ; A┠B Γ┠ A→B(即演绎定理)
Γ; A┠f Γ┠ ¬A(反证法)
11
谓词演算:自然推理系统ND ND的推理规则 ¬消除规则 ¬¬引入规则 ¬¬消除规则 Γ┠A, Γ┠ ¬A
Γ┠B(虚假的前提可以蕴涵任何结论) ¬¬引入规则 Γ┠ A Γ┠ ¬ ¬A ¬¬消除规则
12
谓词演算:自然推理系统ND ND的推理规则 ↔引入规则 Γ┠A→B,Γ┠B→A Γ┠A↔B ↔消除规则 Γ┠A→B
13
谓词演算:自然推理系统ND ND的推理规则 引入规则 引入规则(2) 消除规则 Γ┠ A Γ┠ vA(v在A中无自由出现,FC公理)
Γ┠ vA(v)(v在Γ中无自由出现,全称引入规则) 消除规则 Γ┠ vA(v) Γ┠ A(t/v)(t对v可代入) 源于FC的公理A4:xA(x)→A(t/x)
14
谓词演算:自然推理系统ND ND的推理规则 引入规则 消除规则 Γ┠ A(t)
Γ┠ vA(v/t)(源于永真式A(t)→vA(v/t)) 消除规则 Γ┠ vA(v),Γ; A(e/v)┠C Γ┠C
15
谓词演算:自然推理系统ND 演绎结果 在ND中,称A为Γ的演绎结果,即Γ┠NDA简记为Γ┠A,如果存在如下序列:
(Γ=Γ1)Γ1┠A1, Γ2┠A2, …, Γn┠An(Γn=Γ,An=A) 使得Γi┠Ai (1≤i≤n) 或者是公理; 或者是Γj┠Aj (j<i) 或者是对Γj1┠Aj1,…, Γjk┠Ajk(j1,…,jk<i)使用推理规则导出的 如果有Γ┠A,且Γ=ø,则称A为ND的定理
16
谓词演算:自然推理系统ND 证明定理:A∨¬A (1) A┠A;公理 (2) A┠A∨¬A; ∨引入规则(1) (3) ¬A┠ ¬A;公理
17
谓词演算:自然推理系统ND 证明定理: x(A(x)→B(x))→(xA(x)→xB(x))
(1) x(A(x)→B(x)), xA(x)┠xA(x);公理 (2) x(A(x)→B(x)), xA(x)┠A(x);消除规则(1) (3) x(A(x)→B(x)), xA(x)┠x(A(x)→B(x));公理 (4) x(A(x)→B(x)), xA(x)┠A(x)→B(x); 消除规则(3) (5) x(A(x)→B(x)), xA(x)┠B(x);→消除规则(2)(4) (6) x(A(x)→B(x)), xA(x)┠xB(x); 引入规则(5) (7) x(A(x)→B(x))┠xA(x)→xB(x);→引入规则(6) (8)┠x(A(x)→B(x))→(xA(x)→xB(x)) ;→引入规则(7)
18
谓词演算:自然推理系统ND ND的重要性质 FC的公理和定理都是ND的定理 ND是合理的、一致的、完备的
19
数理逻辑作业 请分别从初等几何和高等数学中找两个定理,将定理的证明过程形式化为自然推理系统ND中的演绎过程。 确定原子命题、谓词
运用推理规则 有可能的话,应该引入一些公理 形式化是否适当 每个证明步骤都有明确的依据
20
数理逻辑作业 命题逻辑和现代计算机的原理有非常密切的关系,如:2位加法器 请你写出2位加法器所有真值函数的主析取范式 每个端子取值0或1
输入二进制数x1x2,y1y2 输出二进制和f1f2 以及输出进位标志f3 例如:输入10,11,输出01,进位标志1 其中x1=1,x2=0,y1=1,y2=1,f1(x1,x2,y1,y2)=0 一个2位加法器可以看作3个4元真值函数 请你写出2位加法器所有真值函数的主析取范式 x1 x2 y1 y2 f1 f2 f3
21
数理逻辑作业 如果有下面三种部件(门电路) 与门,或门,非门 部件的输出端可以接到另一个部件的输入端 非门 与门 或门
22
数理逻辑作业 门电路的连接 f= (¬p∧q)∨(q∨r) g= ¬(q∨r) 你能设计出最简洁的2位加法器电路吗? p q r f g
23
下次我们讲…… 集合论概论 集合论基本概念
24
关于课程教材 [O158/75]计算机科学中的离散结构 [O158/60]离散数学导论 [O158/36]离散数学
王元元, 张桂芸编著,机械工业出版社 2004 [O158/60]离散数学导论 王元元, 张桂芸编著,科学出版社 2002 [O158/36]离散数学 王元元,李尚奋编著,科学出版社 1994
25
END 特殊符号表 ∴,∵,╞═╡,╞═,∈,≠,∑,↓,∪,∩,╞,┠PC
αΑ,βΒ,γΓ,δΔ,εΕ,ζΖ,ηΗ,θΘ,ιΙ,κΚ,λΛ,μΜ,νΝ,ξΞ,οΟ,πΠ,ρΡ,ς,σΣ,τΤ,υΥ,φΦ,χΧ,ψΨ,ωΩ {¬,∧,∨,→,↔} ≦≧≠≤ø
Similar presentations