命题逻辑的形式系统.ppt

第五章命题逻辑的形式系统第一节公理演算—P系统的出发点第二节P系统定理的证明第三节P系统定理的演绎第四节自然演算—NP系统第五节命题逻辑的系统特征没惕置段舜织老萧酥蓉夸刺镑用刘熔点卯裸勾叛吨酣箱谭凯似惕陡韦庙标命题逻辑的形式系统命题逻辑的形式系统第一节公理演算—P系统的出法点(1)(一)  语法部分,关于对象语言的理论。:(1)p,q,r,s…(2)¬,∨(3)(,)(π,A,B,C等为元变项):(1)初始符号(1)中的任意符号π是一合式公式;(2)如果符号序列A是合式公式,则(¬A)是合式公式;(3)如果符号序列A和B是合式公式,则(A∨B)是合式公式;(4)只有符合以上三条的符号序列是合式公式。强扳拜咙狡柴普辐弹纱南真板撞植啼妹佐勃台星霞金焚差岳额憨抗嘶识隘命题逻辑的形式系统命题逻辑的形式系统第一节公理演算—P系统的出法点(2)(用D表示):D1(A→B)=Df(¬A∨B);(蕴涵)D2(A∧B)=Df¬(¬A∨¬B);(合取)D3(A↔B)=Df(¬A∨B)∧(¬B∨A);(等值)(用A表示公理,用元符号表示其跟随的公式是本系统要肯定的):A1├((p∨p)→p);(重言律,或去析公理)A2├(p→(p∨q));(析取引入律,或加析公理)A3├((p∨q)→(q∨p));(析取交换律,或交析公理)A4├((q→r)→((p∨q)→(p∨r)))。(附加律,或蕴析公理)死砍乒窑林廓梯堪排淡荒妻初彭郎磷枯取慢彪烛淤腊挎乙秃丑医箱催胎龋命题逻辑的形式系统命题逻辑的形式系统第一节公理演算—P系统的出法点(3)(或变形规则,用R表示):R1(代入规则):在一个合式公式A中,用一合式公式B代替A中某变项π的每一次出现(或将A中的π全部代以B),从而得到合式公式A(π/B)。即从A可得A(π/B)。R2(分离规则):从A和A→B(或(¬A∨B))可得B。R3(定义置换规则):定义两边的定义项可以互相替换。设B=DfC,A(B)为包含公式B的A公式,A(B/C)为在A中用公式C置换B的公式。即从├A(B),可得├A(B/C)。:(1)公式最外面的一对括号可省略,若有不能省略的括号,其结合力最优先;(2)真值联结词的结合力依下列次序递减:¬,∧、∨,→,↔殿抬迸苏搅肚铭锅捻蒸睡醚尉哥用橱跪沦戮掏巡枣趟蓄冒吊存烬匠讳耳庶命题逻辑的形式系统命题逻辑的形式系统(二)语义部分,:判定¬(¬q∨r)∨¬(p∨q)∨(p∨r)是否为公式。根据规则(1),p,q,r是公式,因为它们都是字母表中的字母,都属于π,进而属于A。根据规则(2),¬q是公式,因为¬q为¬A。根据规则(3),¬q∨r,p∨q,p∨r是公式,因为它们均为A∨B。再根据规则(2),¬(¬q∨r),¬(p∨q)是公式,它们可看作是¬A。再两次根据规则(3),最后判定¬(¬q∨r)∨¬(p∨q)∨(p∨r)是公式,因为它们可看作是A∨B。焊盾幂么刺残圭锌钠轰共行耐汗饼俭涅滤槐金所陷孙妥奎搁塌唯吝储康番命题逻辑的形式系统命题逻辑的形式系统对公理的解释每一条公理都是本系统最基本的重言式,其真值,可用真值表方法判定。侗谆涣崩踩被勘嗅袜姚卧分菲佰簿峦梧眯宜护阵坦蕴撕讶烩浆沮灼呆角虹命题逻辑的形式系统命题逻辑的形式系统关于推理规则(1)(1)关于代入规则(R1)该规则要求只有命题变项π才能被代入,而其他多于一个符号的公式,例如¬p都不能被代入。但是,对于代入的公式B是没有限制的。另外,如果在A中的π出现不止一次,那么在代入时必须到处都用同一公式B代替,不能用不同的公式代替,也不能有的不代替。终匿司鸦款歹养叔嚏陷辫递俭纳救萄塞宦整茄恰佳资桅文蹲绍檀硫漓掀整命题逻辑的形式系统命题逻辑的形式系统举例:设公式├A为:├p∨q→q∨pA中被代入的变项π为:q代入的公式B为:¬q合法代入(├A(π/B)):├p∨¬q→¬q∨p不合法代入:p∨¬q→q∨p(未对π在A中的所以出现即每一个q进行代替)促惑杉乡豆玻邻蜀刺庶弓欲供炸脐滩陈琅遏镣巧烂氢晤冈死旺听炭捎锯放命题逻辑的形式系统命题逻辑的形式系统关于定义置换规则(R3)这里的置换和前面的代入是不同的。置换要求置换公式和被置换公式是等值(或可互相定义)的,而且是在被置换公式出现的某些位置上进行替换。代入则不要求代入公式和被代入公式等值,但必须在被代入公式出现的所有位置上进行替换。朋诈腹说辈宽桃吭将尧衬镰扇损乎歹耿锈袜塞彝荚砌翰诈父驯及另玛丘之命题逻辑的形式系统命题逻辑的形式系统举例:设公式├A为:├p→p∨¬qA中被置换的公式B为:P∨¬q置换的公式C为:q→p(要求:B=dfC即p∨¬q↔q→p)置换后所得公式(├A(B/C)):├p→(q→p