一阶逻辑等值演算与推理ch5.ppt

本章说明 本章的主要内容一阶逻辑等值式与基本等值式置换规则 换名规则 代替规则前束范式一阶逻辑推理理论本章与其他各章的关系本章先行基础是前四章本章是集合论各章的先行基础 本章主要内容 5 1一阶逻辑等值式与置换规则5 2一阶逻辑前束范式5 3一阶逻辑的推理理论 5 1一阶逻辑等值式与置换规则 在一阶逻辑中 有些命题可以有不同的符号化形式 例如 没有不犯错误的人令M x x是人 F x x犯错误 则将上述命题的符号化有以下两种正确形式 1 x M x F x 2 x M x F x 我们称 1 和 2 是等值的 说明 等值式的定义 定义5 1设A B是一阶逻辑中任意两个公式 若A B是永真式 则称A与B是等值的 记做A B 称A B是等值式 例如 判断公式A与B是否等值 等价于判断公式A B是否为永真式 谓词逻辑中关于联结词的等值式与命题逻辑中相关等值式类似 说明 一阶逻辑中的一些基本而重要等值式 代换实例消去量词等值式量词否定等值式量词辖域收缩与扩张等值式量词分配等值式 代换实例 由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式 因而第二章的16组等值式模式给出的代换实例都是一阶逻辑的等值式的模式 例如 1 xF x xF x 双重否定律 2 F x G y F x G y 蕴涵等值式 3 x F x G y zH z x F x G y zH z 蕴涵等值式 消去量词等值式 设个体域为有限集D a1 a2 an 则有 1 xA x A a1 A a2 A an 2 xA x A a1 A a2 A an 5 1 量词否定等值式 设A x 是任意的含自由出现个体变项x的公式 则 1 xA x x A x 2 xA x x A x 否定内移 量词互换 任意变存在 存在变任意 说明 并不是所有的x都有性质A 与 存在x没有性质A 是一回事 不存在有性质A的x 与 所有X都没有性质A 是一回事 5 2 量词辖域收缩与扩张等值式 设A x 是任意的含自由出现个体变项x的公式 B中不含x的出现 则 1 x A x B xA x B x A x B xA x B x A x B xA x B x B A x B xA x 2 x A x B xA x B x A x B xA x B x A x B xA x B x B A x B xA x 5 3 5 4 证明 xA x B x A x B xA x B xA x B x A x B x A x B x A x B 量词分配等值式 设A x B x 是任意的含自由出现个体变项x的公式 则 1 x A x B x xA x xB x 2 x A x B x xA x xB x 5 5 例如 联欢会上所有人既唱歌又跳舞 和 联欢会上所有人唱歌且所有人跳舞 这两个语句意义相同 故有 1 式 由 1 式推导 2 式 x A x B x xA x xB x x A x B x x A x x B x x A x B x xA x xB x x A x B x xA x xB x 一阶逻辑等值演算的三条原则 置换规则 设 A 是含公式A的公式 B 是用公式B取代 A 中所有的A之后的公式 若A B 则 A B 换名规则 设A为一公式 将A中某量词辖域中某约束变项的所有出现及相应的指导变元改成该量词辖域中未曾出现过的某个体变项符号 公式的其余部分不变 设所得公式为A 则A A 代替规则 设A为一公式 将A中某个自由出现的个体变项的所有出现用A中未曾出现过的个体变项符号代替 A中其余部分不变 设所得公式为A 则A A 说明 一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同 只是在这里A B是一阶逻辑公式 嗨 别睡了 例5 1 例5 1将下面公式化成与之等值的公式 使其没有既是约束出现又是自由出现的个体变项 1 xF x y z yG x y z 2 x F x y yG x y z 1 xF x y z yG x y z tF t y z yG x y z 换名规则 tF t y z wG x w z 换名规则 或 xF x y z yG x y z xF x t z yG x y z 代替规则 xF x t z yG w y z 代替规则 解答 例5 1的解答 2 x F x y yG x y z x F x t yG x y z 代替规则 或 x F x y yG x y z x F x y tG x t z 换名规则 解答 例5 2 例5 2证明 1 x A x B x xA x xB x 2 x A x B x xA x xB x 其中A x B x 为含x自由出现的公式 只要证明在某个解释下两边的式子不等值 取解释I 个体域为自然数集合N 1 取F x x是奇数 代替A x 取G x x是偶数 代替B x 则 x F x G x 为真命题 而 xF x xG x 为假命题 两边不等值 证明 例5 2 2 x A x B x xA x xB x x F x G x 有些x既是奇数又是偶数为假命题 而 xF x xG x 有些x是奇数并且有些x是偶数为真命题 两边不等值 证明 说明 全称量词 对 无分配律 存在量词 对 无分配律 当B x 换成没有x出现的B时 则有 x A x B xA x B x A x B xA x B 例5 3 消去量词 例5 3设个体域为D a b c 将下面各公式的量词消去 1 x F x G x 2 x F x yG y 3 x yF x y 说明 如果不用公式 5 3 将量词的辖域缩小 演算过程较长 注意 此时 yG y 是与x无关的公式B 解答 1 x F x G x F a G a F b G b F c G c 2 x F x yG y xF x yG y 公式5 3 F a F b F c G a G b G c 例5 3 消去量词 3 x yF 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 在演算中先消去存在量词也可以 得到结果是等值的 x yF x y yF a y yF b y yF c y 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 例5 4 例5 4给定解释I如下 a 个体域D 2 3 b D中特定元素 c D上的特定函数 x 为 d D的特定谓词 在解释I下求下列各式的值 1 x F x G x a 2 x F f x G x f x 3 x yL x y 4 y xL x y 例5 4的解答 1 x F x G x a F 2 G 2 2 F 3 G 3 2 0 1 1 1 0 2 x F f x G x f x F f 2 G 2 f 2 F f 3 G 3 f 3 F 3 G 2 3 F 2 G 3 2 1 1 0 1 1 例5 4的解答 3 x yL x y L 2 2 L 2 3 L 3 2 L 3 3 1 0 0 1 1 4 y xL x y y L 2 y L 3 y L 2 2 L 3 2 L 2 3 L 3 3 1 0 0 1 0 说明 由 3 4 的结果进一步可以说明量词的次序不能随意颠倒 例5 5 例5 5证明下列等值式 1 x M x F x x M x F x 2 x F x G x x F x G x 3 x y F x G y H x y x y F x G y H x y 4 x y F x G y L x y x y F x G y L x y 例5 5的证明 1 x M x F x x M x F x x M x F x x M x F x x M x F x x M x F x 2 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 例5 5的证明 3 x y F x G y H x y x y F x G y H x y x y F x G y H x y x y F x G y H x y x y F x G y H x y x y F x G y H x y 例5 5的证明 4 x y F x G y L x y x y F x G y L x y x y F x G y L x y x y F x G y L x y x y F x G y L x y x y F x G y L x y x y F x G y L x y 5 2一阶逻辑前束范式 定义5 2设A为一个一阶逻辑公式 若A具有如下形式Q1x1Q2x2 QkxkB则称A为前束范式 其中Qi 1 i k 为 或 B为不含量词的公式 前束范式的例子 x y F x G y H x y x y z F x G y H z L x y z 不是前束范式的例子 x F x y G y H x y x F x y G y H x y 前束范式存在定理 定理5 1一阶逻辑中的任何公式都存在与之等值的前束范式 说明 求前束范式的过程 就是制造量词辖域可以扩大的条件 进行量词辖域扩大 任何公式的前束范式都是存在的 但一般说来 并不唯一 利用一阶逻辑等值式以及三条变换规则 置换规则 换名规则 代替规则 就可以求出与公式等值的前束范式 或所谓公式的前束范式 1 利用量词转化公式 把否定深入到指导变元的后面 xA x x A x xA x x A x 2 利用 x A x B xA x B和 x A x B xA x B把量词移到全式的最前面 这样便得到前束范式 例5 6求公式的前束范式 1 xF x xG x xF x yG y 换名规则 xF x y G y 5 2 第二式 x F x y G y 5 3 第二式 x y F x G y 5 3 第二式 y x F x G y 或者 xF x xG x xF x x G x 5 2 第二式 x F x G x 5 5 第一式 例5 6求公式的前束范式 2 xF x xG x xF x x G x 5 2 第二式 xF x y G y 换名规则 x F x y G y 5 3 第一式 x y F x G y 5 3 第一式 说明 公式的前束范式是不唯一的 例5 7求前束范式 1 xF x xG x yF y xG x y x F y G x 2 xF x xG x yF y xG x y x F y G x 3 xF x xG x yF y xG x y x F y G x 4 xF x yG y x y F x G x 例5 8求公式的前束范式 1 xF x y yG x y tF t y wG x w 换名规则 t w F t y G x w 5 3 5 4 或者 xF x y yG x y xF x t yG w y 代替规则 x y F x t G w y 5 3 5 4 说明 解本题时一定注意 哪些个体变项是约束出现 哪些是自由出现 特别要注意那些既是约束出现又是自由出现的个体变项 不能混淆 例5 8求公式的前束范式 2 x1F x1 x2 x2G x2 x1H x1 x2 x3 x4F x4 x2 x5G x5 x1H x1 x2 x3 x4 x5 F x4 x2 G x5 x1H x1 x2 x3 x4 x5 x1 F x4 x2 G x5 H x1 x2 x3 5 3一阶逻辑的推理理论 在一阶逻辑中 从前提A1 A2 Ak出发推结论B的推理形式结构 依然采用如下的蕴涵式形式A1 A2 Ak B 5 6 若式 5 6 为永真式 则称推理正确 否则称推理不正确 于是 在一阶逻辑中判断推理是否正确也归结为判断 5 6 式是否为永真式了 在一阶逻辑中称永真式的蕴涵式为推理定律 若一个推理的形式结构正是某条推理定律 则这个推理显然是正确的 在一阶逻辑的推理中 某些前提与结论可能是受量词限制 为了使用命题逻辑中的等值式和推理定律 必须在推理过程中有消去和添加量词的规则 以便使谓词演算公式的推理过程可类似于命题演算中推理理论那样进行 推理定律的来源 命题逻辑推理定律的代换实例由基本等值式生成的推理定律量词分配等值式推理规则 量词消去和引入规则 命题逻辑推理定律的代换实例 xF x yG y xF x 化简律的代换实例 xF x xF x yG y 附加律的代换实例 由基本等值式生成的推理定律 xF x xF x xF x xF x xF x x F x x F x xF x 其他推理定律 xA x xB x x A x B x x A x B x xA x xB x x A x B x xA x xB x x A x B x xA x xB x 对 x A x B x xA x xB x 的讨论若 x A x B x 为真 则有一个客体c 使得A c B c 为真 即A c 和B c 都为真 所以 xA x xB x 也为真 推理规则 为了构造推理系统 还要给出4条重要的推理规则 即消去量词和引入量词的规则 1 全称量词消去规则 简记为 2 全称量词引入规则 简记为 3 存在量词引入规则 简称E 4 存在量词消去规则 简记为E 全称量词消去规则 简记为 含义 如果个体域的所有元素都具有性质A 则个体域中的任一元素具有性质A 两式成立的条件 1 在第一式中 取代x的y应为任意的不在A x 中约束出现的个体变项 2 在第二式中 c为个体常项 3 用y或c去取代A x 中自由出现的x时 一定要在x自由出现的一切地方进行取代 全称量词消去规则 简记为 举例 当A x 为原子公式时 比如A x F x 则当 xA x 为真时 对于个体域中任意的个体变项y 不会出现F y 为假的情况 当A x 不是原子公式时 如y已在A x 中约束出现了 就不能用y取代x 否则会出现 xA x 为真而A y 为假的情况 考虑个体域为实数集合 公式A x yF x y 为x y 当对公式 xA x x yF x y 使用 规则时 用y取代x 就会得到A y yF y y 即 y y y 这显然是假命题 原因是违背了条件 1 若用z取代x 得A z yF z y y z y 就不会产生这种错误 全称量词引入规则 简记为 该式成立的条件是 1 无论A y 中自由出现的个体变项y取何值 A y 应该均为真 2 取代自由出现的y的x也不能在A y 中约束出现 举例 取个体域为实数集 F x y 为x y A y xF x y 显然A y 满足条件 1 对A y 应用 规则时 若取已约束出现的x取代y 会得到 xA x x x x x 这是假命题 产生这种错误的原因是违背了条件 2 若取z取代y 得 zA z z x x z 为真命题 存在量词引入规则 简称 该式成立的条件是 1 c是特定的个体常项 2 取代c的x不能在A c 中出现过 举例 取个体域为实数集 F x y 为x y 取A 5 xF x 5 显然A 5 是真命题 在应用E 规则时 若用A 5 中已出现的x取代5 得 x xF x x x x x 这是假命题 产生这种错误的原因是违背了条件 2 若用A 5 中未出现过的个体变项y取代5 得 yA y y xF x y 这为真命题 存在量词消去规则 简记为 该式成立的条件是 1 c是使A为真的特定的个体常项 2 c不在A x 中出现 3 若A x 中除自由出现的x外 还有其它自由出现的个体变项 此规则不能使用 举例 取个体域为自然数集合 F x 为x是奇数 G x 为x是偶数 xF x 与 xG x 都是真命题 则对于某些c和d 可以断定F c G d 必定为真 但不能断定F c G c 是真 对 xF x 使用 规则时 取代x的c一定是特定的个体常项1 3 5等奇数 对 xG x 使用E 规则时 取代x的c一定是特定的个体常项2 4 6等偶数 定义5 3自然推理系统定义 1 字母表 同一阶语言的字母表 2 合式公式 同合式公式的定义 3 推理规则 1 前提引入规则 2 结论引入规则 3 置换规则 4 假言推理规则 5 附加规则 6 化简规则 7 拒取式规则 8 假言三段论规则 9 析取三段论规则 10 构造性二难推理规则 11 合取引入规则 12 规则 13 规则 14 规则 15 规则 例题 例题在自然推理系统中 构造下面推理的证明所有的人都是要死的 苏格拉底是人 所以苏格拉底是要死的 解 先将原子命题符号化 设F x x是一个人 G x x是要死的 s 苏格拉底 前提 x F x G x F s 结论 G s 证明 x F x G x 前提引入 F s G s F s 前提引入 G s 假言推理 例5 9 例5 9设个体域为实数集合 F x y 为x y 指出在推理系统F中 以 x yF x y 真命题 为前提 推出 xF x c 假命题 的下述推理证明中的错误 x yF x y 前提引入 yF z y F z c E xF x c 解由于c为特定的个体常项 所以 xF x c 即为 x x c 为假命题 如果按F中推理规则进行推理 不会从真命题推出假命题 在以上推理证明中 第三步错了 由于F z y 中除有自由出现的y 还有自由出现的z 按E 规则应该满足的条件 3 此处不能用E 规则 用了E 规则 导致了从真命题推出假命题的错误 例5 10 例5 10在自然推理系统中 构造下面推理的证明任何自然数都是整数 存在着自然数 所以存在着整数 个体域为实数集合R 解 先将原子命题符号化 设F x x为自然数 G x x为整数 前提 x F x G x xF x 结论 xG x 证明 xF x 前提引入 F c E x F x G x 前提引入 F c G c G c 假言推理 xG x E 例5 10说明 以上证明的每一步都是严格按推理规则及应满足的条件进行的 因此 前提的合取为真时 结论必为真 但如果改变命题序列的顺序会产生由真前提推出假结论的错误 如果证明如下进行 x F x G x 前提引入 F c G c xF x 前提引入 F c E 在 中取c 则F G 为真 前件假 于是 中F 为假 这样从前件真推出了假的中间结果 例5 11 例5 11在自然推理系统F中 构造下面推理的证明 前提 x F x G x x F x H x 结论 x G x H x 提示在证明序列中先引进带存在量词的前提 例5 11证明 x F x H x 前提引入 F c H c E x F x G x 前提引入 F c G c F c 化简 G c 假言推理 H c 化简 G c H c 合取 G x H x E 例5 12 例5 12在自然推理系统F中 构造下面推理的证明 不存在能表示成分数的无理数 有理数都能表示成分数 因此 有理数都不是无理数 个体域为实数集合 设F x x为无理数 G x x为有理数 H x x能表示成分数 前提 x F x H x x G x H x 结论 x G x F x 解答 例5 12证明 x F x H x 前提引入 x F x H x 置换 x H x F x 置换 H y F y x G x H x 前提引入 G y H y G y F y 假言三段论 x G x F x 注意 x F x H x 不是前束范式 因而不能对它使用 规则 因为结论中的量词是全称量词 因而在使