第五章-一阶逻辑等值演算与PPT课件

.,1,第五章一阶逻辑等值演算与推理,本章的主要内容一阶逻辑等值式与基本的等值式置换规则、换名规则、代替规则前束范式一阶逻辑推理理论本章与其他各章的关系本章的先行基础是前四章本章是集合论各章的先行基础,.,2,5.1一阶逻辑等值式与置换规则,一、等值式与基本的等值式,1等值式（定义5.1）AB当且仅当AB为永真式（A与B为任意的一阶逻辑公式）注意：与定义2.1的区别与联系,2基本的等值式第一组：命题逻辑中16组基本等值式代换实例,例如，xF(x)yG(y)xF(x)yG(y),pqpq的代换实例,.,3,第二组：本章新给出（1）消去量词等值式D=a1,a2,anxA(x)A(a1)A(a2)A(an)xA(x)A(a1)A(a2)A(an)（2）量词否定等值式xA(x)xA(x)xA(x)xA(x),.,4,（3）量词辖域收缩与扩张等值式.A(x)是含x自由出现的公式，B中不含x的出现,关于存在量词的：x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x)BxA(x),关于全称量词的：x(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(A(x)B)xA(x)Bx(BA(x)BxA(x),.,5,（4）量词分配等值式x(A(x)B(x)xA(x)xB(x)x(A(x)B(x)xA(x)xB(x),注意：对无分配律，对无分配律,.,6,二、置换规则、换名及代替规则1置换规则（同命题逻辑）,2换名规则设A为一公式，将A中某量词辖域中约束变项的所有出现及相应的指导变元，改成该量词辖域中未曾出现过的某个体变项符号，公式中其余部分不变，设所得公式为A，则AA.,3.代替规则设A为一公式，将A中某个自由出现的个体变项的所有出现用A中未曾出现过的某个体变项符号代替，A中其余部分不变，设所得公式为A，则AA.,.,7,例将下面命题用两种形式符号化（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),.,8,5.2一阶逻辑前束范式,一、前束范式与命题公式的前束范式1前束范式：定义5.2设A为一个一阶逻辑公式，若A具有形式Q1x1Q2x2QkxkB则称A为前束范式，其中Qi(1ik)为或，B为不含量词的公式.,x(F(x)y(G(y)H(x,y)xy(F(x)(G(y)H(x,y)x(F(x)G(x)x(F(x)G(x),不是,是,不是,是,.,9,2.公式的前束范式定理5.1（前束范式存在定理）一阶逻辑中的任何公式都存在与之等值的前束范式（不惟一）,3.如何求公式的前束范式利用重要等值式、置换规则、换名规则、代替规则进行等值演算,.,10,例求下列公式的前束范式（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)两步结果都是前束范式，说明不惟一性.,.,11,（2）xF(x)xG(x)xF(x)xG(x)（量词否定等值式）x(F(x)G(x)（量词分配等值式）另有一种形式xF(x)xG(x)xF(x)xG(x)xF(x)yG(y)xy(F(x)G(y)两种形式等值吗？,（3）xF(x)xG(x)xF(x)xG(x)x(F(x)G(x)（为什么？）或xy(F(x)G(y)（为什么？）,.,12,（4）xF(x)y(G(x,y)H(y)zF(z)y(G(x,y)H(y)（换名规则）zy(F(z)(G(x,y)H(y)（为什么？）或xF(x)y(G(z,y)H(y)（代替规则）xy(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)xy(F(x,u)G(x,y)H(x,z),注意：x与y不能颠倒,.,13,5.3一阶逻辑的推理理论,一、推理的形式结构以及推理正确与错误1形式结构：A1A2AkB（*）其中，A1，A2，Ak，B为一阶逻辑公式.若（*）为永真式，则推理正确.,2判断方法判（*）是否为永真式很难.本章主要介绍在形式系统F中构造证明，采用的形式结构为前提：A1，A2，Ak结论：B,.,14,二、重要的推理定律,如xF(x)yG(y)xF(x)为化简律代换实例,第二组由上节基本等值式生成，,如由xA(x)xA(x)生成xA(x)xA(x)与xA(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),注意：反向蕴涵式不成立,.,15,三、量词消去或引入规则,两式成立的条件是：（1）在第一式中，取代x的y应为任意的不在A(x)中约束出现的个体变项.（2）在第二式中，c为任意个体常项.（3）用y或c去取代A(x)中的自由出现的x时，一定要在x自由出现的一切地方进行取代.,1全称量词消去规则（简记为UI规则或UI）,.,16,2全称量词引入规则（简记为UG规则或UG）,该式成立的条件是：（1）无论A(y)中自由出现的个体变项y取何值，A(y)应该均为真.（2）取代自由出现的y的x，也不能在A(y)中约束出现.,.,17,3存在量词引入规则（简记为EG规则或EG）,该式成立的条件是：（1）c是特定的个体常项.（2）取代c的x不能在A(c)中出现过.,.,18,4存在量词消去规则（简记为EI规则或EI）,该式成立的条件是：（1）c是使A为真的特定的个体常项.（2）c不在A(x)中出现.（2）A(x)中除自由出现的x外，还有其他自由出现的个体变项，此规则不能使用.,.,19,四、自然推理系统F定义5.3自然推理系统F定义如下：1字母表，同一阶语言F的字母表（定义4.1）2合式公式，同F合式公式的定义（定义4.4）3推理规则：（1）前提引入规则（2）结论引入规则（3）置换规则（4）假言推理规则,.,20,（5）附加规则（6）化简规则（7）拒取式规则（8）假言三段论规则（9）析取三段论规则（10）构造性二难,（11）合取引入规则（12）UI规则（13）UG规则（14）EG规则（15）EI规则,.,21,五.在自然推理系统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)UIG(a)假言推理,注意：使用UI时，用a取代x,.,22,例乌鸦都不是白色的.北京鸭是白色的.因此，北京鸭不是乌鸦.,令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)UIx(G(x)H(x)前提引入G(y)H(y)UIH(y)G(y)置换F(y)G(y)假言三段论G(y)F(y)置换x(G(x)F(x)UG,.,23,例前提：x(F(x)G(x)，xF(x)结论：xG(x),证明：xF(x)前提引入x(F(x)G(x)前提引入F(c)EIF(c)G(c)UIG(c)假言推理xG(x)EG,注意：一定先消存在量词！,.,24,例前提：xF(x)xG(x)结论：x(F(x)G(x),证明：xF(x)xG(x)前提引入xy(F(x)G(y)置换x(F(x)G(z)UIF(z)G(z)UIx(F(x)G(x)UG,说明：不能对xF(x)xG(x)消量词，因为它不是前束范式。对此题不能用附加前提证明法,.,25,例前提：x(F(x)G(x)结论：xF(x)xG(x),证明：xF(x)附加前提引入F(y)UIx(F(x)G(x)前提引入F(y)G(y)UIG(y)假言推理xG(x)UG,本题可以使用附加前提证明法,为什么上例不能用?,.,26,第五章小结,一、本章的主要内容及要求1主要内容重要的等值式在有限个体域内消去量词等值式量词否定等值式量词辖域收缩与扩张等值式量词分配等值式基本规则置换规则换名规则代替规则前束范式与公式的前束范式自然推理系统F,.,27,2要求,深刻理解并记住重要等值式，并能熟练地应用它们熟练地使用置换规则、换名规则、代替规则准确地求出给定公式的前束范式正确地使用UI,UG,EG,EI规则，特别要注意它们之间的关系对给定的推理，正确地构造出它的证明,.,28,二、练习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)xy(F(x)G(y)L(x,y),.,29,证:(1)与(2)略；由（1）与（2）可知，“并不是所有的人都喜欢吃馒头.”,“没有不犯错误的人”，都可以有两种等值的符号化形式.（3）x(F(x)y(G(y)L(x,y)x(F(x)y(G(y)L(x,y)xy(F(x)(G(y)L(x,y)xy(F(x)(G(y)L(x,y)（量词辖域扩张）xy(F(x)G(y)L(x,y)由（3）可知，“火车都比汽车快”等命题可以有不同的符号化形式.,.,30,2.设个体域D=a,b,c，消去下列公式的量词（1）xF(x)yG(y)（2）xy(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）先将量词辖域缩小，再消量词方便xy(F(x)G(y)xF(x)yG(y)（量词辖域收缩扩张等值式）(F(a)F(b)F(c)(G(a)G(b)G(c)（1）与（2）等值,.,31,（3）先将量词辖域缩小x(F(x)yG(y)xF(x)yG(y)（量词辖域收缩扩张等值式）(F(a)F(b)F(c)(G(a)G(b)G(c),说明：在做此类问题时，若能将量词辖域缩小，就缩小后再消量词，否则太麻烦.,.,32,3求下列各公式的前束范式（1）xF(x)yG(x,y)（2）xF(x,y)xG(x,y)（3）(x1F(x1,x2)x2G(x2)x2H(x1,x2),.,33,（1）xF(x)yG(x,y)xF(x)yG(x,y)（量词否定等值式）xF(x)yG(z,y)（代替规则）xy(F(x)G(z,y)（辖域收缩扩张等值式）（2）xF(x,y)xG(x,y)xF(x,y)zG(z,y)（换名规则）xz(F(x,y)G(z,y),求前束范式时，要用换名规则、代替规则、量词否定等值式、量词辖域收缩与扩张等值式.,.,34,（3）(x1F(x1,x2)x2G(x2)x2H(x1,x2)(x1F(x1,x2)x3G(x3)x4H(x5,x4)x1x3(F(x1,x2)G(x3)x4H(x5,x4)x1x3x4(F(x1,x2)G(x3)H(x5,x4),.,35,4在自然推理系统F中构造下面推理的证明.每个喜欢步行的人都不喜欢骑自行车.每个人或者是喜欢骑自行车或者喜欢乘汽车.有的人不喜欢乘汽车.所以，有人