第第5 5章章 一阶逻辑等值演算与推理一阶逻辑等值演算与推理离散数学离散数学 2本章说明本章说明本章说明本章说明q本章的主要内容本章的主要内容一阶逻辑等值式与基本等值式一阶逻辑等值式与基本等值式置换规则、换名规则、代替规则置换规则、换名规则、代替规则前束范式前束范式一阶逻辑推理理论一阶逻辑推理理论q本章与其他各章的关系本章与其他各章的关系本章先行基础是前四章本章先行基础是前四章本章是集合论各章的先行基础本章是集合论各章的先行基础 3本章主要内容本章主要内容 5.1 5.1 一阶逻辑等值式与置换规则一阶逻辑等值式与置换规则5.2 5.2 一阶逻辑前束范式一阶逻辑前束范式5.3 5.3 一阶逻辑的推理理论一阶逻辑的推理理论 45.1 5.1 一阶逻辑等值式与置换规则一阶逻辑等值式与置换规则q在一阶逻辑中，有些命题可以有不同的符号化形式。在一阶逻辑中，有些命题可以有不同的符号化形式。q例如：没有不犯错误的人例如：没有不犯错误的人令令 M(x):xM(x):x是人。是人。 F(x):xF(x):x犯错误。犯错误。则将上述命题的符号化有以下两种正确形式：则将上述命题的符号化有以下两种正确形式：(1) (1) x(M(x)x(M(x)F(xF(x)(2)(2) x(M(x)F(xx(M(x)F(x)q我们称我们称(1)(1)和和(2)(2)是等值的。是等值的。说说明明 5等值式的定义等值式的定义定义定义5.15.1 设设A A，B B是一阶逻辑中任意两个公式，若是一阶逻辑中任意两个公式，若 A AB B是永是永真式，则称真式，则称A A与与B B是是等值等值的。的。记做记做A AB B，称，称 A AB B 是是等值式等值式。例如：例如：q判断公式判断公式A A与与B B是否等值，等价于判断公式是否等值，等价于判断公式A AB B是否为永真式。是否为永真式。q谓词逻辑中关于联结词的等值式与命题逻辑谓词逻辑中关于联结词的等值式与命题逻辑中相关等值式类似。中相关等值式类似。 说说明明 6一阶逻辑中的一些基本而重要等值式一阶逻辑中的一些基本而重要等值式q代换实例代换实例q消去量词等值式消去量词等值式 q量词否定等值式量词否定等值式 q量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式 q量词分配等值式量词分配等值式 7代换实例代换实例q由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式，因而第二章的真式，因而第二章的1616组等值式模式给出的代换实例都是组等值式模式给出的代换实例都是一阶逻辑的等值式的模式。一阶逻辑的等值式的模式。q例如：例如：(1)(1) xF(x) xF(x) xF(xxF(x) )（双重否定律）（双重否定律）(2)F(x)G(y) (2)F(x)G(y) F(x)G(yF(x)G(y) ) （蕴涵等值式）（蕴涵等值式）(3)(3) x(F(x)G(y) x(F(x)G(y) zH(zzH(z) ) x(F(x)G(y)x(F(x)G(y) zH(zzH(z) ) （蕴涵等值式）（蕴涵等值式） 8消消去量词等值式去量词等值式设个体域为有限集设个体域为有限集D=aD=a1 1,a,a2 2, ,a,an n,则有则有（1 1） xA(xxA(x) ) A(aA(a1 1)A(a)A(a2 2)A(aA(an n) ) （2 2） xA(xxA(x) ) A(aA(a1 1)A(a)A(a2 2)A(aA(an n) ) （5.15.1） 9量词否定等值式量词否定等值式设设A(xA(x) )是任意的含自由出现个体变项是任意的含自由出现个体变项x x的公式，则的公式，则（1 1） xA(xxA(x) ) xA(xxA(x) )（2 2） xA(xxA(x) ) xA(xxA(x) )说明说明q“并不是所有的并不是所有的x x都有性质都有性质A A”与与“存在存在x x没有没有性质性质A A”是一回事。是一回事。q”不存在有性质不存在有性质A A的的x x”与与”所有所有x x都没有性质都没有性质A A”是一回事。是一回事。（5.25.2） 10量词否定等值式(举例)q N N n (n ( nNnN |a|an n-a|-a|N n ( nN |a |an n-a|-a|N n ( nN |a |an n-a|-a|N ( nN |a |an n-a|-a|N ( nN |a |an n-a|-a|NnN |a|an n-a|-a|N n ( nN |a|an n-a|-a|N n ( nN |a|an n-a|-a| ) ) 12量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式设设A(xA(x) )是任意的含自由出现个体变项是任意的含自由出现个体变项x x的公式，的公式，B B中不含中不含x x的出现的出现，则，则（1 1） x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(BA(xx(BA(x) ) BB xA(xxA(x) )（2 2） x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(BA(xx(BA(x) ) BB xA(xxA(x) )（5.35.3）（5.45.4） 13量词辖域收缩与扩张(、续)q x x( (A(x)A(x)B B) ) xA(x)xA(x)B B 证明证明: : x(A(x)x(A(x)B B) ) x(x( A(x)A(x)B B) ) x x A(x)A(x)B B xA(x)xA(x)B B xA(x)xA(x)B Bq x x(B(BA(xA(x) ) ) B B xA(xxA(x) ) 证明证明: : x(Bx(BA(xA(x) x(x( B BA(xA(x) ) ) B B x xA(xA(x) ) B B x xA(xA(x) ) B B xA(xxA(x) ) 14量词辖域收缩与扩张(、续)q x x( (A(x)A(x)B B) ) xA(x)xA(x)B B 证明证明: : x(A(x)x(A(x)B B) ) x(x( A(x)A(x)B B) ) x x A(x)A(x)B B xA(x)xA(x)B B xA(x)xA(x)B Bq x x(B(BA(xA(x) ) ) B B xA(xxA(x) ) 证明证明: : x(Bx(BA(xA(x) x(x( B BA(xA(x) ) ) B B x xA(xA(x) ) B B x xA(xA(x) ) B B xA(xxA(x) ) 15量词分配等值式量词分配等值式设设A(xA(x) )，B(xB(x) )是任意的含自由出现个体变项是任意的含自由出现个体变项x x的公式，则的公式，则（1 1） x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) )（2 2） x(A(x)B(xx(A(x)B(x) ) xA(xxA(x) ) xB(xxB(x) )（5.55.5）q例如，例如，“联欢会上所有人既唱歌又跳舞联欢会上所有人既唱歌又跳舞”和和“联欢会上所联欢会上所有人唱歌且所有人跳舞有人唱歌且所有人跳舞” ，这两个语句意义相同。故有，这两个语句意义相同。故有(1)(1)式。式。q由由(1)(1)式推导式推导(2)(2)式式 x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) ) x(x(A(x)A(x)B(xB(x) ) x xA(x)A(x) x xB(xB(x) ) x(A(x)B(xx(A(x)B(x) ) ( xA(x)xA(x) xB(xxB(x) x(A(x)B(xx(A(x)B(x) ) xA(xxA(x) ) xB(xxB(x) ) 16q量词分配等值式量词分配等值式 x(A(x) B(x) xA(x)xB(x) x(A(x) B(x) xA(x)xB(x)q注意注意: 对对 无分配律无分配律, 对对 无分配律无分配律 17量词分配(反例)q x(A(x)x(A(x)B(xB(x) ) xA(x)xA(x) xB(xxB(x) )q x(A(x)x(A(x)B(xB(x) ) xA(x)xA(x) xB(xxB(x) ) 个体域为全体自然数个体域为全体自然数; ; A(xA(x): x): x是偶数是偶数 B(xB(x): x): x是奇数是奇数; ; 左左1, 1, 右右0 0 q x(A(x)x(A(x)B(xB(x) ) xA(x)xA(x) xB(xxB(x) )q x(A(x)x(A(x)B(xB(x) ) xA(x)xA(x) xB(xxB(x) ) 个体域为全体自然数个体域为全体自然数; ; A(xA(x): x): x是偶数是偶数 B(xB(x): x): x是奇数是奇数; ; 左左0, 0, 右右1 1 18量词的次序q x x yA(xyA(x, y) , y) y y x x A(xA(x, y), y)q x x yA(xyA(x, y) , y) y y x x A(xA(x, y), y)q y y xA(xxA(x, y) , y) x x y y A(xA(x, y), y)q x x yA(xyA(x, y) , y) y y x x A(xA(x, y), y)q x x yA(xyA(x, y) , y) y y x x A(xA(x, y), y)相邻的同名量词的次序无关紧要相邻的同名量词的次序无关紧要, , 不同名量词的次不同名量词的次序是不可随意变更的序是不可随意变更的 19一阶逻辑等值演算的三条原则一阶逻辑等值演算的三条原则q置换规则置换规则：设：设(A)(A)是含公式是含公式A A的公式，的公式，(B)(B)是用公式是用公式B B取代取代(A)(A)中所有的中所有的A A之后的公式，若之后的公式，若A AB B，则，则(A)(A)(B)(B)。 q换名规则换名规则：设设A A为一公式，将为一公式，将A A中某量词辖域中某约束变项的中某量词辖域中某约束变项的所有出现及相应的指导变元改成该量词辖域中未曾出现过的所有出现及相应的指导变元改成该量词辖域中未曾出现过的某个体变项符号，公式的其余部分不变，设所得公式为某个体变项符号，公式的其余部分不变，设所得公式为AA，则则AAA A。q代替规则代替规则：设设A A为一公式，将为一公式，将A A中某个自由出现的个体变项的中某个自由出现的个体变项的所有出现用所有出现用A A中未曾出现过的个体变项符号代替，中未曾出现过的个体变项符号代替，A A中其余部中其余部分不变，设所得公式为分不变，设所得公式为AA，则，则AAA A。说明说明q一阶逻辑中的置换规则与命题逻辑中的置换一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同，只是在这里规则形式上完全相同，只是在这里A A，B B是一是一阶逻辑公式。阶逻辑公式。 20例例5.15.1例例5.15.1 将下面公式化成与之等值的公式，使其将下面公式化成与之等值的公式，使其没有既是约束没有既是约束出现又是自由出现的个体变项出现又是自由出现的个体变项。(1)(1) xF(x,y,z)xF(x,y,z) yG(x,y,z)yG(x,y,z)(2)(2) x(F(x,y)x(F(x,y) yG(x,y,zyG(x,y,z)(1)(1) x xF(F(x x,y,z) ,y,z) yG(x,y,zyG(x,y,z) ) tF(t,y,z)tF(t,y,z) y yG(x,G(x,y y,z,z) )( (换名规则换名规则) ) tF(t,y,z)tF(t,y,z) wG(x,w,zwG(x,w,z) )( (换名规则换名规则) )或或 xF(x,xF(x,y y,z),z) yG(x,y,zyG(x,y,z) ) xF(x,t,z)xF(x,t,z) y yG(G(x x, ,y y,z,z) )( (代替规则代替规则) ) x xF(x,t,z)F(x,t,z) y yG(w,y,zG(w,y,z) )( (代替规则代替规则) )解答解答 21例例例例5.15.15.15.1的解答的解答的解答的解答(2)(2) x(F(x,x(F(x,y y) ) yG(x,y,z)yG(x,y,z) x(F(x,t)x(F(x,t) yG(x,y,zyG(x,y,z)( (代替规则代替规则) )或或 x(F(x,y)x(F(x,y) y yG(x,y,zG(x,y,z) x(F(x,y)x(F(x,y) tG(x,t,ztG(x,t,z)( (换名规则换名规则) )解答解答 22例例5.25.2例例5.25.2 证明证明（1 1） x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) ) （2 2） x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) )其中其中A(xA(x) )，B(xB(x) )为含为含x x自由出现的公式。自由出现的公式。只要证明在某个解释下两边的式子不等值。只要证明在某个解释下两边的式子不等值。取解释取解释I I：个体域为自然数集合：个体域为自然数集合N N；(1)(1)取取F(xF(x) )：x x是奇数，代替是奇数，代替A(xA(x) )；取取G(xG(x) )：x x是偶数，代替是偶数，代替B(xB(x) )。则则 x(F(x)G(xx(F(x)G(x)为真命题，为真命题，而而 xF(xxF(x) xG(xxG(x) )为假命题。为假命题。两边不等值。两边不等值。证明证明 23例例例例5.25.25.25.2(2)(2) x(A(x)B(x) x(A(x)B(x) xA(x)xA(x) xB(xxB(x) ) x(F(x)G(xx(F(x)G(x)：有些：有些x x既是奇数又是偶数为假命题；既是奇数又是偶数为假命题；而而 xF(x)xF(x) xG(xxG(x) )：有些：有些x x是奇数并且有些是奇数并且有些x x是偶数为真是偶数为真命题。命题。 两边不等值。两边不等值。证明证明说明说明q全称量词全称量词“ ”对对“”无分配律。无分配律。q存在量词存在量词“ ”对对“”无分配律。无分配律。q当当B(xB(x) )换成没有换成没有x x出现的出现的B B时，则有时，则有 x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B x(A(x)Bx(A(x)B) ) xA(x)BxA(x)B 24例例5.35.3消消去量词去量词例例5.3 5.3 设个体域为设个体域为D D a,b,ca,b,c ，将下面各公式的量词消去：，将下面各公式的量词消去： (1) (1) x(F(x)G(xx(F(x)G(x)(2) (2) x(F(xx(F(x) ) yG(yyG(y)(3) (3) x x yF(x,yyF(x,y) )说明说明q如果不用公式如果不用公式(5.3)(5.3)将量词的辖域缩小，演算过程较将量词的辖域缩小，演算过程较长。注意，此时长。注意，此时 yG(yyG(y) )是与是与x x无关的公式无关的公式B B。解答解答(1)(1) x(F(x)G(x)x(F(x)G(x) ( (F(a)G(aF(a)G(a) () (F(b)G(bF(b)G(b) () (F(c)G(cF(c)G(c)(2)(2) x(F(x) x(F(x) yG(yyG(y) ) xF(x)xF(x) yG(yyG(y) ) ( (公式公式5.3) 5.3) ( (F(a)F(b)F(c)(G(a)G(b)G(cF(a)F(b)F(c)(G(a)G(b)G(c) ) 25例例5.35.3消消去量词去量词(3) (3) x x yF(x,yyF(x,y) ) x(F(x,a)F(x,b)F(x,cx(F(x,a)F(x,b)F(x,c) ) ( (F(a,a)F(a,b)F(a,cF(a,a)F(a,b)F(a,c)(F(b,a)F(b,b)F(b,cF(b,a)F(b,b)F(b,c)(F(c,a)F(c,b)F(c,cF(c,a)F(c,b)F(c,c) ) 在演算中先消去存在量词也可以，得到结果是等值的。在演算中先消去存在量词也可以，得到结果是等值的。 x x yF(x,yyF(x,y) ) yF(a,yyF(a,y) ) yF(b,yyF(b,y) ) yF(c,yyF(c,y) ) ( (F(a,a)F(a,b)F(a,cF(a,a)F(a,b)F(a,c)(F(b,a)F(b,b)F(b,cF(b,a)F(b,b)F(b,c)(F(c,a)F(c,b)F(c,cF(c,a)F(c,b)F(c,c) ) 26例例5.45.4例例5.45.4 给定解释给定解释I I如下：如下：（a a）个体域）个体域 D D2,32,3（b b）D D中特定元素中特定元素（c c）D D上的特定函数上的特定函数(x)(x)为：为：（d d）D D的特定谓词的特定谓词在解释在解释I I下求下列各式的值：下求下列各式的值：（1 1） x(F(x)G(x,ax(F(x)G(x,a) ) （2 2） x(F(f(x)G(x,f(xx(F(f(x)G(x,f(x)（3 3） x x yL(x,yyL(x,y) ) （4 4） y y xL(x,yxL(x,y) ) 27例例5.45.4的解答的解答（1 1） x(F(x)G(x,ax(F(x)G(x,a) (F(2)G(2,2) (F(3)G(3,2) (F(2)G(2,2) (F(3)G(3,2) (01) (11)(01) (11) 0 0 （2 2） x(F(f(x)G(x,f(xx(F(f(x)G(x,f(x) (F(f(2)G(2,f(2) (F(f(3)G(3,f(3) (F(f(2)G(2,f(2) (F(f(3)G(3,f(3) (F(3)G(2,3) (F(2)G(3,2) (F(3)G(2,3) (F(2)G(3,2) (11) (01)(11) (01) 1 1 28例例5.45.4的解答的解答（3 3） x x yL(x,yyL(x,y) ) (L(2,2)L(2,3) (L(3,2)L(3,3) (L(2,2)L(2,3) (L(3,2)L(3,3) (10) (01) (10) (01) 1 1（4 4） y y xL(x,yxL(x,y) ) y(L(2,y)L(3,y) y(L(2,y)L(3,y) (L(2,2)L(3,2) (L(2,3)L(3,3) (L(2,2)L(3,2) (L(2,3)L(3,3) (10) (01)(10) (01) 0 0说明说明q由由(3)(3)，(4)(4)的结果进一步可以说明量词的次的结果进一步可以说明量词的次序不能随意颠倒。序不能随意颠倒。 29例例5.55.5例例5.55.5 证明下列等值式。证明下列等值式。 （1 1） x(M(x)F(xx(M(x)F(x) ) x(M(x)F(xx(M(x)F(x) ) （2 2） x(F(x)G(xx(F(x)G(x) ) x(F(x)G(xx(F(x)G(x) ) （3 3） x x y(F(x)G(y)H(xy(F(x)G(y)H(x，y)y) x x y(F(x)G(y)H(x,yy(F(x)G(y)H(x,y) ) （4 4） x x y(F(x)G(y)L(xy(F(x)G(y)L(x，y)y) x x y(F(x)G(y)L(x,yy(F(x)G(y)L(x,y) ) 30例例5.55.5的证明的证明（1 1） x(M(x)F(xx(M(x)F(x) ) x(M(x)F(xx(M(x)F(x) x(M(x)F(xx(M(x)F(x) x(M(x)F(xx(M(x)F(x) x(M(x)F(xx(M(x)F(x) x(M(x)F(xx(M(x)F(x) ) （2 2） x(F(x)G(xx(F(x)G(x) ) x(F(x)G(xx(F(x)G(x) x(F(x)G(xx(F(x)G(x) x(F(x)G(xx(F(x)G(x) x(F(x)G(xx(F(x)G(x) x(F(x)G(xx(F(x)G(x) ) 31例例例例5.55.55.55.5的证明的证明的证明的证明（3 3） x x y(F(x)G(y)H(xy(F(x)G(y)H(x，y)y) x x y(F(x)G(y)H(x,yy(F(x)G(y)H(x,y) x x y y( (F(x)G(y)H(xF(x)G(y)H(x，y)y) ) xx( ( y y( (F(x)G(y)H(xF(x)G(y)H(x，y)y) ) ) x x yy( (F(x)G(y)H(x(F(x)G(y)H(x，y)y) ) x x y(F(x)G(y)H(x,yy(F(x)G(y)H(x,y) ) 32例例例例5.55.55.55.5的证明的证明的证明的证明（4 4） x x y(F(x)G(y)L(xy(F(x)G(y)L(x，y)y) x x y(F(x)G(y)L(x,yy(F(x)G(y)L(x,y) x x y(F(x)G(y)L(xy(F(x)G(y)L(x，y)y) x x ( y(F(x)G(y)L(xy(F(x)G(y)L(x，y)y) x x y(F(x)G(y)L(xy(F(x)G(y)L(x，y)y) x x y(F(x)G(y)L(x,yy(F(x)G(y)L(x,y) ) x x y(F(x)G(y)L(x,yy(F(x)G(y)L(x,y) ) 335.2 5.2 一阶逻辑前束范式一阶逻辑前束范式定义定义5.25.2 设设A A为一个一阶逻辑公式，若为一个一阶逻辑公式，若A A具有如下形式具有如下形式Q Q1 1x x1 1Q Q2 2x x2 2 Q Qk kx xk kB B则称则称A A为为前束范式前束范式，其中，其中Q Qi i(1ik)(1ik)为为 或或 ，B B为不含量词为不含量词的公式。的公式。q前束范式的例子：前束范式的例子： x x y(F(x)G(y)H(xy(F(x)G(y)H(x，y) y) x x y y z(F(x)G(y)H(z)L(xz(F(x)G(y)H(z)L(x，y y，z) z) q不是前束范式的例子：不是前束范式的例子： x x( (F(x)F(x) y y(G(y)H(x(G(y)H(x，y)y) ) x x( (F(x)F(x) y y(G(y)H(x(G(y)H(x，y)y) ) 34前束范式存在定理前束范式存在定理定理定理5.1 5.1 一阶逻辑中的任何公式都存在与之等值的前束范式。一阶逻辑中的任何公式都存在与之等值的前束范式。说明说明q求前束范式的过程，就是制造量词辖域可以扩大的求前束范式的过程，就是制造量词辖域可以扩大的条件，进行量词辖域扩大。条件，进行量词辖域扩大。q任何公式的前束范式都是存在的，但一般说来，并任何公式的前束范式都是存在的，但一般说来，并不唯一。不唯一。q利用一阶逻辑等值式以及三条变换规则（置换规则、利用一阶逻辑等值式以及三条变换规则（置换规则、换名规则、代替规则）就可以求出与公式等值的前换名规则、代替规则）就可以求出与公式等值的前束范式，或所谓公式的前束范式。束范式，或所谓公式的前束范式。(1)(1)利用量词转化公式，把否定深入到指导变元的后面。利用量词转化公式，把否定深入到指导变元的后面。 xA(xxA(x) ) xA(xxA(x) ) xA(xxA(x) ) xA(xxA(x) )(2)(2)利用利用 x(A(x)B)x(A(x)B) xA(x)BxA(x)B和和 x(A(x)B)x(A(x)B) xA(x)BxA(x)B把把量词移到全式的最前面，这样便得到前束范式。量词移到全式的最前面，这样便得到前束范式。 35例例5.6 5.6 求公式的前束范式求公式的前束范式（1 1） xF(x)xF(x) x xG(G(x x) ) xF(x)xF(x) yG(yyG(y) ) ( (换名规则换名规则) ) xF(x)xF(x) yG(yyG(y) ) (5.2)(5.2)第二式第二式) ) x(F(x)x(F(x) yG(yyG(y) ) (5.3)(5.3)第二式第二式) ) x x y(F(x)G(yy(F(x)G(y) ) (5.3)(5.3)第二式第二式) ) （ y y x(F(x)G(yx(F(x)G(y) ) ）或者或者 xF(x)xF(x) xG(xxG(x) ) xF(x)xF(x) xG(xxG(x) ) (5.2)(5.2)第二式第二式) ) x(F(x)G(xx(F(x)G(x) ) (5.5)(5.5)第一式第一式) ) 36例例例例5.6 5.6 5.6 5.6 求公式的前束范式求公式的前束范式求公式的前束范式求公式的前束范式（2 2） xF(x)xF(x) xG(xxG(x) ) xF(x)xF(x) xG(xG(x x) ) (5.2)(5.2)第二式第二式) ) xF(x)xF(x) yG(yyG(y) ) ( (换名规则换名规则) ) x(F(x)x(F(x) yG(yyG(y) ) (5.3)(5.3)第一式第一式) ) x x y(F(x)G(yy(F(x)G(y) ) (5.3)(5.3)第一式第一式) ) 说明说明q公式的前束范式是不唯一的。公式的前束范式是不唯一的。 37例例5.7 5.7 求前束范式求前束范式(1)(1) xF(xF(x x) ) xG(xxG(x) ) yF(yyF(y) ) xG(xxG(x) ) y y x(F(y)G(xx(F(y)G(x)(2) (2) xF(xF(x x) ) xG(xxG(x) ) y yF(yF(y) ) xG(xxG(x) ) y y x(x(F(y)G(xF(y)G(x)(3) (3) xF(xF(x x) ) xG(xxG(x) ) y yF(yF(y) ) xG(xxG(x) ) y y x(x(F(y)G(xF(y)G(x)(4) (4) xF(xxF(x) ) y yG(yG(y) ) x x y(y(F(x)G(xF(x)G(x) 38例例5.8 5.8 求公式的前束范式求公式的前束范式(1)(1) xF(xF(x,x,y)y) yG(x,yG(x,y y) ) tF(t,y)tF(t,y) wG(x,wwG(x,w) () (换名规则换名规则) ) t t w(F(t,y)G(x,ww(F(t,y)G(x,w) (5.3),(5.4) ) (5.3),(5.4) 或者或者 xF(x,xF(x,y y) yG(yG(x x,y,y) ) xF(x,t)xF(x,t) yG(w,yyG(w,y) () (代替规则代替规则) ) x x y(F(x,t)G(w,yy(F(x,t)G(w,y) (5.3),(5.4) (5.3),(5.4)说明说明q解本题时一定注意，哪些个体变项是约束出现，解本题时一定注意，哪些个体变项是约束出现，哪些是自由出现，特别要注意那些既是约束出哪些是自由出现，特别要注意那些既是约束出现又是自由出现的个体变项。不能混淆现又是自由出现的个体变项。不能混淆。 39例例例例5.8 5.8 5.8 5.8 求公式的前束范式求公式的前束范式求公式的前束范式求公式的前束范式(2)(2)( x x1 1F(F(x x1 1,x,x2 2) ) x x2 2G(G(x x2 2) ) x x1 1H(xH(x1 1,x,x2 2,x,x3 3) ) ( ( x x4 4F(F(x x4 4,x,x2 2) ) x x5 5G(G(x x5 5) ) x x1 1H(xH(x1 1,x,x2 2,x,x3 3) ) x x4 4 x x5 5(F(F(x x4 4,x,x2 2) G() G(x x5 5) ) x x1 1H(xH(x1 1,x,x2 2,x,x3 3) ) x x4 4 x x5 5 x x1 1( ( (F(F(x x4 4,x,x2 2) G() G(x x5 5) ) ) H(x H(x1 1,x,x2 2,x,x3 3) ) ) 405.3 5.3 一阶逻辑的推理理论一阶逻辑的推理理论q在一阶逻辑中，从前提在一阶逻辑中，从前提A A1 1,A,A2 2, ,A Ak k出发推结论出发推结论B B的推理形式结的推理形式结构，依然采用如下的蕴涵式形式构，依然采用如下的蕴涵式形式A A1 1 ,A,A2 2 , , , ,A Ak k B B （5.65.6）若式（若式（5.65.6）为永真式，则称）为永真式，则称推理正确推理正确，否则称推理不正确。，否则称推理不正确。q于是，在一阶逻辑中判断推理是否正确也归结为判断（于是，在一阶逻辑中判断推理是否正确也归结为判断（5.65.6）式是否为永真式了。式是否为永真式了。q在一阶逻辑中称永真式的蕴涵式为在一阶逻辑中称永真式的蕴涵式为推理定律推理定律，若一个推理的，若一个推理的形式结构正是某条推理定律，则这个推理显然是正确的。形式结构正是某条推理定律，则这个推理显然是正确的。q在一阶逻辑的推理中，某些前提与结论可能是受量词限制，在一阶逻辑的推理中，某些前提与结论可能是受量词限制，为了使用命题逻辑中的等值式和推理定律，为了使用命题逻辑中的等值式和推理定律，必须在推理过程必须在推理过程中有消去和添加量词的规则中有消去和添加量词的规则，以便使谓词演算公式的推理过，以便使谓词演算公式的推理过程可类似于命题演算中推理理论那样进行。程可类似于命题演算中推理理论那样进行。 41推理定律的来源推理定律的来源q命题逻辑推理定律的代换实例命题逻辑推理定律的代换实例q由基本等值式生成的推理定律由基本等值式生成的推理定律q量词分配等值式量词分配等值式q推理规则推理规则量量词消去和引入规则词消去和引入规则 42命题逻辑推理定律的代换实例命题逻辑推理定律的代换实例q xF(x)xF(x) yG(yyG(y) ) xF(xxF(x) )（化简律的代换实例）（化简律的代换实例）q xF(xxF(x) ) xF(xxF(x) ) yG(yyG(y) ) （附加律的代换实例）（附加律的代换实例）q 43由基本等值式生成的推理定律由基本等值式生成的推理定律q xF(xxF(x) ) xF(xxF(x) ) q xF(xxF(x) ) xF(xxF(x) )q xF(xxF(x) ) xF(xxF(x) )q xF(xxF(x) ) xF(xxF(x) ) q 44其他推理定律其他推理定律q xA(x)xA(x) xB(xxB(x) ) x(A(x)B(xx(A(x)B(x) ) q x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) ) q x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) ) q x(A(x)B(xx(A(x)B(x) ) xA(xxA(x) ) xB(xxB(x) ) q q对对 x(A(x)B(xx(A(x)B(x) ) xA(x)xA(x) xB(xxB(x) )的讨论的讨论若若 x(A(x)B(xx(A(x)B(x)为真，则有一个客体为真，则有一个客体c c，使得，使得A(c)B(cA(c)B(c) )为真，即为真，即A(cA(c) )和和B(cB(c) )都为真，所以都为真，所以 xA(x)xA(x) xB(xxB(x) )也为真。也为真。 45推理规则推理规则q为了构造推理系统，还要给出为了构造推理系统，还要给出4 4条重要的推理规则条重要的推理规则, ,即消去量词和引入量词的规则：即消去量词和引入量词的规则：1 1全称量词消去规则全称量词消去规则( (简记为简记为UIUI规则或规则或UI)UI)Universal instantiation Universal instantiation 2 2全称量词引入规则全称量词引入规则( (简记为简记为UGUG规则或规则或UG)UG)Universal Generalize Universal Generalize 3 3存在量词引入规则存在量词引入规则( (简称简称EGEG规则或规则或EG)EG)Existential Generalize Existential Generalize 4 4存在量词消去规则存在量词消去规则( (简记为简记为EIEI规则或规则或EI)EI)Existential instantiation Existential instantiation 46全称量词消去规则全称量词消去规则( (简记为简记为UIUI规则或规则或UI)UI)含含义义：如如果果个个体体域域的的所所有有元元素素都都具具有有性性质质A A，则则个个体体域域中中的的任任一元素具有性质一元素具有性质A A。 两式成立的条件两式成立的条件： (1)(1)在在第第一一式式中中，取取代代x x的的y y应应为为任任意意的的不不在在A(xA(x) )中中约约束束出出现现的的个体变项。个体变项。 (2)(2)在第二式中，在第二式中，c c为任意个体变项。为任意个体变项。 (3)(3)用用y y或或c c去去取取代代A(xA(x) )中中自自由由出出现现的的x x时时，一一定定要要在在x x自自由由出出现现的一切地方进行取代。的一切地方进行取代。 47全称量词消去规则全称量词消去规则( (简记为简记为UIUI规则或规则或UI)UI)举例举例当当A(xA(x) )为原子公式时，比如为原子公式时，比如A(xA(x)=)=F(xF(x) )，则当，则当 xA(xxA(x) )为为真时，对于个体域中任意的个体变项真时，对于个体域中任意的个体变项y y，不会出现，不会出现F(yF(y) )为为假的情况。假的情况。当当A(xA(x) )不是原子公式时，如不是原子公式时，如y y已在已在A(xA(x) )中约束出现了，就中约束出现了，就不能用不能用y y取代取代x x，否则会出现，否则会出现 xA(xxA(x) )为真而为真而A(yA(y) )为假的情为假的情况。况。考虑个体域为实数集合，公式考虑个体域为实数集合，公式A(xA(x)=)= yF(x,yyF(x,y) )为为xyxy。当对公式当对公式 xA(xxA(x)=)= x x yF(x,yyF(x,y) )使用使用UIUI规则时，用规则时，用y y取代取代x x，就会得到，就会得到A(yA(y)=)= yF(y,yyF(y,y) )，即，即 y(yy(yy)y)，这显然是假，这显然是假命题。原因是违背了条件命题。原因是违背了条件(1)(1)。若用若用z z取代取代x x，得，得A(zA(z)=)= yF(z,yyF(z,y)=)= y(zy(zy)y)就不会产生就不会产生这种错误。这种错误。 48全称量词引入规则全称量词引入规则( (简记为简记为UGUG规则或规则或UG)UG)该式成立的条件是：该式成立的条件是：(1)(1)无论无论A(yA(y) )中自由出现的个体变项中自由出现的个体变项y y取何值，取何值，A(yA(y) )应该均为真。应该均为真。 (2)(2)取代自由出现的取代自由出现的y y的的x x也不能在也不能在A(yA(y) )中约束出现。中约束出现。 举例举例取个体域为实数集，取个体域为实数集，F(x,yF(x,y) )为为xyxy，A(yA(y)=)= xF(x,yxF(x,y) )。显然显然A(yA(y) )满足条件满足条件(1)(1)。对对A(yA(y) )应用应用UGUG规则时，若取已约束出现的规则时，若取已约束出现的x x取代取代y y，会得，会得到到 xA(xxA(x)=)= x x x(xx(xx)x)，这是假命题。，这是假命题。产生这种错误的原因是违背了条件产生这种错误的原因是违背了条件(2)(2)。若取若取z z取代取代y y，得，得 zA(zzA(z)=)= z z x(xx(xz)z)为真命题。为真命题。 49存在量词引入规则存在量词引入规则( (简称简称EGEG规则或规则或EG) EG) 该式成立的条件是：该式成立的条件是： (1)c(1)c是特定的个体常项。是特定的个体常项。(2)(2)取代取代c c的的x x不能在不能在A(cA(c) )中出现过。中出现过。 举例举例取个体域为实数集，取个体域为实数集，F(x,yF(x,y) )为为xyxy，取，取A(5)=A(5)= xF(x,5)xF(x,5)。显然显然A(5)A(5)是真命题。是真命题。在应用在应用EGEG规则时，若用规则时，若用A(5)A(5)中已出现的中已出现的x x取代取代5 5，得，得 x x xF(x,xxF(x,x)=)= x(xx(xx)x)，这是假命题。，这是假命题。产生这种错误的原因是违背了条件产生这种错误的原因是违背了条件(2)(2)。若用若用A(5)A(5)中未出现过的个体变项中未出现过的个体变项y y取代取代5 5，得，得 yA(yyA(y)=)= y y xF(xxF(xy)y)，这为真命题。，这为真命题。 50存在量词消去规则存在量词消去规则( (简记为简记为EIEI规则或规则或EI) EI) 该式成立的条件是：该式成立的条件是：(1)c(1)c是使是使A A为真的特定的个体常项。为真的特定的个体常项。 (2)c(2)c不在不在A(xA(x) )中出现。中出现。 (3)(3)若若A(xA(x) )中中除除自自由由出出现现的的x x外外，还还有有其其它它自自由出现的个体变项，此规则不能使用。由出现的个体变项，此规则不能使用。 举例举例取个体域为自然数集合，取个体域为自然数集合，F(xF(x) )为为x x是奇数，是奇数，G(xG(x) )为为x x是偶数是偶数。 xF(xxF(x) )与与 xG(xxG(x) )都是真命题，则对于某些都是真命题，则对于某些c c和和d d，可以断定，可以断定P(c)Q(dP(c)Q(d) )必定为真，但不能断定必定为真，但不能断定P(c)Q(cP(c)Q(c) )是真。是真。 对对 xF(xxF(x) )使用使用EIEI规则时，取代规则时，取代x x的的c c一定是特定的个体常项一定是特定的个体常项1,3,51,3,5等奇数。等奇数。对对 xG(xxG(x) )使用使用EIEI规则时，取代规则时，取代x x的的c c一定是特定的个体常项一定是特定的个体常项2,4,62,4,6等偶数。等偶数。 51定义定义5.3 5.3 自然推理系统定义自然推理系统定义1.1.字母表。同一阶语言的字母表。字母表。同一阶语言的字母表。2.2.合式公式。同合式公式的定义。合式公式。同合式公式的定义。3.3.推理规则：推理规则：(1)(1)前提引入规则。前提引入规则。(2)(2)结论引入规则。结论引入规则。(3)(3)置换规则。置换规则。 52(4)假言推理规则假言推理规则ABAB(5)附加规则附加规则:AA B(6)化简规则化简规则:A BA(7)拒取式规则拒取式规则:AB BA(8)假言三段论规则假言三段论规则:ABBCAC 53(9)析取三段论规则析取三段论规则:A B BA(10)构造性二难推理规则构造性二难推理规则:ABCDA CB D(11)合取引入规则合取引入规则:ABA B 54(12)UI(12)UI规则。规则。(13)UG(13)UG规则。规则。(14)EG(14)EG规则。规则。(15)EI(15)EI规则。规则。 55例题例题例题例题 在自然推理系统中，构造下面推理的证明在自然推理系统中，构造下面推理的证明所有的人都是要死的，苏格拉底是人，所以苏格拉底是要所有的人都是要死的，苏格拉底是人，所以苏格拉底是要死的。死的。 解解：先将原子命题符号化。：先将原子命题符号化。 设设 F(x):xF(x):x是一个人，是一个人，G(x):xG(x):x是要死的，是要死的，a a：苏格拉底。：苏格拉底。 前提：前提： x(F(x)G(xx(F(x)G(x), ), F(aF(a) ) 结论：结论：G(aG(a) )证明：证明： x(F(x)G(xx(F(x)G(x)前提引入前提引入 F(a)G(aF(a)G(a) ) UIUI规则规则 F(aF(a) ) 前提引入前提引入 G(aG(a) ) 假言推理假言推理 56例例5.95.9例例5.9 5.9 设个体域为实数集合，设个体域为实数集合，F(x,yF(x,y) )为为xyxy。指出在推理系统。指出在推理系统F F中，以中，以 x x yF(xyF(x，y)(y)(真命题真命题) )为前提，推出为前提，推出 xF(x,cxF(x,c)()(假命假命题题) )的下述推理证明中的错误。的下述推理证明中的错误。 x x yF(x,yyF(x,y) ) 前提引入前提引入 yF(z,yyF(z,y) ) UIUI规则规则 F(z,cF(z,c) ) EIEI规则规则 xF(x,cxF(x,c) ) UGUG规则规则 解解 由由于于c c为为特特定定的的个个体体常常项项，所所以以 xF(x,cxF(x,c)()(即即为为 x(xx(xc)c)为为假假命命题题。如如果果按按F F中中推推理理规规则则进进行行推推理理，不不会会从从真真命命题题推推出出假命题。假命题。在在以以上上推推理理证证明明中中，第第三三步步错错了了，由由于于F(z,yF(z,y) )中中除除有有自自由由出出现现的的y y，还还有有自自由由出出现现的的z z，按按EIEI规规则则应应该该满满足足的的条条件件(3)(3)，此此处处不不能能用用EIEI规规则则。用用了了EIEI规规则则，导导致致了了从从真真命命题题推推出出假假命命题的错误。题的错误。 57例例5.105.10例例5.105.10 在自然推理系统中，构造下面推理的证明在自然推理系统中，构造下面推理的证明任何自然数都是整数；存在着自然数。所以存在着整数。任何自然数都是整数；存在着自然数。所以存在着整数。个体域为实数集合个体域为实数集合R R。解解：先将原子命题符号化。：先将原子命题符号化。设设 F(x):xF(x):x为自然数，为自然数，G(x):xG(x):x为整数。为整数。 前提：前提： x(F(x)G(xx(F(x)G(x), ), xF(xxF(x) ) 结论：结论： xG(xxG(x) )证明：证明： xF(xxF(x) ) 前提引入前提引入 F(cF(c) ) EIEI规则规则 x(F(x)G(xx(F(x)G(x) ) 前提引入前提引入 F(c)G(cF(c)G(c) ) UIUI规则规则 G(cG(c) ) 假言推理假言推理 xG(xxG(x) ) EGEG规则规则 58例例5.105.10说明说明q以以上上证证明明的的每每一一步步都都是是严严格格按按推推理理规规则则及及应应满满足足的的条条件件进进行的。因此，前提的合取为真时，结论必为真。行的。因此，前提的合取为真时，结论必为真。q但但如如果果改改变变命命题题序序列列的的顺顺序序会会产产生生由由真真前前提提推推出出假假结结论论的的错误。如果证明如下进行：错误。如果证明如下进行： x(F(x)G(xx(F(x)G(x) ) 前提引入前提引入 F(c)G(cF(c)G(c) ) UIUI规则规则 xF(xxF(x) ) 前提引入前提引入 F(cF(c) ) EIEI规则规则q在在中取中取c=,c=,则则F()G(F()G() )为真（前件假）为真（前件假）, ,于是于是中中F(F() )为假，这样从前件真推出了假的中间结果。为假，这样从前件真推出了假的中间结果。 59例例5.115.11例例5.115.11 在自然推理系统在自然推理系统F F中中, ,构造下面推理的证明。构造下面推理的证明。前提：前提： x(F(x)G(xx(F(x)G(x), ), x(F(x)H(xx(F(x)H(x)结论：结论： x(x(G(xG(x）H(xH(x)提示提示 在证明序列中先引进带存在量词的前提。在证明序列中先引进带存在量词的前提。 60例例5.115.11证明证明 x(F(x)H(xx(F(x)H(x) ) 前提引入前提引入 F(c)H(cF(c)H(c) ) EIEI规则规则 x(F(x)G(xx(F(x)G(x) ) 前提引入前提引入 F(c)G(cF(c)G(c) ) UIUI规则规则 F(cF(c) ) 化简化简 G(cG(c) ) 假言推理假言推理 H(cH(c) ) 化简化简 G(c)H(cG(c)H(c) ) 合取合取 ( (G(xG(x）H(xH(x) )） EGEG规则规则 61例例5.125.12例例5.125.12 在自然推理系统在自然推理系统F F中，构造下面推理的证明：中，构造下面推理的证明：不存在能表示成分数的无理数，有理数都能表示成分数。不存在能表示成分数的无理数，有理数都能表示成分数。因此，有理数都不是无理数。因此，有理数都不是无理数。个体域为实数集合。个体域为实数集合。设设 F(x):xF(x):x为无理数，为无理数， G(x):xG(x):x为有理数，为有理数， H(x):xH(x):x能表示成分数。能表示成分数。前提：前提： x(F(x)H(xx(F(x)H(x)， x(G(x)H(xx(G(x)H(x)结论：结论： x(G(xx(G(x) ) F(xF(x)解答解答 62例例5.125.12证明证明 x(F(x)H(xx(F(x)H(x) ) 前提引入前提引入 x(F(xx(F(x) ) H(xH(x) ) 置换置换 x(H(xx(H(x) ) F(xF(x) ) ) ) 置换置换 H(yH(y) ) F(yF(y) ) UIUI规则规则 x(G(x)H(xx(G(x)H(x) ) 前提引入前提引入 G(y)H(yG(y)H(y) ) UIUI规则规则 G(yG(y) ) F(yF(y) ) 假言三段论假言三段论 x(G(xx(G(x) ) F(xF(x) ) UGUG规则规则q注意注意 x(F(x)H(xx(F(x)H(x)不是前束范式，因而不能对不是前束范式，因而不能对它使用它使用EIEI规则。规则。q因为结论中的量词是全称量词因为结论中的量词是全称量词 ，因而在使用，因而在使用UIUI规则规则时用第一式，而不能用第二式。时用第一式，而不能用第二式。说说明明 63q例例乌鸦都不是白色的乌鸦都不是白色的.北京鸭是白色的北京鸭是白色的.因此因此,北京鸭不是乌鸦北京鸭不是乌鸦.令令F(x):x是乌鸦是乌鸦,G(x):x是北京鸭是北京鸭,H(x):x是白色的是白色的前提前提: x(F(x)H(x), x(G(x)H(x)结论结论: x(G(x)F(x)q证明证明: x(F(x)H(x)前提引入前提引入F(y)H(y)UI x(G(x)H(x)前提引入前提引入G(y)H(y)UI H(y)G(y)置换置换F(y)G(y)假言三段论假言三段论G(y)F(y)置换置换 x(G(x)F(x)UG 64q例例前提前提: x(F(x)G(x), xF(x)结论结论: xG(x)q证明证明: xF(x)前提引入前提引入 x(F(x)G(x)前提引入前提引入F(c)EIF(c)G(c)UIG(c)假言推理假言推理 xG(x)EGq注意注意:一定先消存在量词一定先消存在量词 65q例例前提前提: xF(x)xG(x)结论结论: x(F(x)G(x)q证明证明: xF(x)xG(x)前提引入前提引入 x y(F(x)G(y)置换置换 x(F(x)G(z)UIF(z)G(z)UI x(F(x)G(x)UGq说明说明:不能对不能对 xF(x)xG(x)消量词消量词,因为它不是前束范式因为它不是前束范式.对此题不能用附加前提证明法对此题不能用附加前提证明法 66q例例前提前提: x(F(x)G(x)结论结论: xF(x)xG(x)q证明证明: xF(x)附加前提引入附加前提引入F(y)UI x(F(x)G(x)前提引入前提引入F(y)G(y)UIG(y)假言推理假言推理 xG(x)UGq本题可以使用附加前提证明法本题可以使用附加前提证明法,为什么上例不能用为什么上例不能用? 67本章主要内容本章主要内容q等值式与基本的等值式等值式与基本的等值式在有限个体域中消去量词等值式在有限个体域中消去量词等值式量词否定等值式量词否定等值式量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式量词分配等值式量词分配等值式q基本规则：置换规则、换名规则、代替规则基本规则：置换规则、换名规则、代替规则q前束范式前束范式q推理理论：推理的形式结构、推理正确、构造证明推理理论：推理的形式结构、推理正确、构造证明q新的推理规则：新的推理规则：UIUI、UGUG、EIEI、EGEG 68学习要求学习要求q深刻理解重要的等值式，并能熟练地使用它们。深刻理解重要的等值式，并能熟练地使用它们。 q熟练地使用置换规则、换名规则和代替规则。熟练地使用置换规则、换名规则和代替规则。 q准确地求出给定公式的前束范式（形式可以不唯一）。准确地求出给定公式的前束范式（形式可以不唯一）。 q正正确确地地使使用用UIUI、UGUG、EIEI、EGEG规规则则，特特别别地地要要注注意意它它们们之之间间的的关系。关系。 一一定定对对前前束束范范式式才才能能使使用用UIUI、UGUG、EIEI、EGEG规规则则，对对不不是是前前束范式的公式要使用它们，一定先求出公式的前束范式。束范式的公式要使用它们，一定先求出公式的前束范式。记住记住UIUI、UGUG、EIEI、EGEG规则的各自使用条件。规则的各自使用条件。在在同同一一推推理理的的证证明明中中，如如果果既既要要使使用用UIUI规规则则，又又要要使使用用EIEI规规则则，一一定定要要先先使使用用EIEI规规则则，后后使使用用UIUI规规则则，而而且且UIUI规规则则使用的个体常项一定是使用的个体常项一定是EIEI规则中使用过的。规则中使用过的。q对于给定的推理，正确地构造出它的证明。对于给定的推理，正确地构造出它的证明。 69q练习题练习题q1证明下列各等值式证明下列各等值式(1)x(F(x)G(x) x(F(x)G(x)(2)x(F(x)G(x) x(F(x)G(x)(3) x(F(x)y(G(y)L(x,y) x y(F(x) G(y)L(x,y)q证证:由由(1)与与(2)可知可知,“并不是所有的人都喜欢吃馒头并不是所有的人都喜欢吃馒头.”,“没没有不犯错误的人有不犯错误的人”,都可以有两种等值的符号化形式都可以有两种等值的符号化形式.(3) x(F(x)y(G(y)L(x,y) x y(F(x)(G(y)L(x,y)(量词辖域扩张量词辖域扩张) x y(F(x) G(y)L(x,y)q由由(3)可知可知,“火车都比汽车快火车都比汽车快”等命题可以有不同的符号化等命题可以有不同的符号化形式形式. 70q2设个体域设个体域D=a,b,c,消去下列公式的量词消去下列公式的量词(1) xF(x)yG(y)(2) x y(F(x) G(y)(3) x(F(x)yG(y)q解解:(1) xF(x)yG(y)(F(a) F(b) F(c) (G(a) G(b) G(c)(2)先将量词辖域缩小先将量词辖域缩小,再消量词方便再消量词方便 x y(F(x) G(y) xF(x)yG(y)(量词辖域收缩扩张等值式量词辖域收缩扩张等值式)(F(a) F(b) F(c) (G(a) G(b) G(c)原来原来(1)与与(2)等值等值 71q(3)先将量词辖域缩小先将量词辖域缩小 x(F(x)yG(y) xF(x)yG(y)(量词辖域收缩扩张等值式量词辖域收缩扩张等值式)(F(a) F(b) F(c)(G(a) G(b) G(c)说明说明:在做此类问题时在做此类问题时,若能将量词辖域缩小若能将量词辖域缩小,就缩小后就缩小后再消量词再消量词,否则太麻烦否则太麻烦. 72q3求下列各公式的前束范式求下列各公式的前束范式(1) xF(x)yG(x,y)(2) xF(x,y)xG(x,y)(3)( x1F(x1,x2)x2G(x2)x2H(x1,x2) 73q解解:求前束范式时求前束范式时,要用换名规则、代替规则、量词否定要用换名规则、代替规则、量词否定等值式、量词辖域收缩与扩张等值式等值式、量词辖域收缩与扩张等值式.(1) xF(x)yG(x,y) xF(x)y G(x,y)(量词否定等值式量词否定等值式) xF(x)y G(z,y)(代替规则代替规则) x y(F(x)G(z,y)(辖域收缩扩张等值式辖域收缩扩张等值式) 74(2) xF(x,y)xG(x,y) xF(x,y)zG(z,y)(换名规则换名规则) x z(F(x,y)G(z,y)(3)( x1F(x1,x2)x2G(x2)x2H(x1,x2)( x1F(x1,x2)x3G(x3)x4H(x5,x4) x1 x3(F(x1,x2)G(x3)x4H(x5,x4) x1 x3 x4(F(x1,x2)G(x3)H(x5,x4)请填上每步用的等值式或规则请填上每步用的等值式或规则. 75q4在自然推理系统在自然推理系统F中构造下面推理的证明中构造下面推理的证明.每个喜欢步行的人都不喜欢骑自行车每个喜欢步行的人都不喜欢骑自行车.每个人或者是喜每个人或者是喜欢骑自行车或者喜欢乘汽车欢骑自行车或者喜欢乘汽车.有的人不喜欢乘汽车有的人不喜欢乘汽车.所所以以,有人不喜欢步行有人不喜欢步行(个体域为人的集合个体域为人的集合)令令F(x):x喜欢步行喜欢步行,G(x):x喜欢骑自行车喜欢骑自行车H(x):x喜欢乘汽车喜欢乘汽车因为个体域是人的集合因为个体域是人的集合,故不引入特性谓词故不引入特性谓词前提前提: x(F(x)G(x), x(G(x) H(x), x H(x)结论结论: x F(x) 76q证明证明: x H(x)前提引入前提引入 H(c)EI x(G(x) H(x)前提引入前提引入G(c) H(c)UIG(c)析取三段论析取三段论 x(F(x)G(x)前提引入前提引入F(c)G(c)UI F(c)拒取式拒取式 x F(x)EGq注意注意:先消去存在量词先消去存在量词 77在自然推理系统在自然推理系统F F中构造推理的证明中构造推理的证明前提：前提： xF(xxF(x) ) xG(xxG(x) )结论：结论： x(F(x)G(xx(F(x)G(x)证明证明 xF(xxF(x) ) xG(xxG(x) ) 前提引入前提引入 yF(yyF(y) ) xG(xxG(x) ) 置换（换名规则）置换（换名规则） y y x(F(y)G(xx(F(y)G(x) ) 置换置换 x(F(z)G(xx(F(z)G(x) ) UIUI规则规则 F(z)G(zF(z)G(z) ) UIUI规则规则 x(F(x)G(xx(F(x)G(x) ) UGUG规则规则 78在自然推理系统在自然推理系统在自然推理系统在自然推理系统F F F F中构造推理的证明中构造推理的证明中构造推理的证明中构造推理的证明前提：前提： x(F(xx(F(x) ) G(xG(x)结论：结论： xF(x)xF(x) xG(xxG(x) )证明证明 xF(xxF(x) ) 附加前提引入附加前提引入 F(yF(y) ) UIUI规则规则 x(F(x)G(xx(F(x)G(x) ) 前提引入前提引入 F(y)G(yF(y)G(y) ) UIUI规则规则 G(yG(y) ) 假言推理假言推理 xG(xxG(x) ) UGUG规则规则 79例题选讲例题选讲例题例题 在自然推理系统在自然推理系统F F中，构造下面推理的证明：中，构造下面推理的证明：实数不是有理数就是无理数，无理数都不是分数，所以，实数不是有理数就是无理数，无理数都不是分数，所以，若有分数，则必有有理数（个体域为实数集合）若有分数，则必有有理数（个体域为实数集合）设设 F(x):xF(x):x是有理数，是有理数， G(x):xG(x):x是无理数，是无理数， H(x):xH(x):x是分数。是分数。前提：前提： x(F(x)G(xx(F(x)G(x)， x(G(xx(G(x) ) H(xH(x)结论：结论： xH(xxH(x) ) xF(xxF(x) )解答解答 80例题的证明例题的证明 xH(xxH(x) ) 附加前提引入附加前提引入 x(F(x)G(xx(F(x)G(x) ) 前提引入前提引入 H(cH(c) ) EI EI规则规则 F(cF(c) ) G(cG(c) ) UI UI规则规则 x(G(xx(G(x) ) H(xH(x) ) 前提引入前提引入 G(cG(c) ) H(cH(c) ) UIUI规则规则 G(cG(c) ) 拒取式拒取式 F(cF(c) ) 析取三段论析取三段论 ( (x)F(xx)F(x) ) EGEG规则规则 81作业作业习题五习题五课本上：课本上：2 2、3 3、习题本上：习题本上：1313、15(1,2)15(1,2)、2525