主要内容 l 一阶逻辑等值式与基本的等值式 l 置换规则、换名规则、代替规则 l 前束范式 l 自然推理系统NL 及其推理规则第五章 一阶逻辑等值演算与推理15.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)2基本等值式(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) 3基本等值式关于存在量词的： 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) 注意：对，对无分配律4置换规则、换名规则、代替规则1. 置换规则设(A)是含A的公式, 那么, 若AB, 则(A)(B). 2. 换名规则设A为一公式，将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号，其余部分不变，设所得公式为A，则AA. 3. 代替规则设A为一公式，将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替，其余部分不变，设所得公式为A，则AA.5实例例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) 置换6实例(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) 置换7实例例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) 辖域扩张等值式8实例例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) 9实例解法二 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)例3 设个体域D=a,b,c, 消去下述公式中的量词: (1) xy(F(x)G(y)10实例(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)例3 设个体域D=a,b,c, 消去下述公式中的量词: 115.2 一阶逻辑前束范式定义5.2 设A为一个一阶逻辑公式，若A具有如下形式Q1x1Q2x2QkxkB 则称A为前束范式，其中Qi (1 i k)为或，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) 不是前束范式， 12前束范式存在定理定理5.1（前束范式存在定理）一阶逻辑中的任何公式都存在与之等值的前束范式例4 求下列公式的前束范式(1) x(M(x)F(x) 解 x(M(x)F(x) x(M(x)F(x) （量词否定等值式） x(M(x)F(x) 后两步结果都是前束范式，说明公式的前束范式不惟一.13求前束范式的实例(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) 辖域收缩扩张规则14求前束范式的实例(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) 辖域收缩扩张规则155.3 一阶逻辑的推论理论推理的形式结构 1. A1A2Ak B若次式是永真式, 则称推理正确, 记作A1A2Ak B 2. 前提: A1, A2, Ak 结论: B推理定理: 永真式的蕴涵式16推理定律第一组 命题逻辑推理定律的代换实例如, 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)17量词消去引入规则1. 全称量词消去规则(-)或 其中x,y是个体变项符号, c是个体常项符号, 且在A中x不在y 和y的辖域内自由出现. 2. 全称量词引入规则(+)其中x是个体变项符号, 且不在前提的任何公式中自由出现xA(x) A(y)xA(x) A(c)A(x) xA(x)18量词消去引入规则3. 存在量词消去规则(-)其中x是个体变项符号, 且不在前提的任何公式和B中自由出现A(x)B xA(x)B19量词消去引入规则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)20自然推理系统NL定义5.3 自然推理系统NL 定义如下: 1. 字母表. 同一阶语言L 的字母表 2. 合式公式. 同L 的合式公式3. 推理规则: (1) 前提引入规则 (2) 结论引入规则 (3) 置换规则 (4) 假言推理规则 (5) 附加规则 (6) 化简规则 (7) 拒取式规则21自然推理系统NL(8) 假言三段论规则 (9) 析取三段论规则 (10) 构造性二难推理规则 (11) 合取引入规则 (12) -规则 (13) +规则 (14) -规则 (15) +规则推理的证明22构造推理证明的实例例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) 假言推理 23构造推理证明的实例 例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) -24构造推