一阶逻辑等值式

1、12.3 一阶逻辑等值式一阶逻辑等值式等值式等值式基本等值式基本等值式量词否定等值式量词否定等值式量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式量词分配等值式量词分配等值式前束范式前束范式 2等值式与基本等值式等值式与基本等值式 基本等值式基本等值式:命题逻辑中命题逻辑中1616组基本等值式的代换实例组基本等值式的代换实例如，如， xF(x) xF(x) xF(x) xF(x)yG(y) xF(x)yG(y) ( xF(x)yG(y) xF(x)yG(y) 定义定义 设设A、B是一阶逻辑中的任意两个公式，若是一阶逻辑中的任意两个公式，若AB为逻辑有效式，则称为逻辑有效式，则称A与与B是是等值

2、等值的，记作的，记作 AB，并称并称AB为为等值式等值式. 3基本等值式基本等值式:消去量词等值式消去量词等值式 设设D=a1,a2,an (1) xA(x)A(a1) A(a2) A(an) (2) xA(x)A(a1) A(a2) A(an)量词否定等值式量词否定等值式 (1) xA(x) x A(x) (2) xA(x) x A(x) 4基本等值式基本等值式( (续续) )量词辖域收缩与扩张等值式量词辖域收缩与扩张等值式 设设A(x)是含是含x自由出现的公式，自由出现的公式，B中不含中不含x的出现的出现关于全称量词的：关于全称量词的： x(A(x) B)xA(x) B x(A(x) B)

3、xA(x) B x(A(x)B)xA(x)B x(BA(x)BxA(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)5基本的等值式基本的等值式( (续续) )量词分配等值式量词分配等值式 x(A(x) B(x)xA(x)xB(x) x(A(x) B(x)xA(x)xB(x)注意：注意： 对对 无分配律，无分配律， 对对 无分配律无分配律 量词等值式量词等值式 x y A(x,y) y x A(x,y) x y y x A(x,y)其中其中A(x,y) 是是x,y自由出现的谓词公式自

4、由出现的谓词公式6基本的等值式基本的等值式( (续续) )例例 将下面命题用两种形式符号化将下面命题用两种形式符号化 (1) 没有不犯错误的人没有不犯错误的人 (2) 不是所有的人都爱看电影不是所有的人都爱看电影解解 (1) 令令F(x)：x是人，是人，G(x)：x犯错误犯错误. x(F(x)G(x) x(F(x)G(x) 请给出演算过程，并说明理由请给出演算过程，并说明理由. (2) 令令F(x)：x是人，是人，G(x)：爱看电影：爱看电影. x(F(x)G(x) x(F(x)G(x) 给出演算过程，并说明理由给出演算过程，并说明理由. 7前束范式前束范式 例如，例如， x y(F(x)(G

5、(y) H(x,y) x (F(x) G(x)是前束范式是前束范式, 而而 x(F(x)y(G(y) H(x,y) x(F(x) G(x)不是前束范式，不是前束范式，定义定义 设设A为一个一阶逻辑公式为一个一阶逻辑公式, 若若A具有如下形式具有如下形式Q1x1Q2x2QkxkB, 则称则称A为为前束范式前束范式, 其中其中Qi (1 i k)为为 或或 ，B为不含量词的公式为不含量词的公式.8公式的前束范式公式的前束范式 定理（前束范式存在定理）定理（前束范式存在定理）一阶逻辑中的任何公一阶逻辑中的任何公式都存在与之等值的前束范式式都存在与之等值的前束范式 注意注意: : 公式的前束范式不惟一

6、公式的前束范式不惟一 求公式的前束范式的方法求公式的前束范式的方法: : 利用重要等值式、利用重要等值式、 置换规则、换名规则、代替规则进行等值演算置换规则、换名规则、代替规则进行等值演算. . 9换名规则与代替规则换名规则与代替规则 换名规则换名规则: : 将量词辖域中出现的某个约束出现的将量词辖域中出现的某个约束出现的个体变项及对应的指导变项，改成另一个辖域中未个体变项及对应的指导变项，改成另一个辖域中未曾出现过的个体变项符号，公式中其余部分不变，曾出现过的个体变项符号，公式中其余部分不变，则所得公式与原来的公式等值则所得公式与原来的公式等值. .代替规则代替规则: : 对某自由出现的个体

7、变项用与原公式对某自由出现的个体变项用与原公式中所有个体变项符号不同的符号去代替，则所得公中所有个体变项符号不同的符号去代替，则所得公式与原来的公式等值式与原来的公式等值. . 10公式的前束范式公式的前束范式( (续续) )例例 求下列公式的前束范式求下列公式的前束范式 (1) x(M(x) F(x)解解 x(M(x) F(x) x( M(x)F(x) （量词否定等值式）（量词否定等值式） x(M(x)F(x) 两步结果都是前束范式，说明前束范式不惟一两步结果都是前束范式，说明前束范式不惟一.11例例( (续续) ) (2) xF(x)xG(x)解解 xF(x)xG(x) xF(x)x G(

8、x) （量词否定等值式）（量词否定等值式） x(F(x)G(x) （量词分配等值式）（量词分配等值式）另有一种形式另有一种形式 xF(x)xG(x) xF(x)x G(x) xF(x)y G(y) ( 代替规则代替规则 ) x y(F(x)G(y) ( 量词辖域扩张量词辖域扩张 )两种形式是等值的两种形式是等值的 12例例( (续续) ) (3) xF(x)xG(x) 解解 xF(x)xG(x) xF(x)x G(x) x(F(x)G(x) （为什么？）（为什么？） 或或 x y(F(x)G(y) （为什么？）（为什么？） (4) xF(x)y(G(x,y)H(y) 解解 xF(x)y(G(x

9、,y)H(y) zF(z)y(G(x,y)H(y) （换名规则）（换名规则） z y(F(z)(G(x,y)H(y) （为什么？）（为什么？）13例例( (续续) )或或 xF(x)y(G(z,y)H(y) （代替规则）（代替规则） x y(F(x)(G(z,y)H(y) (5) x(F(x,y)y(G(x,y) H(x,z)解解 用换名规则用换名规则, 也可用代替规则也可用代替规则, 这里用代替规则这里用代替规则 x(F(x,y)y(G(x,y) H(x,z) x(F(x,u)y(G(x,y) H(x,z) x y(F(x,u)G(x,y) H(x,z)注意：注意： x与与 y不能颠倒不能颠

10、倒 142.4 一阶逻辑推理理论一阶逻辑推理理论推理的形式结构推理的形式结构判断推理是否正确的方法判断推理是否正确的方法重要的推理定律重要的推理定律推理规则推理规则构造证明构造证明附加前提证明法附加前提证明法 15推理推理 推理的形式结构推理的形式结构有两种：有两种： 第一种第一种 A1 A2 AkB (*) 第二种第二种 前提：前提：A1，A2，Ak 结论：结论： B其中其中 A1,A2,Ak,B为一阶逻辑公式为一阶逻辑公式. 若若(*)为永真式为永真式, 则称则称推理正确推理正确, 否则称否则称推理不正确推理不正确.判断方法判断方法: 真值表法真值表法, 等值演算法等值演算法, 主析取范式

11、法及构造证主析取范式法及构造证明法明法. 前前3种方法采用第一种形式结构种方法采用第一种形式结构, 构造证明构造证明法采用第二种形式结构法采用第二种形式结构.16重要的推理定律重要的推理定律 第一组第一组 命题逻辑推理定律代换实例命题逻辑推理定律代换实例 如如 xF(x)yG(y)xF(x)为化简律代换实例为化简律代换实例. 第二组第二组 由基本等值式生成由基本等值式生成 如如 由由 xA(x)x A(x) 生成生成 xA(x)x A(x), x A(x)xA(x), 第三组第三组 xA(x)xB(x)x(A(x) B(x) x(A(x) B(x)xA(x)xB(x) x（A(x) B(x)）

12、 xA(x) x B(x)） x（A(x) B(x)） xA(x) x B(x)）17推理规则推理规则 (1)(1)前提引入规则前提引入规则 (2)(2)结论引入规则结论引入规则(3)(3)置换规则置换规则 (4)(4)假言推理规则假言推理规则(5)(5)附加规则附加规则 (6)(6)化简规则化简规则(7)(7)拒取式规则拒取式规则 (8)(8)假言三段论规则假言三段论规则(9)(9)析取三段论规则析取三段论规则 (10)(10)构造性二难推理规则构造性二难推理规则(11)(11)合取引入规则合取引入规则 18推理规则推理规则( (续续) )(12) 全称量词消去规则（简记为全称量词消去规则（

13、简记为UI规则或规则或UI）两式成立的条件是：两式成立的条件是： x是是A(x)中的自由出现的个体变项中的自由出现的个体变项 在第一式中，取代在第一式中，取代x的的y应为任意的不在应为任意的不在A(x)中中约束出现的个体变项约束出现的个体变项. 在第二式中，在第二式中，c为任意个体常项为任意个体常项. 用用y或或c去取代去取代A(x)中的自由出现的中的自由出现的x时，一定要时，一定要在在x自由出现的一切地方进行取代自由出现的一切地方进行取代.)()()()(cAxxAyAxxA 或或19推理规则推理规则( (续续) )(13) 全称量词引入规则（简记为全称量词引入规则（简记为UG规则或规则或U

14、G） 该式成立的条件是：该式成立的条件是： y是是A(y)中自由出现的个体变项；中自由出现的个体变项； 无论无论y取何值，取何值，A(y)应该均为真；应该均为真； 取代自由出现的取代自由出现的y的的x，也不能，也不能在在A(y)中约束出中约束出现现. )()(xxAyA 20推理规则推理规则( (续续) )(14) 存在量词引入规则（简记为存在量词引入规则（简记为EG规则或规则或EG） 该式成立的条件是：该式成立的条件是： c是使是使A为真的特定个体常项为真的特定个体常项. 取代取代c的的x不能在不能在A(c)中出现过中出现过. )()(xxAcA 21推理规则推理规则( (续续) )(15)

15、 存在量词消去规则存在量词消去规则（简记为简记为EI规则或规则或EI） 该式成立的条件是：该式成立的条件是： c是使是使A为真的特定的个体常项为真的特定的个体常项. c不在不在A(x)中出现中出现. 若若A(x)中除自由出现的中除自由出现的x外，还有其他自由出现外，还有其他自由出现的个体变项，此规则不能使用的个体变项，此规则不能使用.)()(cAxxA 22构造推理证明构造推理证明 例例1 证明苏格拉底三段论证明苏格拉底三段论: “人都是要死的人都是要死的, 苏格拉苏格拉底是人，所以苏格拉底是要死的底是人，所以苏格拉底是要死的.” 令令 F(x): x是人是人, G(x): x是要死的是要死的

16、, a: 苏格拉底苏格拉底 前提：前提： x(F(x)G(x)，F(a) 结论：结论：G(a) 证明：证明： F(a) 前提引入前提引入 x(F(x)G(x) 前提引入前提引入 F(a)G(a) UI G(a) 假言推理假言推理注意：使用注意：使用UI时，用时，用a取代取代x .23构造推理证明构造推理证明( (续续) )例例2 乌鸦都不是白色的乌鸦都不是白色的. 北京鸭是白色的北京鸭是白色的. 因此，因此，北京鸭不是乌鸦北京鸭不是乌鸦. 令令 F(x): x是乌鸦是乌鸦, G(x): x是北京鸭是北京鸭, H(x): x是白色的是白色的前提：前提： x(F(x)H(x)， x(G(x)H(x

17、)结论：结论： x(G(x)F(x)24例例2( (续续) )证明：证明： 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) UG25构造推理证明构造推理证明( (续续) )例例3 构造下述推理证明构造下述推理证明 前提：前提： x(F(x)G(x)， xF(x) 结论：结论： xG(x)证明：证明： xF(x) 前提引入前提引入 x(F(x)G(x) 前提引入前提引入 F(c) EI F(c)G(c) UI G(c) 假言推理假言推理 xG(x) EG注意：必须先消存在量词注意：必须先消存在量词 26构造推理证明构造推理证明( (续续) )例例4 构造下述推理证明构造下述推理证明 前提：前提： xF(x)xG(x) 结论：结论： x(F(x)G(x)证明：证明： xF(x)xG(x) 前提引入前提引入 x y(F(x)G(y) 置换置换 x(F(x)G(z) UI F(z)G(z) UI x(F(