复旦大学：《离散数学 Discrete Mathematics（下）》英文课件（赵一鸣）29/32

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

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

冷定义21.17:设P1=P(Y1)和P2=P(Y2),其个 体变元与个体常元分别为X1C1和X2C2, 并且或者C=或者C2≠。一个半同态映 射(ax,8):P1X1Uc)→(P2X2UC2)是一对映 射a:P1→>P2;B:X1∪C1X2UC2,它们联 合实现了映射p(x,c)→>(p)(β(x),β(c),且具 有性质: 冷(1)B(XX2,β(CC2,而且β在X上是 一对一的。 冷(2)a是F,→}同态映射 (3对任何p∈P1有a(vxp)=vpa(p)

❖ 定义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)

冷引理21.3:设(a,B):(P1X1Uc1→ (P2X2Uc2)是半同态映射,p∈P1,并且 假设 Xvar(p)。则p(x)var(a(p) 冷证明: XEvar(p) 冷(1)x不在p中出现 冷(2)x在p中约束出现 都要利用在X1上是一对一的

❖ 引 理 2 1 . 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上是一对一的

冷定理219代换定理)设 (aB):(P1×1Uc1)→(P2X2UC2)是半同态 映射,AcP1,p∈P1 今如果AFp,则a(A)a(p)l 证明:对证明序列用归纳法 n=1,p1p∈AP∪A 冷对n>1,假设对一切证明序列<n结论成立 p=p1→pn(<n) "s p=Vxg(Ao lq, AocA, Xevar(Ao)

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

§5前束范式 冷定义2117前束范式:p∈P(Y为前束范式, 当且仅当它具有下面的形式: 冷p=01x102x2…01X1q,其中(i=1,…k)是或彐, 且X1x2,xk是不同的,q是P(Y中不带量词 的公式。称01X102X2…0x为前束,称q为母 式。 冷定义21.17:设p∈P(Y),称与p语法等价的前 束范式为p的前束范式

§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的前束范式

冷定理21:对任何p∈P(Y,有前束范式p 满足pHp' 例将彐xR21(x,Z)yR2(xy)变换为前束 范式。 冷定义2119(斯柯伦范式):p∈P(Y是前束 范式 而且它的形式:p=01x102x2…01x1q中的 所有全称量词(如果有的话)总在存在量 词彐(如果有的话)的后面,则称p为斯柯 伦(T. Skolem)范式

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

§4谓词演算的性质 冷谓词逻辑 Pred(Y)。 冷是Y上的关于类型{F,→,Vxx∈X的自由代数 今赋值 令形式证明 赋值解释和证明之间的关系

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

作业:P42520,21,23,31

❖作业：P425 20,21,23,31

(7)-(pAq)→q 冷证明:即证-(-p-q)→>q 冷由演绎定理即证{(p→-q)-q 令p1=-(7p→7q)=(-p→(q→+F)→F(A) 令p2=(77p→(q→F)→F)→(q→F)→(77p→(q→F) F)(A1) 令p3=(q→F)→(77p→(qF)→F)(p1,p2MP) P4=(q.)F)(-p→(qF)→F)→((4qF)→(7-p (q→F)→(q→F)→F))(A 冷p5=(qF)→(p→(q→F)→(q→F)→F) (p3, p4MP 冷p6=(qF)→(-p→(q→F)(A1) p7=(q→F)→F=77q(p6,p5MP) 冷P8==q→q (A3) 令P9=q (p7, p8MP) 冷可简单,利用-q→(--p→-q)

❖ (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)

p1=q(p-→7q) A1 P2=(q→(-p→q)-(- p→>-q))-q)已证 P3=-(p→-q)77q p1, p2MP 冷P4=-(7p→7q) 冷P5=7=q p4, p3MP P6=7q一q (A3) % P7Eq p5, p6MP

❖ 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