《§3谓词演算的形式证明》由会员分享，可在线阅读，更多相关《§3谓词演算的形式证明（12页珍藏版）》请在金锄头文库上搜索。
1、3 谓词演算的形式证明,一、形式证明 P(Y)上的一阶谓词演算用Pred(Y)表示 定义21.14：称A=A1A2A3A4A5 中的所有元素为Pred(Y)上的公理集。其中： A1=p(qp)|p,qP(Y)； A2=(p(qr)(pq)(pr)|p,q,rP(Y)； A3=pp|pP(Y)。 A4=x(pq)(pxq)|p,qP(Y),xvar(p) A5=xp(x)p(t)|p(x)P(Y),项t对p(x)中的x是自由的,除了MP规则外，还要用一个推理规则，这个规则在以后的论证中常会用到：对任意的x证明了p(x)，则有xp(x)成立。这个推理规则称为全称推广规则，它使得在对一般的x证明了p
2、(x)后，可推出xp(x)。在使用全称推广规则时必须仔细地陈述限制。全称推广规则也称为G规则。,定义21.15:设pP(Y)，AP(Y)，由假设A导出p的长度为n的证明是一组有限序列 p1,pn，这里piP(Y)(i=1,n)，pn=p，而p1,pn-1是长度为n-1的由A导出pn-1的证明序列，并且：对所有kn， (1)pkAA，或者 (2)存在i,j(i,jk)，有pi=(pjpk)。或者 (3)pk=xw(x)，并且p1,pk-1的某个子序列pk1,pkr是一个由A的子集A0(xvar(A0)导出w(x)的证明(长度小于n)。,如果存在一个由A导出p的证明，则记为Ap，且用Ded(A)表
3、示满足Ap所有p的全体。对于p，简写为p，并称p为 Pred(Y)的定理。 例:xpxp, pP(Y) 根据定义，xp就是xp。 p1=xp 假设 p2=xpxp A3 p3=xp p1, p2 MP p4=xpp A5 p5=p p3, p4 MP p6=pp A3 p7=p p5, p6 MP p8=xp p7 G规则(xvar(xp),例: 设yvar(p(x)，且p(x)中的自由变元x不会出现在y的辖域中。证明：xp(x)yp(y)，这里p(x)P(Y).,定理21.5:(演绎定理)设AP=P(Y)，设p,qP。则Apq当且仅当Apq 证明:(1)由Apq,证明Apq 存在A导出pq的
4、有限证明序列 p1,pn=pq， 由MP规则即得. (2)若Apq 对证明序列长度用归纳法 其他与命题逻辑类似,主要考虑q=xr(x) 设A0是导出r(x)的假设集 (i)pA0 (ii)pA0,二、等价替换定理与代换定理 定义21.16：设p,qP(Y)，若pq且qp，则称p,q语法等价，记为pq。 引理21.2:若pq，则xpxq 因为pq,由演绎定理知 pq,同样有 qp 然后分别证明xpxq, xqxp,定理21.6(等价替换定理):设p,p1,p2P(Y)，p1 p2，现在p中将p1的某些(不一定所有)出现替换为p2而得到的结果记为p，则pp。 证明:对p在P(Y)中的层次l用归纳法
5、 l=0,则p是原子公式或p=F, 因此p=p1,当用p1替换为p2而得到p, 则p1p2得pp,成立 对l 0,假设对一切l k结论成立, 对l=k,除p=p1这种平凡情况外, 分以下几种情况 (1)p=(qr) (2)p=xq,定理21.7(约束变元符可替换性):设在p中将xq(x)的某些(不一定所有)出现替换为yq(y)而得到p(这里yvar(q(x)，且p(x)中的自由变元x不会出现在y的辖域中)，则pp。 定理21.8:在P(Y)中有： (1)pqpq； (2)pq(pq)(pq)； (3)pq(pq)(pq)； (4)pp；,(5)xp(x)xp(x)，这里我们约定：用和分别表示和
6、； (6)pxq(x)x(pq(x)，xvar(p)； (7)pxq(x)x(pq(x)，xvar(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)1x2y(p(x)q(y)，xvar(q(y),yvar(p(x)； (11)1xp(x)2yq(y)1x2y(p(x)q(y)，xvar(q(y),yvar(p(x)。,在命题演算中，代换定理是基于同态映射:P1P2，这里P1,P2为二个命题代数，如果P1,P2为谓词代数，则根据同态映射的要求，P1,P2应该有相同的运算集，对其个体符集有新的要求,作业:P423 18,19(1),
