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

1、第四章 谓词演算的推理理论4.1 谓词演算的永真推理系统谓词演算的永真推理系统 4.1.1 公理系统的组成部分公理系统的组成部分 4.1.2 公里系统的推理过程公里系统的推理过程4.2谓词演算的假设推理系统谓词演算的假设推理系统4.3谓词演算的归结推理系统谓词演算的归结推理系统4.1.1 公理系统的组成部分公理系统的组成部分一、语法部分一、语法部分 (一一) 基本符号基本符号 (二二) 公理公理 (三三) 规则规则二、语义部分二、语义部分三、关于公理的几点说明三、关于公理的几点说明（一） 基本符号公理系统所允许出现的全体符号的集合。公理系统所允许出现的全体符号的集合。(1) 命题变元：命题变元

2、：P，Q，R，等字母表示命题变元等字母表示命题变元(2) 个体变元：个体变元：x，y，等小写字母表示个体变元等小写字母表示个体变元(3) 谓词变元：谓词变元：X，Y，等大写字母表示谓词变元等大写字母表示谓词变元(4) 联结词：联结词： 、 、 、是联结词是联结词(5) 量词：全称量词量词：全称量词 、存在量词、存在量词 (6) 括号：括号：(，)是括号是括号(7) 全称封闭符：全称封闭符：基本符号（续）(8) 合式公式：合式公式： (i) 原子命题原子命题P是合式公式；是合式公式； (ii) 谓词填式谓词填式A(x1，x2，x3，xn)是合式公式；是合式公式； (iii) 若若A是公式，则是公

3、式，则 A是合式公式；是合式公式； (iv) 若若A和和B是合式公式，则是合式公式，则 (A B)，(A B)，(AB)，(AB)为公式；为公式； (v) 若若A是合式公式，是合式公式，x是是A中出现的任何个体变元，中出现的任何个体变元， 则则 xA(x)， xA(x)为合式公式；为合式公式； (vi) 只有有限次使用只有有限次使用(i)、(ii)、(iii)、(iv)、(v)所得到所得到的式子才是合式公式。的式子才是合式公式。基本符号（续）(9) 全称封闭式：设全称封闭式：设 为含有为含有n个自由变元的公个自由变元的公式，如果在式，如果在 前用全称量词把前用全称量词把n个自由变元个自由变元约

4、束起来后所得到的公式，称为约束起来后所得到的公式，称为 的的全称全称封闭式封闭式。记为。记为 。 例例 写出下式的全称封闭式写出下式的全称封闭式 = xP(x，y)uQ(u，v)解：解： =( xP(x，y)uQ(u，v) = y v( xP(x，y)uQ(u，v)（二） 公理公理公理1 (PP)公理公理2 (P(QR)(Q(PR)公理公理3 (PQ)(QR)(PR)公理公理4 (P(PQ)(PQ)公理公理5 (PQ)(PQ)公理公理6 (PQ)(QP)公理公理7 (PQ)(QP)(PQ)调头调头传递传递凝缩凝缩与与有关有关（二） 公理公理公理8 (P Q)P)公理公理9 (P Q)Q)公理公

5、理10 (P(Q(P Q)公理公理11 (P(P Q)公理公理12 (Q(P Q)公理公理13 (PR)(QR)(P Q)R)公理公理14 (PQ)(QP)公理公理15 (PP)与与有关有关与与 有关有关与与有关有关（二） 公理公理公理20 ( xP(x) P(x)公理公理21 (P(x)x P(x)如果只有一个自由变元，公理如果只有一个自由变元，公理20与公理与公理21可以分可以分别理解如下：别理解如下： x( yP(y) P(x) x(P(x)y P(y)与与量词有关量词有关（三） 规则(1)分离规则：分离规则：如果如果(AB)且且A，则，则B。(2)全称规则：全称规则：( P(x)(x

6、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)

7、规则规定如何从永真公式推出永真公式。规则规定如何从永真公式推出永真公式。 分离规则指明，如果分离规则指明，如果(AB)永真且永真且A永真，则永真，则B也为永真公式。也为永真公式。(3) 定理为永真公式，它们是从公理出发利用定理为永真公式，它们是从公理出发利用上述规则推出来的公式。上述规则推出来的公式。三、关于公理的几点说明(1) 本系统中本系统中不引入代入规则不引入代入规则，它的作用由下，它的作用由下面的面的(2)来实现；来实现；(2) 本系统中的所有公理我们把它看作本系统中的所有公理我们把它看作公理模公理模式式，即只要形如某一公理，我们就称其为，即只要形如某一公理，我们就称其为某一公理。某一

8、公理。 如如 (PP)、 (P(QR)(P(QR)、 ( xP(x)x P(x) 等均为公理等均为公理1。第四章 谓词演算的推理理论4.1 谓词演算的永真推理系统谓词演算的永真推理系统 4.1.1 公理系统的组成部分公理系统的组成部分 4.1.2 公里系统的推理过程公里系统的推理过程4.2谓词演算的假设推理系统谓词演算的假设推理系统4.3谓词演算的归结推理系统谓词演算的归结推理系统例例1 (p41)已知已知定理定理(P(QP), 求证求证: 全全0规则规则 (x) x (x)证明：证明：(1) (x)(2) ( (x)(PP)(x) 引用定理引用定理 (3) (PP)(x) (2)(1)分离分

9、离(4) (PP)x (x) 全称规则全称规则(3)(5) (PP) 公理公理(1)(6) x (x) (4)(5)分离分离则有全则有全0规则规则 (x) x (x)全n规则、存n规则全全n规则：规则： ( 1( 2( n(x) ( 1( 2( nx (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) (

10、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) 证明: (1) x(P(x) ( P(x) )公理公理20 : P(x)与与P(x)同形同形(2) x(P(x) ( x P(x) )全全2规则规则( 1( 2(x) ( 1( 2x (x)例例(续续) x(P(x)(x P(x)再证明再证明 ( x P(x) x( P(x) ) 证明: (3) xP(x

11、)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)(RP)(RQ) 例例 (再续再续) 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

12、)(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( xP(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) 全称

13、规则例例(再续再续) 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(QP) (B) (PP) 及分离规则和全称规则，全称规则为：及分离规则和全称规则，全称规则为： ( 1

14、( 2(x)( 1( 2x (x)试证：全试证：全0规则规则 (x) x (x)证证: (1) (x) (2) (P(QP) 公理公理A (3) ( (x) (PP) (x) 代入代入(1) (4) (PP) (x) (1)(3)分离分离 (5) (PP) (x) (PP) (PP) (x) 代入代入(2) (6) (PP) (PP) (x) (4)(5)分离分离 (7) (PP) (PP) x (x) 全称规则全称规则 (8) (PP) 公理公理B (9) (PP) x (x) (7)(8)分离分离 (10) ( x (x) (9)(8)分离分离例例2 (p42) 试证明：试证明：(A) (

15、 x P(x) xP(x)证证(A)(1) ( x P(x)P(x) 公理公理20(2) ( 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)(5) ( xP(x)x P(x)( x P(x)xP(x) 公理公理14(6) ( x P(x)xP(x) (5)(4)分离分离 例例2 (p42) 已知定理：已知定理：(PQ)( QP)试证明：试证明： (B) (xP(x)x P(x)证证(B)(7) (P(x)xP(x) 公理公理21(8) (P(x)xP(x)

16、(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)两式两式(6)( 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) (PQ(x) (P xQ(x)证明：证明：(1)(Q(x)xQ(x)公理公理21(2)(PQ(x)(Q(x) xQ(x)(P xQ(x)公理公理3(3)(PQ(