第五章 一阶逻辑等值演算与推理.ppt

第五章一阶逻辑等值演算与推理 本章的主要内容一阶逻辑等值式与基本的等值式置换规则 换名规则 代替规则前束范式一阶逻辑推理理论本章与其他各章的关系本章的先行基础是前四章本章是集合论各章的先行基础 5 1一阶逻辑等值式与置换规则 一 等值式与基本的等值式 1 等值式 定义5 1 A B当且仅当A B为永真式 A与B为任意的一阶逻辑公式 注意 与定义2 1的区别与联系 2 基本的等值式第一组 命题逻辑中16组基本等值式代换实例 例如 xF x yG y xF x yG y p q p q的代换实例 第二组 本章新给出 1 消去量词等值式D a1 a2 an xA x A a1 A a2 A an xA x A a1 A a2 A an 2 量词否定等值式 xA x x A x xA x x A x 例 设个体域D a b c 消去下列各公式的量词 1 x F x G x 2 x F x yG y 3 x yF x y 解 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 F a F b F c G a G b G c 解 3 x y F 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 注意 也可以先消存在量词 得到的结果是等值的 练习 在有限个体域内消去下列公式的量词 1 个体域 D 1 2 3 x y F x G y 2 个体域 D a b x y F x y G y 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 B A x B xA x 关于全称量词的 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 4 量词分配等值式 x A x B x xA x xB x x A x B x xA x xB x 注意 对 无分配律 对 无分配律 例 证明 1 x A x B x 与 xA x xB x 不等值 2 x A x B x 与 xA x xB x 不等值 证明 1 取解释I为 个体域为自然数集合N A x 解释为 x是奇数 B x 解释为 x是偶数 则 x A x B x 为真命题 而 xA x xB x 为假命题 2 取解释I为 个体域为自然数集合N A x 解释为 x是奇数 B x 解释为 x是偶数 则 x A x B x 为假命题 而 xA x xB x 为真命题 二 置换规则 换名及代替规则1 置换规则 同命题逻辑 2 换名规则设A为一公式 将A中某量词辖域中约束变项的所有出现及相应的指导变元 改成该量词辖域中未曾出现过的某个体变项符号 公式中其余部分不变 设所得公式为A 则A A 3 代替规则设A为一公式 将A中某个自由出现的个体变项的所有出现用A中未曾出现过的某个体变项符号代替 A中其余部分不变 设所得公式为A 则A A 例 将下列公式化成与其等值的公式 使其不含既是约束出现又是自由出现的个体变项 1 xF x y z yG x y z 2 x F x y yG x y z 例将下面命题用两种形式符号化 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 例 证明下列等值式 1 x M x F x x M x F x 2 x M x F x x M x F 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 2一阶逻辑前束范式 一 前束范式与命题公式的前束范式1 前束范式 定义5 2设A为一个一阶逻辑公式 若A具有形式Q1x1Q2x2 QkxkB则称A为前束范式 其中Qi 1 i k 为 或 B为不含量词的公式 x F x y G y H x y x y F x G y H x y x F x G x x F x G x 不是 是 不是 是 2 公式的前束范式定理5 1 前束范式存在定理 一阶逻辑中的任何公式都存在与之等值的前束范式 不惟一 3 如何求公式的前束范式利用重要等值式 置换规则 换名规则 代替规则进行等值演算 例求下列公式的前束范式 1 x M x F x 2 xF x xG x 3 xF x xG x 4 xF x y G x y H y 5 x F x y y G x y H x z 解 1 x M x F x x M x F x 量词否定等值式 x M x F x 两步结果都是前束范式 说明不惟一性 2 xF x xG x xF x x G x 量词否定等值式 x F x G x 量词分配等值式 3 xF x xG x xF x x G x x F x G x 为什么 或 x y F x G y 为什么 另有一种形式 xF x xG x xF x x G x xF x y G y x y F x G y 两种形式等值吗 4 xF x y G x y H y zF z y G x y H y 换名规则 z y F z G x y H y 为什么 或 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 u y G x y H x z x y F x u G x y H x z 注意 x与 y不能颠倒 练习 求下列公式的前束范式 1 xF x y yG x y 2 xF x y yG y xH x y z 5 3一阶逻辑的推理理论 一 推理的形式结构以及推理正确与错误1 形式结构 A1 A2 Ak B 其中 A1 A2 Ak B为一阶逻辑公式 若 为永真式 则推理正确 2 判断方法判 是否为永真式很难 本章主要介绍在形式系统F中构造证明 采用的形式结构为前提 A1 A2 Ak结论 B 二 重要的推理定律 如 xF x yG y xF x 为化简律代换实例 第二组由上节基本等值式生成 如由 xA x x A x 生成 xA x x A x 与 x A x xA 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 注意 反向蕴涵式不成立 三 量词消去或引入规则 两式成立的条件是 1 在第一式中 取代x的y应为任意的不在A x 中约束出现的个体变项 2 在第二式中 c为任意个体常项 3 用y或c去取代A x 中的自由出现的x时 一定要在x自由出现的一切地方进行取代 1 全称量词消去规则 简记为UI规则或UI 2 全称量词引入规则 简记为UG规则或UG 该式成立的条件是 1 无论A y 中自由出现的个体变项y取何值 A y 应该均为真 2 取代自由出现的y的x 也不能在A y 中约束出现 3 存在量词引入规则 简记为EG规则或EG 该式成立的条件是 1 c是特定的个体常项 2 取代c的x不能在A c 中出现过 4 存在量词消去规则 简记为EI规则或EI 该式成立的条件是 1 c是使A为真的特定的个体常项 2 c不在A x 中出现 2 A x 中除自由出现的x外 还有其他自由出现的个体变项 此规则不能使用 四 自然推理系统F定义5 3自然推理系统F定义如下 1 字母表 同一阶语言F的字母表 定义4 1 2 合式公式 同F合式公式的定义 定义4 4 3 推理规则 1 前提引入规则 2 结论引入规则 3 置换规则 4 假言推理规则 5 附加规则 6 化简规则 7 拒取式规则 8 假言三段论规则 9 析取三段论规则 10 构造性二难 11 合取引入规则 12 UI规则 13 UG规则 14 EG规则 15 EI规则 五 在自然推理系统F中构造下列推理的证明例证明苏格拉底三段论 人都是要死的 苏格拉底是人 所以苏格拉底是要死的 令F x x是人 G x x是要死的 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 例乌鸦都不是白色的 北京鸭是白色的 因此 北京鸭不是乌鸦 令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 前提引入 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 例前提 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 注意 一定先消存在量词 例前提 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 x G x UG 说明 不能对 xF x xG x 消量词 因为它不是前束范式 对此题不能用附加前提证明法 例前提 x F x G x 结论 xF x xG x 证明 xF x 附加前提引入 F y UI x F x G x 前提引入 F y G y UI G y 假言推理 xG x UG 本题可以使用附加前提证明法 为什么上例不能用 例 如果一个三角形有两条长度相等的边 那么它是一个等腰三角形 如果一个三角形是等腰三角形 那么它有两个度数相同的角 在三角形ABC中没有两个度数相同的角 所以三角形ABC没有两条长度相等的边 论域 三角形的集合 令P t t有两条长度相等的边 Q t t是一个等腰三角形 R t t有两个度数相同的角 c 三角形ABC 前提 t P t Q t t Q t R t R c 结论 P c 证明 t P t Q t 前提引入 P c Q c UI t Q t R t 前提引入 Q c R c UI P c R c 假言三段论 R c 前提引入 P c 拒取式 第五章小结 一 本章的主要内容及要求1 主要内容重要的等值式 在有限个体域内消去量词等值式 量词否定等值式 量词辖域收缩与扩张等值式 量词分配等值式基本规则 置换规则 换名规则 代替规则前束范式与公式的前束范式自然推理系统F 2 要求 深刻理解并记住重要等值式 并能熟练地应用它们熟练地使用置换规则 换名规则 代替规则准确地求出给定公式的前束范式正确地使用UI UG EG EI规则 特别要注意它们之间的关系对给定的推理 正确地构造出它的证明 二 练习1 证明下列各等值式 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 证 1 与 2 略 由 1 与 2 可知 并不是所有的人都喜欢吃馒头 没有不犯错误的人 都可以有两种等值的符号化形式 3 x F x y G y L x y 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 量词辖域扩张 x y F x G y L x y 由 3 可知 火车都比汽车快 等命题可以有不同的符号化形式 2 设个体域D a b c 消去下列公式的量词 1 xF x yG y 2 x y F x G y 3 x F x yG y 解 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 等值 3 先将量词辖域缩小 x F x yG y xF x yG y 量词辖域收缩扩张等值式 F a F b F c G a G b G c 说明 在做此类问题时 若能将量词辖域缩小 就缩小后再消量词 否则太麻烦 3 求下列各公式的前束范式 1 xF x yG x y 2 xF x y xG x y 3 x1F x1 x2 x2G x2 x2H x1 x2 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 辖域收缩扩张等值式 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 4 在自然推理系统F中构造下面推理的证明