§4谓词演算的性质 冷谓词逻辑 Pred(Y)。 冷是Y上的关于类型{F,→,Vxx∈X的自由代数 今赋值 令形式证明 赋值解释和证明之间的关系
§4 谓词演算的性质 ❖ 谓词逻辑Pred(Y)。 ❖ 是Y上的关于类型 {F,→,x|xX}的自由代数 ❖ 赋值 ❖ 形式证明 ❖ 赋值解释和证明之间的关系
定理21.8(可靠性定理):设AcP(Y)peP(Y 若AFp,则有AF 对证明序列长度用归纳法 冷其他与命题逻辑类似考虑pn=Vxq(x) 设q1(x),q2(x),…q(x)=q(x)是由A的子集导 出q的证明序列其中 XEvar(A0) 利用量词深度, 冷设d(Pn)=r引进新变量x'XUC, 根据赋值概念讨论 由于增加了新变量,必须构造新的谓词代数 P(Y") 冷构造P(Y到P(Y)的半同态映射 今利用代换定理
❖ 定理21.8(可靠性定理):设AP(Y),pP(Y)。 若A┣p，则有A╞p。 ❖ 对证明序列长度用归纳法 ❖ 其他与命题逻辑类似,考虑pn =xq(x) ❖ 设q1 (x), q2 (x),… qk (x)=q(x)是由A的子集导 出q的证明序列,其中xvar(A0 ) ❖ 利用量词深度, ❖ 设d(pn )=r,引进新变量x'X∪C, ❖ 根据赋值概念讨论 ❖ 由于增加了新变量,必须构造新的谓词代数 P(Y') ❖ 构造P(Y)到P(Y')的半同态映射 ❖ 利用代换定理
冷推论211:(协调性定理)F不是 Pred(Y的定理。 冷引理214设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协调矛盾
❖ 推论21.1:(协调性定理):F不是Pred(Y)的定理。 ❖ 引理21.4:设A是P(Y)的协调子集。如果 xp(x)A，yvar(A)，且y不在p(x)中出现， 则FDed(A∪p(y))。 ❖ 反证:若FDed(A∪p(y)),设法证明FDed(A) ❖ 由演绎定理和G规则得yp(y)Ded(A), ❖ 再由约束变元可替换性得xp(x)Ded(A), ❖ 利用MP规则可得FDed(A),与A协调矛盾
引理21.5:设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。 引理214引理205
❖ 引理 21.5:设 A是 P(Y)的协调子集，则存在 XX* ,AA* ，这里A* P(Y* )(P(Y* )与 P(Y)的区 别是：P(Y* )中的项集为X*∪C 上的自由代数)， 使得： ❖ (i)FDed(A* )，并且 ❖ (ii)对所有的pP(Y* )，或者pA* ，或者pA* ， 并且 ❖ (iii) 如 果 xp(x)A* ， 则存在 x'X* ， 使 得 p(x')A* 。 ❖ 相当与命题逻辑中极大协调的概念 ❖ 基本步骤是根据公式中的存在量词，添加谓词 公式到A* 。 ❖ 引理21.4,引理20.5
定理21,9(可满足性定理)设A是P(Y的协 调子集,则存在P(Y)的解释域U和项解释 使得赋值函数vA)≤{1}。 不失一般性,假设X,A是满足引理21.5的 i)(i)和(i)。现构造解释域如下 YU=I, (c)=c, 2(ifm i, (3(R,)=R,i 定义fu(t1…,t)=(fn,t1…,t,并规定:当 Rn(t1…,t)∈A时,(t1,tn)∈Rn",否则, (t1…,t)gRn"。又定义变元指派p(x)=x 由此扩张为项解释这就构成了P(Y)的解 释域和项解释
❖ 定理21.9(可满足性定理)设A是P(Y)的协 调子集，则存在P(Y)的解释域U和项解释 ，使得赋值函数v(A){1}。 ❖ 不失一般性，假设X,A是满足引理21.5的 (i),(ii)和(iii)。现构造解释域如下： ❖ 令U=I，1 (c)=c， 2 (fn i )=fn ' i ，3 (Rn i )=Rn ' i ， 定义fn ' i (t1 ,…,tn )=(fn i , t1 ,…,tn ),并规定：当 ❖ Rn i (t1 ,…,tn )A时，(t1 ,…,tn )Rn ' i ，否则， (t1 ,…,tn )Rn ' i 。又定义变元指派0 (x)=x, 由此扩张为项解释,这就构成了P(Y)的解 释域和项解释
冷在此U和φ下定义函数v:P(Y9)→Z2如下: 当p∈A时,v(p)=1,否则v(p)=0。下面证 明v是满足赋值函数的定义(a)(b)(c)
❖ 在此U和下,定义函数v: P(YU,)→Z2如下： 当p A时，v(p)=1，否则v(p)=0。下面证 明v是满足赋值函数的定义(a)(b)(ck)