4谓词演算的性质.pptVIP

在命题演算中，代换定理是基于同态映射?: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))。 证明: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 对n1,假设对一切证明序列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*)中的项集为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)=fni，?3(Rni)=Rni，定义fni(t1,…,tn)=(fni, t1,…,tn),并规定：当 Rni(t1,…,tn)?A时，(t1,…,tn)?Rni，否则，(t1,…,tn)?Rni。又定义变元指派?0(x)=x,由此扩张为项解释,这就构成了P(Y)的解释域和项解释。 在此U和?下,定义函数v: