离散数学 第六讲.pdf

2006 3 29电子工程学院 离散数学1 2 3 2 基本而重要的等值式 定理 基本而重要的等值式 定理2 1 命题逻辑中的永真式的代换实例均为一阶逻 辑中的永真式 命题逻辑中的永真式的代换实例均为一阶逻 辑中的永真式 置换规则置换规则 24个基本等值式的代换实例是一阶逻辑的永真 式的模式 如 个基本等值式的代换实例是一阶逻辑的永真 式的模式 如 x F x x F x x F x G x x F x G x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学2 定理定理2 2 量词否定等值式 量词否定等值式 1 x A x x A x 2 x A x x A x 证明 不妨设证明 不妨设D a b 1 x A x A a A b A a A b x A x 2 x A x A a A b A a A b x A x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学3 定理定理2 3 量词辖域收缩与扩张的等值式 量词辖域收缩与扩张的等值式 1 x A x B x A x B x A x B x A x B x A x B x A x B x B A x B xA x 证明 证明 x A x B x A x B x A x B x A x B x A x B x B A x x B A x B x A x B xA x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学4 定理定理2 3 量词辖域收缩与扩张的等值式 量词辖域收缩与扩张的等值式 2 x A x B x A x B x A x B x A x B x A x B x A x B x B A x B x A x 证明 证明 x A x B x A x B x A x B x A x B x A x B x B A x x B A x B x A x B x A x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学5 定理定理2 4 量词分配等值式 量词分配等值式 1 x A x B x x A x x B x 2 x A x B x x A x x B x 证明 不妨设证明 不妨设D a b 1 x A x B x A a B a A b B b A a A b B a B b x A x x B x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学6 定理定理2 5 下列等值式成立 下列等值式成立 1 x y A x y y x A x y 2 x y A x y y x A x y 证明 略证明 略 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学7 1 x M x F x x M x F x 2 x F x G x x F x G x 证明 证明 1 x M x F x x M x F x 定理 定理2 2 2 x M x F x 置换规则 置换规则 x M x F x 置换规则 置换规则 2 x F x G x x F x G x 定理 定理2 2 1 x F x G x 置换规则 置换规则 x F x G x 置换规则 置换规则 例例例例2 9 2 9 证明下列各等值式 证明下列各等值式 证明下列各等值式 证明下列各等值式 2006 3 29电子工程学院 离散数学8 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 定理 定理2 2 1 x y F x G y H x y 定理 定理2 2 1 x y F x G y H x y 置换规则 置换规则 x y F x G y H x y 置换规则 置换规则 例例例例2 9 2 9 证明下列各等值式 证明下列各等值式 证明下列各等值式 证明下列各等值式 2006 3 29电子工程学院 离散数学9 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 定理 定理2 2 2 x y F x G y L x y 定理 定理2 2 2 x y F x G y L x y 置换规则 置换规则 x y F x G y L x y 置换规则 置换规则 例例例例2 9 2 9 证明下列各等值式 证明下列各等值式 证明下列各等值式 证明下列各等值式 2006 3 29电子工程学院 离散数学10 2 3 3 前束范式 定义 前束范式 定义2 1 设设A是一公式 若是一公式 若A具有形式具有形式Q1x1Q2x2 QkxkB 则称则称A为前束范式 其中为前束范式 其中Qi为 或 为 或 B为不含量词的公 式 如 为不含量词的公 式 如 x y F x G y H x y 是前束范式 但 是前束范式 但 x F x y G y 不是前束范式 不是前束范式 定理定理2 3 6 前束范式存在定理 前束范式存在定理 一阶逻辑中的任何谓词 公式都存在与之等值的前束范式 注意 虽然前束范式存在 但一般说来并不唯一 如例 一阶逻辑中的任何谓词 公式都存在与之等值的前束范式 注意 虽然前束范式存在 但一般说来并不唯一 如例2 8 没有不犯错误的人没有不犯错误的人 两个等值式均为前束范式 两个等值式均为前束范式 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学11 例例2 9 将求下列各式的前束范式 将求下列各式的前束范式 1 x F x x G x 解 解 1 x F x x G x y F y x G x 换名规则 换名规则 y F y x G x 定理 定理2 3 2 x A x B x A x B y x F y G x 定理 定理2 3 1 x y F y G x 自己验证 自己验证 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学12 例例2 9 将求下列各式的前束范式 将求下列各式的前束范式 2 xF x xG x 解 解 2 xF x xG x yF y xG x 换名规则 换名规则 y F y xG x 定理 定理2 3 2 x A x B x A x B y x F y G x 定理 定理2 3 2 x B A x B x A x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学13 例例2 9 将求下列各式的前束范式 将求下列各式的前束范式 3 xF x x G x 解 解 3 xF x x G x yF y x G x 换名规则 换名规则 y F y x G x 定理 定理2 3 1 x A x B x A x B y x F y G x 定理 定理2 3 1 x B A x B xA x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学14 例例2 9 将求下列各式的前束范式 将求下列各式的前束范式 4 xF x yG y 解 解 4 xF x yG y x F x yG y 定理 定理2 3 2 x A x B x A x B x y F x G y 定理 定理2 3 2 x B A x B x A x 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学15 例例2 9 将求下列各式的前束范式 将求下列各式的前束范式 5 xF x y yG y xH x y 解 解 4 xF x y yG y x H x y xF x z yG y x H x z 代替规则 代替规则 xF x z yG y t H t z 换名规则 换名规则 x F x z yG y t H t z 定理 定理2 3 2 x y F x z G y t H t z 定理 定理2 3 2 x y F x z G y t H t z 定理 定理2 3 1 x y t F x z G y H t z 定理 定理2 3 1 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学16 注意 注意 1 前束范式的不唯一性 前束范式的不唯一性 2 尽管形式上不唯一 但前束范式中指导变项若 为自由出现的个体变项 在原公式中也必为自由出 现的个体变项 尽管形式上不唯一 但前束范式中指导变项若 为自由出现的个体变项 在原公式中也必为自由出 现的个体变项 这一点是不变的 这一点是不变的 2 3 2 3 2 3 2 3 一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式一阶逻辑等值式 2006 3 29电子工程学院 离散数学17 2 4 1 基本概念基本概念 在一阶逻辑中 推理的形式结构仍然为 在一阶逻辑中 推理的形式结构仍然为 A1 A2 An B 在一阶逻辑中判断 在一阶逻辑中判断 是否为永真式远比命题逻辑 中判断蕴涵重言式要困难得多 因此我们着重介绍 在形式系统中构造证明的方法 是否为永真式远比命题逻辑 中判断蕴涵重言式要困难得多 因此我们着重介绍 在形式系统中构造证明的方法 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学18 2 4 2 推理定律 第一组 命题逻辑中推理定律的代换实例 如 推理定律 第一组 命题逻辑中推理定律的代换实例 如 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 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学19 第三组 重要推理定律 如 第三组 重要推理定律 如 1 xA x xB x x A x B x 2 xA x xB x x A x B x 3 x A x B x xA x xB x 4 x A x B x xA x xB x 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学20 为了构造推理系统 还要给出为了构造推理系统 还要给出4条重要的推理规 则 即消去量词和引入量词的规则 条重要的推理规 则 即消去量词和引入量词的规则 1 全称量词消去规则 全称量词消去规则 UI Universal Isolation x A x A y x A x A c 说明 说明 a 中取代 中取代x的的y是任意不在是任意不在A x 中出现的个体变项 中出现的个体变项 b 中的 中的c是一定不在是一定不在A x 中出现的个体常项 中出现的个体常项 c 无论用无论用y或或c代替代替x 一定要在 一定要在x自由出现的一切地方处 处代替 自由出现的一切地方处 处代替 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学21 2 全称量词引入规则 全称量词引入规则 UG Universal Get A y xA x 说明 说明 a y在在A y 中自由出现 且中自由出现 且y取任何值时取任何值时A为真 为真 b 取代取代y的的x不能在不能在A y 中约束出现 否则出错 例 中约束出现 否则出错 例 D为实数集 为实数集 F x y x y 则 则A y x F x y 对 任意的实数 对 任意的实数y均成立均成立 但若将 但若将y用用x代替 得 代替 得 x x F x x 显然这是假命题 显然这是假命题 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学22 3 存在量词引入规则 存在量词引入规则 EG Exist Get A c xA x 说明 说明 a c是特定的个体常项 是特定的个体常项 b 取代取代c的的x不能在不能在A c 中出现 例 中出现 例 D为实数集 为实数集 F x y x y 取 取A y x F x y 即 即 A 2 x F x 2 仍为真命题仍为真命题 但若将 但若将x用用2代替 得 代替 得 x F x x 显然这是假命题 显然这是假命题 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学23 4 存在量词消去规则 存在量词消去规则 EI Exist Isolation xA x A c 说明 说明 a c是使是使A为真的特定的个体常项 为真的特定的个体常项 b 取代取代x的的c不能在不能在A x 中出现 中出现 c 若若A x 中除中除x以外还有其它自由出现的个体变项 不能用 以外还有其它自由出现的个体变项 不能用EI 见如下例 见如下例 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学24 例例2 10 设个体域设个体域D为实数集合 为实数集合 F x y x y 指出 下列推理中的错误 指出 下列推理中的错误 x y F x y 前提引入 前提引入 y F z y UI F z c EI x F x c UG 解 出错 解 出错 原因在于原因在于EI规则中规则中F z y 不能含除不能含除y 以外的其它自由出现的个体变项 以外的其它自由出现的个体变项 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学25 例例2 11 证明苏格拉底三段论 凡是人都是要死的 苏 格拉底是人 所以苏格拉底也是要死的 证明 符号化 证明苏格拉底三段论 凡是人都是要死的 苏 格拉底是人 所以苏格拉底也是要死的 证明 符号化 F x x 是人 是人 G x x 是要死的 是要死的 a 苏格拉底 苏格拉底 D为全总个体域 为全总个体域 前提 前提 x F x G x F a 结论 结论 G a 证明 证明 x F x G x 前提引入 前提引入 F a G a UI F a 前提引入 前提引入 G a 假言推理 假言推理 2 4 2 4 2 4 2 4 一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论一阶谓词的推理理论 2006 3 29电子工程学院 离散数学26 前提 前提 x F x G x H x x F x R x 结论 结论 x F x R x G x 证明 证明 x F x R x 前提引入 前提引入 F c R c EI F c 化简 化简 R c 化简 化简 x F x G x H x 前提引入 前提引入 F c G c H c UI G c H c 假言推理 假言推理 G c 化简 化简 F c R c G c 合取 合取 x F x R x G x EG 例例2 12 构造下面推理的证明 构造下面推理的证明 2006 3 29电子工程学院 离散数学27 前提 前提 x F x G x H x x F x R x 结论 结论 x F x R x G x 证明 证明 x F x G x H x 前提引入 前提引入 F c G c H c UI x F x R x 前提引入 前提引入 F c R c EI 错误 中的错误 中的c未必满足 未必满足 结论 在证明过程中务必先引进带存在量词的前提 结论 在证明过程中务必先引进带存在量词的前提 修改前面的证明步骤 修改前面的证明步骤 2006 3 29电子工程学院 离散数学28 例例2 13 前提 前提 x F x G x x G x H x L x F c H c 结论 结论 L c 证明 证明 注意 在证明过程中先引进带存在量词的前提 注意 在证明过程中先引进带存在量词的前提 F c H c 前提引入 前提引入 F c 化简 化简 H c 化简 化简 x F x G x 前提引入 前提引入 F c G c UI G c 假言推理 假言推理 G c H c 合取 合取 x G x H x L x 前提引入 前提引入 G c H c L c UI L c 假言推理 假言推理 2006 3 29电子工程学院 离散数学29 例例例例2 14 2 14 2 14 2 14 补充例子补充例子补充例子补充例子 D D为全总个体域 为全总个体域 为全总个体域 为全总个体域 如果一个人怕困难 那么他就不会成功 每个人或 者成功或者失败过 有些人未曾失败过 所以有些 人不怕困难 证明 符号化 如果一个人怕困难 那么他就不会成功 每个人或 者成功或者失败过 有些人未曾失败过 所以有些 人不怕困难 证明 符号化 H x x是人 是人 D x x 怕困难怕困难 S x x获得成功 获得成功 F x x是失败过 前提 是失败过 前提 x H x D x S x x H x S x F x x H x F x 结论 结论 x H x D x 2006 3 29电子工程学院 离散数学30 前提 前提 x H x D x S x x H x S x F x x H x F x 结论 结论 x H x D x 证明