在命题演算中，代换定理是基于同态映射:P1→P2，这里P1,P2为二个命题代数，如果P1,P2为谓词代数，则根据同态映射的要求，P1,P2应该有相同的运算集，对其个体符集有新的要求

定义19.17:设P1=P(Y1)和P2=P(Y2)，其个体变元与个体常元分别为X1,C1和 X2,C2，并且或者C1=或者C2。一个半同态映射(,):(P1,X1∪C1)→(P2,X2∪C2)是一对映射: P1→P2; : X1∪C1→X2∪C2，它们联合实现了映射p(x,c)→(p)((x), (c)),且具有性质： (1)(X1)X2，(C1)C2，而且在X1上是一对一的。 (2)是{F,→}-同态映射。 (3)对任何pP1有(xp)=(x)(p)。

引理19.3:设(,):(P1,X1∪C1)→ (P2,X2∪C2)是半同态映射，pP1，并且假设xvar(p)。则(x)var((p))。 (1)x不在p中出现 (2)x在p中约束出现 都要利用在X1上是一对一的

定理19.9(代换定理)设(,):(P1,X1∪C1)→(P2,X2∪C2)是半同态映射，AP1,pP1。 如果A┣p，则(A)┣(p)。 证明:对证明序列用归纳法 n=1,p1=pAP1∪A 对n>1,假设对一切证明序列<n结论成立 pi=pj→pn (i,j <n) pn=xq(A0┣q,A0A,xvar(A0))

§4 前束范式 定义19.18(前束范式):pP(Y)为前束范式，当且仅当它具有下面的形式： p=1x12x2…kxkq,其中i(i=1,…,k)是或，且x1,x2,…xk是不同的，q是P(Y)中不带量词的公式。称1x12x2…kxk为前束，称q为母式。 定义19.19:设pP(Y)，称与p语法等价的前束范式为p的前束范式。

定理19.10:对任何pP(Y)，有前束范式p'满足p┣┫p'。 例:将xR21(x,z)yR22(x,y)变换为前束范式。 定义19.20(斯柯伦范式): pP(Y) 是前束范式 而且它的形式： p=1x12x2…kxkq中的所有全称量词 (如果有的话)总在存在量词(如果有的话)的后面，则称p为斯柯伦(T. Skolem)范式。

§5 谓词演算的性质 谓词逻辑Pred(Y)。 是Y上的关于类型 {F,→,x|xX}的自由代数 赋值 形式证明 赋值解释和证明之间的关系

定理19.11(可靠性定理):设AP(Y),pP(Y)。若A┣p，则有A╞p。 对证明序列长度用归纳法 其他与命题逻辑类似,考虑pn=xq(x) 设q1(x), q2(x),… qk(x)=q(x)是由A的子集导出q的证明序列,其中xvar(A0) 利用量词深度, 设d(pn)=r,引进新变量x'X∪C, 根据赋值概念讨论 由于增加了新变量,必须构造新的谓词代数P(Y') 构造P(Y)到P(Y')的半同态映射 利用代换定理

推论19.1:(协调性定理):F不是Pred(Y)的定理。 引理19.4:设A是P(Y)的协调子集。如果xp(x)A，yvar(A)，且y不在p(x)中出现，则FDed(A∪p(y))。 反证:若FDed(A∪p(y)),设法证明FDed(A) 由演绎定理和G规则得yp(y)Ded(A), 再由约束变元可替换性得xp(x)Ded(A), 利用MP规则可得FDed(A),与A协调矛盾

引理19. 5:设A是P(Y)的协调子集，则存在XX. ,AA. ，这里A. P(Y. )(P(Y. )与 P(Y)的区别是：P(Y 引理19.5:设A是P(Y)的协调子集，则存在XX*,AA*，这里A*P(Y*)(P(Y*)与 P(Y)的区别是：P(Y*)中的项集为X*∪C 上的自由代数)，使得： (i)FDed(A*)，并且 (ii)对所有的pP(Y*)，或者pA*，或者pA*，并且 (iii)如果xp(x)A*，则存在x'X*，使得p(x')A*。 相当与命题逻辑中极大协调的概念 基本步骤是根据公式中的存在量词，添加谓词公式到A*。 引理19.4,引理18.5

定理19.12(可满足性定理)设A是P(Y)的协调子集，则存在P(Y)的解释域U和项解释，使得赋值函数v(A){1}。 不失一般性，假设X,A是满足引理19.5的(i),(ii)和(iii)。现构造解释域如下： 令U=I，1(c)=c， 2(fni)=fn'i，3(Rni)=Rn'i，定义fn'i(t1,…,tn)=(fni, t1,…,tn),并规定：当 Rni(t1,…,tn)A时，(t1,…,tn)Rn'i，否则，(t1,…,tn)Rn'i。又定义变元指派0(x)=x,由此扩张为项解释,这就构成了P(Y)的解释域和项解释。

在此U和下,定义函数v: P(YU,)→Z2如下：当p A时，v(p)=1，否则v(p)=0。下面证明v是满足赋值函数的定义(a)(b)(ck) 定理19.13(完备性定理):设AP(Y),pP(Y), 若A╞p，则A┣p。 (紧致性定理):如果A╞p，则存在A的某个有限子集A0，使得A0╞p。 命题逻辑 Prop(X)的有效性和可证明性是可判定的， 谓词逻辑Pred(Y)的有效性和可证明性则是不具有可判定性的

作业：P257 21(2),22,23,26,27