离散数学(3)省公开课一等奖全国示范课微课金奖

离散数学(3)陈斌gischen@2010.09.23第1页目录数理逻辑集合论图论抽象代数第2页数理逻辑命题演算命题与联结词重言式范式命题演算形式系统谓词演算个体、谓词和量词谓词演算永真式谓词公式前束范式一阶谓词演算形式系统第3页上次我们讲到……几个命题公式重言式、矛盾式、可满足式逻辑等价、逻辑蕴含重言式代入原理命题公式替换原理析（合）取范式、主析（合）取范式联结词（极小）功效完备集第4页命题演算：形式系统重言式反应了人类逻辑思维基本规律排中律A∨¬A╞╡t矛盾律A∧¬A╞╡f假言推理A∧(A→B)╞B归谬推理(A→B)∧¬B╞¬A穷举推理(A∨B)∧(A→C)∧(B→C)╞C真值计算、以代入原理、替换原理进行推演难以反应人类思维推理过程，需要建立严密符号推理体系第5页命题演算：形式系统形式系统是一个符号体系系统中概念由符号表示推理过程即符号变换过程以若干最基本重言式作为基础，称作公理（axioms）系统内符号变换依据是若干确保由重言式导出重言式规则，称作推理规则（rulesofinference）公理和推理规则确保系统内由正确前提总能得到正确推理结果第6页命题演算：证实与演绎证实(proof)公式序列A1,A2,…,Am称作Am一个证实，假如Ai(1≤i≤m)或者是公理，或者由Aj1,…,Ajk(j1,…,jk<i)用推理规则推得。当这么证实存在时，称Am为系统定理(theorem)，记作┠*Am（*是形式系统名称），或者简记为┠Am第7页命题演算：证实与演绎演绎(deduction)设Γ为一公式集合。公式序列A1,A2,…,Am称作Am以Γ为前提演绎，假如Ai(1≤i≤m)或者是Γ中公式，或者是公理，或者由Aj1,…,Ajk(j1,…,jk<i)用推理规则推得。当有这么演绎时，Am称作Γ演绎结果，记作Γ┠*Am（*是形式系统名称），或者简记为Γ┠Am称Γ和Γ组员为Am前提(hypothesis)证实是演绎在Γ为空集时特例第8页命题演算：形式系统PC命题演算形式系统PC(PropositionCalculus)PC符号系统命题变元：p,q,r,s,p1,q1,r1,s1,…命题常元：t,f联结词：¬,→（注意是完备集）括号：(,)命题公式命题变元和命题常元是公式假如A,B是公式，则(¬A)，(A→B)均为公式（结合优先级和括号省略约定同前）只有有限次使用上面两条规则得到符号串才是命题公式第9页命题演算：形式系统PCPC公理（A,B,C表示任意公式）A1:A→(B→A)A2:(A→(B→C))→((A→B)→(A→C))A3:(¬A→¬B)→(B→A)PC推理规则（A,B表示任意公式）A,A→B/B（分离规则）第10页命题演算：形式系统PCPC合理性(soundness)假如公式A是系统PC定理，则A是重言式（假如┠PCA，则╞A）假如A是公式集合Γ演绎结果，那么A是Γ逻辑结果（假如Γ┠PCA，则Γ╞A）PC合理性证实PC中公理A1,A2,A3都是重言式；PC分离规则是“保真”，就是假如A真，A→B真，总有B真。这么，由公理和规则导出全部定理都是重言式由Γ、公理和规则导出公式，在Γ中公式都为真时也为真第11页命题演算：形式系统PCPC一致性(consistency)没有公式A，使得┠PCA和┠PC¬A同时成立由PC合理性轻易证实PC完备性(completeness)假如公式A是重言式，则A一定是PC中定理（假如╞A，则┠PCA）假如公式A是公式集合Γ逻辑结果，则A一定是Γ演绎结果（假如Γ╞A，则Γ┠PCA）证实极难，略。第12页命题演算：形式系统PC证实定理：┠PCA→A1](A→((A→A)→A))→((A→(A→A))→(A→A))：公理A22]A→((A→A)→A)：公理A13](A→(A→A))→(A→A)：对1,2使用分离规则4]A→(A→A)：公理A15]A→A：对3,4使用分离规则第13页命题演算：形式系统PC证实：{A,B→(A→C)}┠B→C1]A：前提2]B→(A→C)：前提3]A→(B→A)：公理A14]B→A：对1,3用分离规则5](B→(A→C))→((B→A)→(B→C))：公理A26](B→A)→(B→C)：对2,5用分离规则7]B→C：对4,6用分离规则第14页命题演算：形式系统PC演绎定理对任意公式集合Γ和公式A,B，Γ┠A→B当且仅当Γ∪{A}┠B当Γ=ø时，┠A→B当且仅当{A}┠B，或A┠B归谬定理对任何公式集合Γ和公式A,B，若Γ∪{¬A}┠B，Γ∪{¬A}┠¬B，那么Γ┠A穷举定理对任何公式集合Γ和公式A,B，若Γ∪{¬A}┠B，Γ∪{A}┠B，那么Γ┠B第15页命题演算：形式系统PC证实：┠¬¬A→A¬¬A→(¬A→¬¬A)：公理A1，由演绎定理证实了：{¬¬A,¬A}┠¬¬A¬A→(¬¬A→¬A)：公理A1，由演绎定理证实了：{¬A,¬¬A}┠¬A，也就是{¬¬A,¬A}┠¬A上面两个前提，用归谬定理得到{¬¬A}┠A再用演绎定理，有┠¬¬A→A第16页命题演算：形式系统PC证实：┠(A→C)→(((B→C)→((¬A→B)→C))依据演绎定理，只需要证实{A→C,B→C,¬A→B}┠C因为{A→C,B→C,¬A→B,A}┠C是显然{A→C,B→C,¬A→B,¬A}┠C是易证依据穷举定理{A→C,B→C,¬A→B}┠C得证第17页命题演算：定理判定问题一个形式系统本质上说是一个符号串集合形式系统定义就是符号串集合结构性定义符号体系要求了符号串可能包含字符（或字符正当组合模式，词）如PC中命题变元、常元和公式定义公理要求了几个集合中符号串（或者这种符号串模式）如PC中公理，实质是公理模式推理规则要求了从集合中已知符号串转换生成集合中其它符号串方法如PC中分离规则第18页命题演算：定理判定问题形式系统中定理本质上就是在集合中符号串定理证实过程就是符号串结构过程这个过程需要在有限步内结束定理判定问题给定一个符号串，判定是否形式系统中定理能否单靠形式系统本身公理和推理规则在有限步骤内判定定理和非定理？第19页命题演算：定理判定问题例子：一个简单形式系统MIU符号系统：M,I,U组成串初始串：MI公理：MI规则1：假如串最终一个符号是I，则能够加上一个U假如xI是定理，那么xIU也是定理规则2：假如串符合Mx，则能够再加上x而生成Mxx，x代表任何一个由M,I,U组成串假如Mx是定理，那么Mxx也是定理第20页命题演算：定理判定问题一个简单形式系统MIU规则3：假如串中出现连续3个I，则能够用U代替III得到新串假如xIIIy是定理，那么xUy也是定理规则4：假如串中出现UU，则能够将UU删去得到新串假如xUUy是定理，那么xy也是定理判定问题：MU是否系统中串？MU是否定理？第21页命题演算：定理判定问题一个简单形式系统MIU由公理和推理规则，我们轻易结构定理树MIMIUMII12MIUIUMIUIUIUIU22MIIUMIIUIIU12MIIIIMIIIIUMIIIIIIIIMUIMIU1233MU??????2第22页命题演算：定理判定问题一个简单形式系统MIU用结构系统中全部定理方法并不能确保在有限步骤内能够判定定理到底MU是不是定理？我们需要利用同构机制求援于系统之外自然数运算定律第23页命题演算：定理判定问题MIU一个同构M对应3，I对应1，U对应0自然数31在集合中规则1：假如集合中有数以1结尾，则添一个0也是集合中数规则2：假如集合中有数以3开始，则把3后面数再重复一次添在末尾也是集合中数规则3：假如集合中有数包含111，则把111替换成0也是集合中数规则4：假如集合中有数包含00，则去掉00数也是集合中数问：30是不是集合中数？第24页命题演算：定理判定问题MIU一个同构经过分析数结构规则，我们发觉集合中数都不可能被3整除31不能被3整除规则1～4都不能从不能被3整除数生成能被3整除数30能够被3整除，所以30不属于这个集合结论：MU不是MIU系统中定理第25页命题演算：定理判定问题形式系统PC定理判定问题一个符合PC符号体系定义命题公式，是否是PC中定理？一样，用PC系统中公理和分离规则不能确保能在有限步骤判定一个命题公式是否定理不过，PC有一个非常主要同构：真值函数运算系统只需要用真值表判定命题公式对应真值函数是否重言式，即可判定是否PC中定理，真值表运算是有限步骤能够完成。（注意：真值表并不是PC中成份）第26页下次我们讲……谓词演算个体、谓词和量词谓词公式永真式一阶谓词演算形式系统FC自然推理系统ND第27页关于课程教材[O158/75]计算机科学中离散结构王元元,张桂芸编著，机械工业出版社[O