一阶逻辑等值演算与推理5．1一阶逻辑等值式与置换规则

《一阶逻辑等值演算与推理5．1一阶逻辑等值式与置换规则》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、一阶逻辑等值演算与推理5．1一阶逻辑等值式与置换规则等值式定义：设A，B是一阶逻辑中任意两个公式，若AB是永真式，则称A与B是等值的，记作AB。称AB为等值式。说明：同命题逻辑一样，人们事先证明了一些重要的等值式，通过它们可推演出更多等值式。21.命题逻辑中等值式的推广命题逻辑中的16组等值式及其代换实例都是一阶逻辑中的等值式。xP(x)xP(x)xP(x)(xP(x)xQ(x))xP(x)xQ(x)x(P(x)Q(x))yR(y)?32.消去量词等值式设个体域为

2、有限集D={a1,a2,…,an}，则有xP(x)xP(x)P(a1)P(a2)…P(an)P(a1)P(a2)…P(an)43.量词否定等值式xP(x)xP(x)xP(x)xP(x)在有限个体域上公式的验证：字面上理解。54.量词辖域收缩与扩张等值式设A(x)是任意的含变量x的公式，B中不含x的出现，则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)B64.量词辖域收

3、缩与扩张等值式2.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)B75.量词分配等值式设A(x),B(x)是含x的任意公式，则x(A(x)B(x))xA(x)xB(x)x(A(x)B(x))xA(x)xB(x)两个重言蕴涵式：xA(x)xB(x)x(A(x)B(x))x(A(x)B(x))xA(x)xB(x)86.多量词等值式多量词相连，同名量词无序，异名量词

4、有序。xyQ(x,y)yxQ(x,y)xyQ(x,y)yxQ(x,y)9等值演算的三条规则置换规则设X是合式公式A的子公式，若XY，如果将A中的X用Y来置换，得到的公式B与公式A等值，即AB。如，x(P(x)Q(x))yR(y)10等值演算的三条规则2.换名规则设A为一公式，将A中某量词的指导变量，及其辖域中该变量的所有约束出现，更改为量词辖域中没有出现过的个体变量符号，最好是公式中未出现过的符号。公式中其余部分不变。设所得公式为A’，则A’A。x(P(x,y)yQ(x

5、,y,z))S(x,z)如:x(P(x)D(x))y(P(y)D(y))u(P(u,y)vQ(u,v,z))S(x,z)11等值演算的三条规则xP(x,x1,x2,…,xn)yP(y,x1,x2,…,xn)xP(x,x1,x2,…,xn)yP(y,x1,x2,…,xn)其中y{x1,x2,…,xn}12等值演算的三条规则3.代替规则设A为一公式，将A中某自由出现的个体变量的所有出现，更改为A中没有出现过的个体变量符号，公式中其余部分不变。设所得公式为A’，则A’A。x(

6、P(x,y)yQ(x,y,z))S(x,z)如，P(x)P(y)x(P(x,v)yQ(x,y,w))S(u,w)13等值演算的三条规则例，使下面公式中每个个体变量只有一种形式的出现。x(P(x,y)yQ(x,y,z))S(x,z)x(P(x,y)yQ(x,y,z))S(x,z)u(P(u,y)yQ(u,y,z))S(x,z)u(P(u,y)vQ(u,v,z))S(x,z)x(P(x,u)yQ(x,y,z))S(x,z)x(P(x,u)yQ

7、(x,y,z))S(v,z)14例设个体域D={a,b,c}，消去公式中的量词。xy((F(x)G(y))xyF(x,y)x(F(x,y)yG(y))15例给定解释I如下：DI={2,3}；DI中特定元素a=2;函数f(x)：f(2)=3，f(3)=2；谓词F(x)：F(2)=0，F(3)=1;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.16在I下求下列各式的真值。1)x(F(x

8、)G(x,a))2)x(F(f(x))G(x,f(x)))(F(2)G(2,2))(F(3)G(3,2))(01)(11)0(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)1173)xyL(x,y)4)yxL(x,y)x(L(x,2)L(x