3谓词演算的形式证明.pptx

3 谓词演算的形式证明谓词演算的形式证明一、形式证明一、形式证明P(Y)上的一阶谓词演算用上的一阶谓词演算用Pred(Y)表示表示定义定义21.14：称：称A=A1 A2 A3 A4 A5 中的所有元素中的所有元素为为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规则规则外，还要用一个推理规则，外，还要用一个推理规则，这个规则在以后的论证中常会用到：对这个规则在以后的论证中常会用到：对任意的任意的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)，pn=p，而而p1,pn-1是长度为是长度为n-1的由的由A导导出出pn-1的证明序列，并且：对所有的证明序列，并且：对所有k n，(1)pk A A，或者或者(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不不会会出出现现在在 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)