5.1 一阶逻辑等值式与置换规则

null第五章 一阶逻辑等值演算与推理 5.1 一阶逻辑等值式与置换规则第五章 一阶逻辑等值演算与推理 5.1 一阶逻辑等值式与置换规则null 定义5.1（等值式） 设A，B是一阶逻辑中任意两个公式，若AB是永真式，则称A和B是等值的，记作AB，称AB是等值式。 下面给出一阶逻辑中的一些基本而重要的等值式： 由于命题逻辑的重言式的代换实例都是一阶逻辑的永真式，所以命题逻辑中24个等值式模式（p.24）给出的代换实例都是一阶逻辑的等值式模式。例如：xF（x）┐┐xF（x） xy（F（x，y）→G（x，y）） ┐┐xy（F（x，y）→G（x，y）） 等都是A┐┐A的代换实例。null 下面介绍一些一阶逻辑固有的等值式，这些等值式都与量词有关。 1、消去量词等值式 设个体域为有限集D={a1，a2，…，an}，则有 （1）xA（x） A（a1）∧A（a2）∧…∧A（an） （2）xA（x） A（a1）∨A（a2）∨…∨A（an） 2、量词否定等值式 对于任意的公式A（x）： （1）┐xA（x）x┐A（x） （2）┐xA（x）x┐A（x） null 3、量词辖域收缩与扩张等值式 设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）null 4、量词分配等值式 对于任意的公式A（x）和B（x）： （1）x（A（x）∧B（x））xA（x）∧x B（x） （2）x（A（x）∨B（x）） xA（x）∨x B（x） 说明：量词分配等值式中，只有对∧的分配和对∨的分配的等值式。而对∨和对∧无分配律。 null5、同种量词顺序置换等值式 对于任意的公式A（x，y） (1)xyA（x，y） yxA（x，y） (2)xyA（x，y） yxA（x，y）null一阶逻辑的等值演算 一阶逻辑的等值演算中三条重要的规则： 1、置换规则 设ф(A)是含公式A的公式，ф(B)是用公式B置换了ф(A)中所有的A后得到的公式，若AB，则ф(A) ф(B)。null解：（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））例 设个体域为D={a，b，c}，将下面公式的量词消去。 （1）x（F（x）→G（x）） （2）x（F（x）∨yG（y）） （3）xyF（x，y）null（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））null例 给定解释I如下： （a）个体域D={2，3}； （b）D中特定元素a=2 （c）D上特定函数f（x）为：f（2）=3，f（3）=2 （d）D上特定谓词 G（x，y）为：G（2，2）= G（2，3）= G（3，2）=1， G（3，3）=0。 L（x，y）为：L（2，2）= L（3，3）=1， L（2，3）= L（3，2）=0。 F（x）为：F（2）=0，F（3）=1。 在I下求下列各式的真值。 （1）x（ F（x）∧ G（x，a）） （2）x（ F（f（x））∧ G（x，f（x））） （3）x y L（x，y） （4）y x L（x，y）null解： （1）x（F（x）∧G（x，a）） （F（2）∧G（2，a））∧（F（3）∧G（3，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）  1null（3）x y L（x，y） x（L（x，2）∨L（x，3）） （L（2，2）∨L（2，3））∧ （L（3，2）∨L（3，3）） （1∨0）∧（0∨1）  1 （4）y x L（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注意：xyL（x，y）<≠>yx L（x，y） ，说明量词的次序不能随意颠倒。 null例 证明下列各等值式。 （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））null证明： （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）） null（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））  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）） 证明与（3）类似，略 null一阶逻辑的等值演算 一阶逻辑的等值演算中三条重要的规则： 1、置换规则 设ф(A)是含公式A的公式，ф(B)是用公式B置换了ф(A)中所有的A后得到的公式，若AB，则ф(A) ф(B)。 2、换名规则 设A为一公式，将A中某量词辖域中某约束变项的所有出现及相应的指导变元，改成该量词辖域中未曾出现过的某个体变项符号，公式中其余部分不变，设所得公式为A’，则AA’。null解： xF（x，y，z）→yG（x，y，z） sF（s，y，z）→yG（x，y，z）（换名规则） sF（s，y，z）→tG（x，t，z）（换名规则） 例 将下面公式化成与之等值的公式，使其没有既是约束出现的又是自由出现的个体变项。 xF（x，y，z）→yG（x，y，z）null一阶逻辑的等值演算中三条重要的规则： 1、置换规则 设ф(A)是含公式A的公式，ф(B)是用公式B置换了ф(A)中所有的A后得到的公式，若AB，则ф(A) ф(B)。 2、换名规则 设A为一公式，将A中某量词辖域中某约束变项的所有出现及相应的指导变元，改成该量词辖域中未曾出现过的某个体变项符号，公式中其余部分不变，设所得公式为A’，则AA’。 3、代替规则 设A为一公式，将A中某个自由出现的个体变项的所有出现用A中未曾出现过的个体变项符号代替，公式中其余部分不变，设所得公式为A’，则AA’。null解： （1）xF（x，y，z）→yG（x，y，z） sF（s，y，z）→yG（x，y，z）（换名规则） sF（s，y，z）→tG（x，t，z）（换名规则） xF（x，y，z）→yG（x，y，z） xF（x，s，z）→yG（x，y，z）（代替规则） xF（x，s，z）→yG（t，y，z）（代替规则） 例 将下面公式化成与之等值的公式，使其没有既是约束出现的又是自由出现的个体变项。 （1）xF（x，y，z）→yG（x，y，z） （2）x（F（x，y）→yG（x，y，z））null（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 一阶逻辑前束范式 定义5.2（前束范式） 设A为一个一阶逻辑公式，如果A具有如下形式Q1x1Q2x2…QkxkB，则称A为前束范式,Qi（1≤i≤k）为或，B为不含量词的公式。 定义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）∨x G（x） x（F（x）∧y（G（y）→H（x，y））） 等公式都不是前束范式。 注意：前束范式中不存在既是自由出现的，又是约束出现的个体变项。 定理5.1（前束范式存在定理） 一阶逻辑中的任何公式都存在与之等值的前束范式。 定理5.1（前束范式存在定理） 一阶逻辑中的任何公式都存在与之等值的前束范式。 说明： （1）定理说明任何公式的前束范式都是存在的，但并不唯一。 （2）可利用上节的等值式和三条变换规则来求公式的前束范式。null例5.6 求下面公式的前束范式。 （1）x F（x）∧┐x G（x） （2）x F（x）∨┐x G（x） （3）x F（x）→x G（x） （4）x F（x）→x G（x） （5）x F（x，y）→y G（x，y） （6）（x F（x，y）→y G（y））→x H（x，y，z）null （1）x F（x）∧┐x G（x） 方法一：  x F（x）∧x┐G（x）（等值置换）  x（F（x）∧┐G（x）） 方法二：  x F（x）∧┐y G（y）（换名规则）  x F（x）∧y ┐G（y）  x（F（x）∧y┐ G（y））  x y（F（x）∧┐ G（y））null（2）xF（x）∨┐xG（x） xF（x）∨x┐G（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））null（3）xF（x）→xG（x） 方法一：  yF（y）→xG（x）  y(F（y）→xG（x）)  yx(F（y）→G（x）) 方法二： ┐xF（x）∨xG（x） x┐F（x）∨xG（x） x（┐F（x）∨G（x）） 方法三： xy(F（x）→G（y）)null（4）x F（x）→x G（x） 方法一： x F（x）→y G（y） x (F（x）→y G（y）) xy (F（x）→G（y）) 方法二： yx(F（y）→G（x）) 方法三： ┐x F（x）∨ x G（x）  x┐F（x）∨ x G（x）  x┐F（x）∨ y G（y）  xy(┐F（x）∨ G（y）) xy (F（x）→G（y）)null（5）x F（x，y）→y G（x，y） 方法一：  t F（t，y）→s G（x，s）（换名规则）  ts（ F（t，y）→G（x，s）） 方法二： x F（x，y）→y G（x，y）  x F（x，t）→y G（s，y） （代替规则）  xy（F（x，t）→G（s，y））null（6）（x F（x，y）→y G（y））→x H（x，y，z） 方法一： （sF（s，y）→t G（t））→xH（x，y，z） st（F（s，y）→G（t））→xH（x，y，z） stx（（F（s，y）→G（t））→H（x，y，z）） 方法二： （xF（x，t）→y G（y））→sH（s，t，z） xy（F（x，t）→G（y））→sH（s，t，z） xys（（F（x，t）→G（y））→H（s，t，z）） null说明： （1）公式的前束范式一般是不唯一的 （2）原公式中自由出现的个体变项在前束范式中还应是自由出现的。