定义21.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),

Presentation on theme: "定义21.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),"— Presentation transcript:

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

2 定义21.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)。

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

4 定理21.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))

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

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

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

8 作业：P ,21,23,31

9 (7) |-(pq) →q 证明:即证|-¬(¬¬p→¬q)→q 由演绎定理即证{¬(¬¬p→¬q)}|-q p1= ¬(¬ ¬ p → ¬q)=(¬ ¬ p →(q→F)) →F (A) p2= ((¬ ¬ p →(q→F)) →F) →((q→F) →((¬ ¬ p →(q→F)) →F)) (A1) p3= (q→F) →((¬ ¬ p →(q→F)) →F) (p1,p2MP) P4=((q→F) →((¬ ¬ p →(q→F)) →F)) →((((q→F) → (¬ ¬ p →(q→F)))→((q→F) →F))) (A2) p5= ((q→F) → (¬ ¬ p →(q→F)))→((q→F) →F) (p3,p4MP) p6= (q→F) → (¬ ¬ p →(q→F)) (A1) p7= (q→F) →F= ¬ ¬ q (p6,p5MP) P8= ¬ ¬q →q (A3) P9=q (p7,p8MP) 可简单，利用 ¬q → (¬ ¬ p → ¬q)

10 p1=¬q→(¬ ¬ p→¬q) A1. P2=(¬q→(¬ ¬ p→¬q))→(¬(¬ ¬p→¬q)→¬ ¬q) 已证 P3=¬(¬¬p→¬q)→¬ ¬q p1,p2MP P4=¬(¬ ¬ p→¬q) A P5=¬ ¬q p4,p3MP P6= ¬ ¬q →q (A3) P7=q p5,p6MP

11 P ,2,6,7,8