复旦大学：《离散数学——代数结构与数理逻辑》PPT课件_28/29

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

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

冷定义1917:设P=P(Y和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)x是,小}同态映射。 (3对任何p∈P1有a(vxp)=vpa(p)

❖ 定义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:设(a,B):(P1X1UC1→ (P2X2Uc2)是半同态映射,p∈P1,并且 假设 Xvar(p)。则p(x)var(a(p) 冷证明: XEvar(p) 冷(1)x不在p中出现 冷(2)x在p中约束出现 都要利用在X1上是一对一的

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

冷定理199代换定理)设 (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)

❖ 定理19.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 ))

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

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

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

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

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

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

氵定理11(可靠性定理:设AcP(①p∈P①Y 若AFp,则有AF 对证明序列长度用归纳法 冷其他与命题逻辑类似考虑pn=Vxq(x) 设q1(x),q2(x),…q(x)=q(x)是由A的子集导 出q的证明序列其中 XEvar(A0) 利用量词深度, 冷设d(pn)=r,引进新变量x'gX∪C, 根据赋值概念讨论 由于增加了新变量,必须构造新的谓词代数 P(Y") 冷构造P(Y到P(Y)的半同态映射 今利用代换定理

❖ 定理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')的半同态映射 ❖ 利用代换定理

冷推论191:(协调性定理)F不是 Pred(Y的定理。 冷引理194设A是P(Y的协调子集。如果 日xp(x)∈A, svar((A,且y不在p(x)中出现, 则 FADed(AUp(y) 冷反证:若F∈ Ded(AUp(y),设法证明F∈Ded(A) 冷由演绎定理和G规则得y_p(y)eDed(A), 冷再由约束变元可替换性得xp(x)∈Ded(A) 冷利用MP规则可得F∈Ded(A),与A协调矛盾

❖ 推论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协调矛盾

引理195:设A是PY)的协调子集,则存在 XcX,AcA,这里AP(Y)P(Y)与P(Y的区 别是:P(Y)中的项集为XUC上的自由代数) 使得: 冷() FEDed(A),并且 冷(i)对所有的p∈P(Y),或者p∈A,或者p∈A 并且 冷(i)如果彐xp(x)∈A,则存在x∈X,使得 p(x)∈A。 相当与命题逻辑中极大协调的概念 冷基本步骤是根据公式中的存在量词,添加谓词 公式到A。 引理194,引理185

❖ 引理 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