1主要内容一阶逻辑等值式与基本的等值式置换规则、换名规则、代替规则前束范式自然推理系统NL及其推理规则第五章一阶逻辑等值演算与推理25.1一阶逻辑等值式与置换规则定义5.1设A,B是两个谓词公式,如果AB是永真式,则称A与B等值,记作AB,并称AB是等值式基本等值式第一组命题逻辑中16组基本等值式的代换实例例如,xF(x)xF(x),xF(x)yG(y)xF(x)yG(y)等第二组(1)消去量词等值式设D={a1,a2,…,an}①xA(x)A(a1)A(a2)…A(an)②xA(x)A(a1)A(a2)…A(an)3基本等值式(2)量词否定等值式①xA(x)xA(x)②xA(x)xA(x)(3)量词辖域收缩与扩张等值式.A(x)是含x自由出现的公式,B中不含x的自由出现关于全称量词的:①x(A(x)B)xA(x)B②x(A(x)B)xA(x)B③x(A(x)B)xA(x)B④x(BA(x))BxA(x)4基本等值式关于存在量词的:①x(A(x)B)xA(x)B②x(A(x)B)xA(x)B③x(A(x)B)xA(x)B④x(BA(x))BxA(x)(4)量词分配等值式①x(A(x)B(x))xA(x)xB(x)②x(A(x)B(x))xA(x)xB(x)注意:对,对无分配律5置换规则、换名规则、代替规则1.置换规则设(A)是含A的公式,那么,若AB,则(A)(B).2.换名规则设A为一公式,将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号,其余部分不变,设所得公式为A,则AA.3.代替规则设A为一公式,将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替,其余部分不变,设所得公式为A,则AA.6实例例1将下面命题用两种形式符号化,并证明两者等值:(1)没有不犯错误的人解令F(x):x是人,G(x):x犯错误.x(F(x)G(x))或x(F(x)G(x))x(F(x)G(x))x(F(x)G(x))量词否定等值式x(F(x)G(x))置换x(F(x)G(x))置换7实例(2)不是所有的人都爱看电影解令F(x):x是人,G(x):爱看电影.x(F(x)G(x))或x(F(x)G(x))x(F(x)G(x))x(F(x)G(x))量词否定等值式x(F(x)G(x))置换x(F(x)G(x))置换8实例例2将公式化成等值的不含既有约束出现、又有自由出现的个体变项:x(F(x,y,z)yG(x,y,z))解x(F(x,y,z)yG(x,y,z))x(F(x,y,z)tG(x,t,z))换名规则xt(F(x,y,z)G(x,t,z))辖域扩张等值式或者x(F(x,y,z)yG(x,y,z))x(F(x,u,z)yG(x,y,z))代替规则xy(F(x,u,z)G(x,y,z))辖域扩张等值式9实例例3设个体域D={a,b,c},消去下述公式中的量词:(1)xy(F(x)G(y))解xy(F(x)G(y))(y(F(a)G(y)))(y(F(b)G(y)))(y(F(c)G(y)))((F(a)G(a))(F(a)G(b))(F(a)G(c)))((F(b)G(a))(F(b)G(b))(F(b)G(c)))((F(c)G(a))(F(c)G(b))(F(c)G(c)))10实例解法二xy(F(x)G(y))x(F(x)yG(y))辖域缩小等值式x(F(x)G(a)G(b)G(c))(F(a)G(a)G(b)G(c))(F(b)G(a)G(b)G(c))(F(c)G(a)G(b)G(c))11实例(2)xyF(x,y)xyF(x,y)x(F(x,a)F(x,b)F(x,c))(F(a,a)F(a,b)F(a,c))(F(b,a)F(b,b)F(b,c))(F(c,a)F(c,b)F(c,c))125.2一阶逻辑前束范式定义5.2设A为一个一阶逻辑公式,若A具有如下形式Q1x1Q2x2…QkxkB则称A为前束范式,其中Qi(1ik)为或,B为不含量词的公式.例如,x(F(x)G(x))xy(F(x)(G(y)H(x,y)))是前束范式而x(F(x)G(x))x(F(x)y(G(y)H(x,y)))不是前束范式,13前束范式存在定理定理5.1(前束范式存在定理)一阶逻辑中的任何公式都存在与之等值的前束范式例4求下列公式的前束范式(1)x(M(x)F(x))解x(M(x)F(x))x(M(x)F(x))(量词否定等值式)x(M(x)F(x))后两步结果都是前束范式,说明公式的前束范式不惟一.14求前束范式的实例(2)xF(x)xG(x)解xF(x)xG(x)xF(x)xG(x)(量词否定等值式)x(F(x)G(x))(量词分配等值式)或xF(x)xG(x)xF(x)xG(x)量词否定等值式xF(x)yG(y)换名规则xy(F(x)G(y))辖域收缩扩张规则15求前束范式的实例(3)xF(x)y(G(x,y)H(y))或xF(x)y(G(z,y)H(y))代替规则xy(F(x)(G(z,y)H(y)))解xF(x)y(G(x,y)H(y))zF(z)y(G(x,y)H(y))换名规则zy(F(z)(G(x,y)H(y)))辖域收缩扩张规则165.3一阶逻辑的推论理论推理的形式结构1.A1A2AkB若次式是永真式,则称推理正确,记作A1A2AkB2.前提:A1,A2,,Ak结论:B推理定理:永真式的蕴涵式17推理定理第一组命题逻辑推理定理的代换实例如,xF(x)yG(y)xF(x)第二组基本等值式生成的推理定理如,xF(x)xF(x),xF(x)xF(x)xF(x)xF(x),xF(x)xF(x)第三组其他常用推理定律(1)xA(x)xB(x)x(A(x)B(x))(2)x(A(x)B(x))xA(x)xB(x)(3)x(A(x)B(x))xA(x)xB(x)(4)x(A(x)B(x))xA(x)xB(x)18量词消去引入规则1.全称量词消去规则(-)或其中x,y是个体变项符号,c是个体常项符号,且在A中x不在y和y的辖域内自由出现.2.全称量词引入规则(+)其中x是个体变项符号,且不在前提的任何公式中自由出现xA(x)A(y)xA(x)A(c)A(x)xA(x)19量词消去引入规则3.存在量词消去规则(-)其中x是个体变项符号,且不在前提的任何公式和B中自由出现A(x)BxA(x)B20量词消去引入规则4.存在量词引入消去规则(+)或或其中x,y是个体变项符号,c是个体常项符号,且在A中y和c不在x和x的辖域内自由出现.BA(y)BxA(x)BA(c)BxA(x)A(y)xA(x)A(c)xA(x)21自然推理系统NL定义5.3自然推理系统NL定义如下:1.字母表.同一阶语言L的字母表2.合式公式.同L的合式公式3.推理规则:(1)前提引入规则(2)结论引入规则(3)置换规则(4)假言推理规则(5)附加规则(6)化简规则(7)拒取式规则22自然推理系统NL(8)假言三段论规则(9)析取三段论规则(10)构造性二难推理规则(11)合取引入规则(12)-规则(13)+规则(14)-规则(15)+规则推理的证明23构造推理证明的实例例5在自然推理系统NL中构造下面推理的证明,取个体域R:任何自然数都是整数.存在自然数.所以,存在整数.解设F(x):x是自然数,G(x):x是整数.前提:x(F(x)G(x)),xF(x)结论:xG(x)证明:①x(F(x)G(x))前提引入②F(x)G(x)①-③F(x)xG(x)②+④xF(x)xG(x)③-⑤xF(x)前提引入⑥xG(x)④⑤假言推理24构造推理证明的实例例6在自然推理系统NL中构造下面推理的证明,取个体域R:不存在能表示成分数的无理数.有理数都能表示成分数.所以,有理数都不是无理数.解设F(x):x是无理数,G(x):x是有理数,H(x):x能表示成分数.前提:x(F(x)H(x)),x(G(x)H(x))结论:x(G(x)F(x))证明:①x(F(x)H(x))前提引入②x(F(x)H(x))①置换③x(F(x)H(x))②置换④F(x)H(x)③-25构造推理证明的实例⑤x(G(x)H(x))前提引入⑥G(x)H(x)⑤-⑦H(x)F(x)④置换⑧G(x)F(x)⑥⑦假言三段论⑨x(G(x)F(x))⑧+26重要提示yxyxF:),(要特别注意使用-、+、-、+规则的条件.反例1.对A=xyF(x,y)使用-规则,推得B=yF(y,y).取解释I:个体域为R,在I下A被解释为xy(xy),真;而B被解释为y(yy),假原因:在A中x自由出现在y的辖域F(x,y)内反例2.前提:P(x)Q(x),P(x)结论:xQ(x)取解释I:个体域为Z,在I下前提为真,结论为假,从而推理不正确整除被是偶数2:)(,:)(xxQxxP27反例2(续)“证明”:①P(x)Q(x)前提引入②P(x)前提引入③Q(x)①②假言推理④xQ(x)③+错误原因:在④使用+规则,而x在前提的公式中自由出现.28第五章习题课主要内容一阶逻辑等值式基本等值式,置换规则、换名规则、代替规则前束范式推理的形式结构自然推理系统NL推理定律、推理规则29基本要求深刻理解并牢记一阶逻辑中的重要等值式,并能准确而熟练地应用它们.熟练正确地使用置换规则、换名规则、代替规则.熟练地求出给定公式的前束范式.深刻理解自然推理系统NL的定义,牢记NL中的各条推理规则,特别是注意使用、+、+、4条推理规则的条件.能正确地给出有效推理的证明.30练习12a1.给定解释I如下:(1)个体域D={2,3}(2)(3)(4)求下述在I下的解释及其真值:xy(F(f(x))G(y,f(a)))2)3(,3)2(:)(ffxf0)3,3(,1)2,3()3,2()2,2(:),(1)3(,0)2(:)(GGGGyxGFFxF解xF(f(x))yG(y,f(a))F(f(2))F(f(3))(G(2,f(2))G(3,f(2)))10(10)031练习22.求下述公式的前束范式:xF(x)y(G(x,y)H(x,y))解使用换名规则,xF(x)y(G(x,y)H(x,y))zF(z)y(G(x,y)H(x,y))z(F(z)y(G(x,y)H(x,y))zy(F(z)(G(x,y)H(x,y)))使用代替规则xF(x)y(G(x,y)H(x,y))xF(x)y(G(z,y)H(z,y))x(F(x)y(G(z,y)H(z,y))xy(F(x)(G(z,y)H(z,y)))32练习33.构造下面推理的证明:(1)