谓词演算的推理理论-永真推理系统

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,第四章 谓词演算的推理理论,4.1,谓词演算的永真推理系统,4.1.1,公理系统的组成部分,4.1.2,公里系统的推理过程,4.2,谓词演算的假设推理系统,4.3,谓词演算的归结推理系统,4.1.1,公理系统的组成部分,一、语法部分,(,一,),基本符号,(,二,),公理,(,三,),规则,二、语义部分,三、关于公理的几点说明,（一）基本符号,公理系统所允许出现的全体符号的集合。,(1),命题变元：,P,，,Q,，,R,，,等字母表示命题变元,(2),个体变元：,x,，,y,，,等小写字母表示个体变元,(3),谓词变元：,X,，,Y,，,等大写字母表示谓词变元,(4),联结词：,、,、,、,、,是联结词,(5),量词：全称量词,、存在量词,(6),括号：,(,，,),是括号,(7),全称封闭符：,基本符号（续）,(8),合式公式：,(i),原子命题,P,是合式公式；,(ii),谓词填式,A,(,x,1,，,x,2,，,x,3,，,，,xn,),是合式公式；,(iii),若,A,是公式，则,A,是合式公式；,(iv),若,A,和,B,是合式公式，则,(,A,B,),，,(,A,B,),，,(,A,B,),，,(,A,B,),为公式；,(v),若,A,是合式公式，,x,是,A,中出现的任何个体变元，则,xA,(,x,),，,xA,(,x,),为合式公式；,(vi),只有有限次使用,(i),、,(ii),、,(iii),、,(iv),、,(v),所得到的式子才是合式公式。,基本符号（续）,(9),全称封闭式：设,为含有,n,个自由变元的公式，如果在,前用全称量词把,n,个自由变元约束起来后所得到的公式，称为,的,全称封闭式,。记为,。,例 写出下式的全称封闭式,=,xP,(x,，,y),uQ,(u,，,v),解：,=,(,xP,(x,，,y,),uQ,(u,，,v,),=,y,v,(,xP,(x,，,y),uQ,(u,，,v),（二）公理,公理,1 (P,P),公理,2 (P,(Q,R),(Q,(P,R),公理,3 (P,Q),(Q,R),(P,R),公理,4 (P,(P,Q),(P,Q),公理,5 (P,Q),(P,Q),公理,6 (P,Q),(Q,P),公理,7 (P,Q),(Q,P),(P,Q),调头,传递,凝缩,与,有关,（二）,公理,公理,8 (P,Q),P),公理,9 (P,Q),Q),公理,10 (P,(Q,(P,Q),公理,11 (P,(P,Q),公理,12 (Q,(P,Q),公理,13 (P,R),(Q,R),(P,Q),R),公理,14 (P,Q),(Q,P),公理,15 (,P,P),与,有关,与,有关,与,有关,（二）,公理,公理,20 (,xP(x),P(x),公理,21 (P(x),x P(x),如果只有一个自由变元，公理,20,与公理,21,可以分别理解如下：,x,(,y,P(y),P(x),x,(P(x),y P(y),与,量词有关,（三）规则,(1),分离规则：,如果,(A,B),且,A,，则,B,。,(2),全称规则：,(,P(x)(,x P(x),(,其中,中不含自由的,x),(3),全称量词消去规则：,xP(x)P(x),(x,可以为任意的变元,),(4),存在量词引入规则：,(P(x),)(,x P(x),),(,其中,中不含自由的,x),回顾,:,量词作用域的收缩与扩张,设公式,中不含有自由的,x,，则下面的公式成立,:,x(,(x),)=(,x,(x),),x(,(x)=(,x,(x),x(,(x),)=(,x,(x),),x(,(x)=(,x,(x),存在量词引入,全称量词引入,二、语义部分,(1),公理是永真公式。,(2),规则规定如何从永真公式推出永真公式。,分离规则指明，如果,(,A,B,),永真且,A,永真，则,B,也为永真公式。,(3),定理为永真公式，它们是从公理出发利用上述规则推出来的公式。,三、关于公理的几点说明,(1),本系统中,不引入代入规则,，它的作用由下面的,(2),来实现；,(2),本系统中的所有公理我们把它看作,公理模式,，即只要形如某一公理，我们就称其为某一公理。,如,(P,P),、,(P,(Q,R),(P,(Q,R),、,(,xP(x),x P(x),等均为公理,1,。,第四章 谓词演算的推理理论,4.1,谓词演算的永真推理系统,4.1.1,公理系统的组成部分,4.1.2,公里系统的推理过程,4.2,谓词演算的假设推理系统,4.3,谓词演算的归结推理系统,例,1,(p41),已知,定理,(P,(,Q,P,),求证,:,全,0,规则,(,x,),x,(,x,),证明：,(1),(,x),(2)(,(,x),(,P,P,),(,x),引用定理,(3)(P,P,),(,x),(2)(1),分离,(4)(P,P,),x,(,x),全称规则,(3),(5)(P,P,),公理,(1),(6),x,(,x),(4)(5),分离,则有全,0,规则,(,x,),x,(,x,),全,n,规则、存,n,规则,全,n,规则：,(,1,(,2,(,n,(x),(,1,(,2,(,n,x,(x),存,n,规则：,(,1,(,2,(,n,(,(x),),(,1,(,2,(,n,(,x,(x),),全,1,规则,=,全称规则,存,0,规则,=,存在规则,例 试利用存,0,规则求证存,1,规则,(,1,(,(x),)(,1,(,x(x),),证明：,(1),(,1,(,(x),),(2),(,1,(,(x),),(,(x),(,1,),公理,2,(3),(,(x),(,1,),分离,(1)(2),(4),(,x,(x),(,1,),存,0,规则,(5),(,x,(x),(,1,),(,1,(,x,(x),),公理,2,(6),(,1,(,x,(x),),),分离,(5)(6),两次运用调头公理,2,例,(,练习,4.1(1),),x,(,P,(,x,),(,xP,(,x,),证明,:,x,(,P,(,x,),(,P,(,x,),),公理,20:,P,(,x,),与,P,(,x,),同形,(2),x,(,P,(,x,),(,x,P,(,x,),),全,2,规则,(,1,(,2,(x)(,1,(,2,x,(x),例,(,续,),x,(,P,(,x,),(,x P,(,x,),再证明,(,x,P,(,x,),x,(,P,(,x,),),证明,:,(3),xP,(,x,),P,(,x,),公理,20,(4),(,xP,(,x,),P,(,x,),),(,(,xP,(,x,),(,P,(,x,),定理,(5)(,xP,(,x,),(,P,(,x,),分离,(3)(4),(6),(,xP,(,x,),x,(,P,(,x,),全,1,规则,定理 ,(,(PQ)(R,P,),(R,Q,),例,(,再续,),x,(,P,(,x,),(,x P,(,x,),已经证得,(2)(6),两式,(2),x,(,P,(,x,),(,x,P,(,x,),(6),(,xP,(,x,),x,(,P,(,x,),于是,(7)(,x,(,P,(,x,),(,x,P,(,x,),),),(,(,(,xP,(,x,),x,(,P,(,x,),),(,x,(,P,(,x,),(,x P,(,x,),),),公理,7,(8),(,(,xP,(,x,),x,(,P,(,x,),),(,x,(,P,(,x,),(,x P,(,x,),),分离,(2)(7),(9),x,(,P,(,x,),(,x P,(,x,),分离,(6)(8),例,(,练习,4.1(2),),x,(,P,(,x,),),(,x P,(,x,),),先证明,x,(,P,(,x,),),(,x P,(,x,),),证明,:,(1),x,(,P,(,x,),),(,P,(,x,),),公理,20,(2),x,(,P,(,x,),),(,x,P,(,x,),),存,1,规则,1,(,P,(,x,),),1,(,x,P,(,x,),),例,(,续,),x,(,P,(,x,),),(,x P,(,x,),),再证明,(,x P,(,x,),),x,(,P,(,x,),),证明,:,(3)P(x),xP(x),公理,21,(4),(,P(x),xP(x),(,(xP(x)(P(x),),公理,3,(5),(xP(x)(P(x),分,(3)(4),(6),(xP(x),x,(P(x),全称规则,例,(,再续,),x,(,P,(,x,),),(,x P,(,x,),),已经证得,(2)(6),两式,(2),x,(,P,(,x,),),(,x P,(,x,),),(6),(xP(x)x(P(x),于是有,(7)(,x,(,P,(,x,),),(,x,P,(,x,),),(xP(x),x,(P(x),(,x,(,P,(,x,),),(,x P,(,x,),),公理,7,(8),(xP(x),x,(P(x),(,x,(,P,(,x,),),(,x P,(,x,),),分离,(2)(7),(9),x,(,P,(,x,),),(,x P,(,x,),),分离,(6)(8),例,(,练习,4.2),已知公理,(,A,)(,P,(,Q,P,),(,B,)(,P,P,),及分离规则和全称规则，全称规则为：,(,1,(,2,(,x)(,1,(,2,x,(,x),试证：全,0,规则 ,(,x,),x,(,x,),证,:(1),(,x,),(2)(,P,(,Q,P,),公理,A,(3)(,(x),(P,P),(x),代入,(1),(4)(P,P),(x)(1)(3),分离,(5)(P,P),(x),(P,P),(P,P),(x),代入,(2),(6)(P,P),(P,P),(x)(4)(5),分离,(7)(P,P),(P,P),x,(x),全称规则,(8)(,P,P,),公理,B,(9)(P,P),x,(x)(7)(8),分离,(10)(,x,(x)(9)(8),分离,例,2,(p42),试证明：,(A)(,x,P,(x),xP,(x),证,(A),(1),(,x,P,(x),P,(x),公理,20,(,x,P,(x),P,(x,)(,P(x),x,P,(x,),公理,14,(3)(,P(x),x,P,(x,),(2)(1),分离,(4)(,xP,(x),x,P,(x,),存在量词引入规则,(3),(,xP,(x),x,P(,x),(,x,P,(x),xP,(x,),公理,14,(6)(,x,P,(x),xP,(x,),(5)(4),分离,例,2,(p42),已知定理：,(P,Q,),(,Q,P,),试证明：,(B)(,xP,(x),x,P,(x),证,(B),(7)(P(x),xP,(x),公理,21,(8)(P(x),xP(,x),(,xP,(x),P,(x),已知定理,(9)(,xP(,x),P(,x),(8)(7),分离,(10)(,xP(,x),x,P(,x),全称规则,(9),例,2,(p42),试证明：,(,x,P,(x),xP,(x),证明：已经分别证出如下,(6)(10),两式,(,x,P,(x),xP,(x,),(10)(,xP(,x),x,P(,x,),(11)(,x,P(,x),xP(,x),(,xP(,x),x,P(,x,),(,x,P,(x),xP(,x,),公理,7,(12)(,xP(,x),x,P(,x),(,x,P,(x),xP(,x,),(11)(6),分离,(13)(,x,P(,x),xP(,x),(12)(10),分离,例,4,(p43),(,(,P,Q(x),),(,P,xQ,(x),),),证明：,(1)(Q(x),xQ,(x),公理,21,(2)(,(,P,Q,(,x),),(,