在命题演算中,代换定理是基于同态映 射φ: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)对任何pP1有(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 )是半同态映射，pP1，并且 假设xvar(p)。则(x)var((p))。 ❖ 证明:xvar(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 )是半同态 映射，AP1 ,pP1。 ❖ 如果A┣p，则(A)┣(p)。 ❖ 证明:对证明序列用归纳法 ❖ n=1,p1=pA P1∪A ❖ 对n>1,假设对一切证明序列<n结论成立 ❖ pi=pj→pn (i,j <n) ❖ pn =xq(A0┣q,A0A,xvar(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(前束范式):pP(Y)为前束范式， 当且仅当它具有下面的形式： ❖ p=1x12x2…kxkq,其中i (i=1,…,k)是或， 且x1 ,x2 ,…xk是不同的，q是P(Y)中不带量词 的公式。称1x12x2…kxk为前束，称q为母 式。 ❖ 定义19.19:设pP(Y)，称与p语法等价的前 束范式为p的前束范式