1、3 谓词演算的形式证明谓词演算的形式证明一、形式证明一、形式证明P(Y)上的一阶谓词演算用上的一阶谓词演算用Pred(Y)表示表示定义定义21.14：称：称A=A1A2A3A4A5 中的所有元中的所有元素为素为Pred(Y)上的公理集。其中：上的公理集。其中：A1=p(qp)|p,q P(Y)；A2=(p(qr)(pq)(pr)|p,q,r P(Y)；A3=pp|p P(Y)。A4=x(pq)(p xq)|p,q P(Y),x var(p)A5=xp(x)p(t)|p(x)P(Y),项项t对对p(x)中的中的x是自由的是自由的除了除了MP规则规则外，还要用一个推理规则，外，还要用一个推理规则，
2、这个规则在以后的论证中常会用到：对这个规则在以后的论证中常会用到：对任意的任意的x证明了证明了p(x)，则有则有 xp(x)成立。成立。这个推理规则称为这个推理规则称为全称推广规则全称推广规则，它使，它使得在对一般的得在对一般的x证明了证明了p(x)后，可推出后，可推出 xp(x)。在使用全称推广规则时必须仔在使用全称推广规则时必须仔细地陈述限制。全称推广规则也称为细地陈述限制。全称推广规则也称为G规则规则。定义定义21.15:设设p P(Y)，A P(Y)，由假设由假设A导出导出p的长度为的长度为n的证明的证明是一组有限序是一组有限序列列 p1,pn，这里这里pi P(Y)(i=1,n)，p
3、n=p，而而p1,pn-1是长度为是长度为n-1的由的由A导导出出pn-1的证明序列，并且：对所有的证明序列，并且：对所有k n，(1)pk AA，或者或者(2)存在存在i,j(i,j0,假设对一切假设对一切l k结论成立结论成立,对对l=k,除除p=p1这种平凡情况外这种平凡情况外,分以下几种情况分以下几种情况(1)p=(qrr)(2)p=xq定理定理21.7(约束变元符可替换性约束变元符可替换性):设在设在p中中将将 xq(x)的某些的某些(不一定所有不一定所有)出现替换为出现替换为 yq(y)而得到而得到p(这里这里y var(q(x)，且，且p(x)中的自由变元中的自由变元x不会出现在
4、不会出现在 y的辖域的辖域中中)，则，则pp。定理定理21.8:在在P(Y)中有：中有：(1)pq p q；(2)pq(p q)(pq)；(3)pq(p q)(pq)；(4)pp；(5)xp(x)x p(x)，这里我们约定：用这里我们约定：用 和和 分别表示分别表示 和和；(6)pxq(x)x(p q(x)，x var(p)；(7)pxq(x)x(p q(x)，x var(p)；(8)xp(x)xq(x)x(p(x)q(x)；(9)xp(x)xq(x)x(p(x)q(x)；(10)1xp(x)2yq(y)1x 2y(p(x)q(y)，x var(q(y),y var(p(x)；(11)1xp(x)2yq(y)1x 2y(p(x)q(y)，x var(q(y),y var(p(x)。在命题演算中，代换定理是基于同态映在命题演算中，代换定理是基于同态映射射:P1P2，这里这里P1,P2为二个命题代数，为二个命题代数，如果如果P1,P2为谓词代数，则根据同态映射为谓词代数，则根据同态映射的要求，的要求，P1,P2应该有相同的运算集，对应该有相同的运算集，对其个体符集有新的要求其个体符集有新的要求作业作业:P423 18,19(1)
