Download presentation
Presentation is loading. Please wait.
1
§4 谓词演算的性质 谓词逻辑Pred(Y)。 是Y上的关于类型 {F,→,x|xX}的自由代数 赋值 形式证明
赋值解释和证明之间的关系
2
定理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')的半同态映射 利用代换定理
3
推论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协调矛盾
4
引理21. 5:设A是P(Y)的协调子集，则存在XX. ,AA. ，这里A. P(Y. )(P(Y. )与 P(Y)的区别是：P(Y
引理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
5
定理21.9(可满足性定理)设A是P(Y)的协调子集，则存在P(Y)的解释域U和项解释，使得赋值函数v(A){1}。
不失一般性，假设X,A是满足引理21.5的(i),(ii)和(iii)。现构造解释域如下： 令U=I，1(c)=c， 2(fni)=fn'i，3(Rni)=Rn'i，定义fn'i(t1,…,tn)=(fni, t1,…,tn),并规定：当 Rni(t1,…,tn)A时，(t1,…,tn)Rn'i，否则，(t1,…,tn)Rn'i。又定义变元指派0(x)=x,由此扩张为项解释,这就构成了P(Y)的解释域和项解释。
6
在此U和下,定义函数v: P(YU,)→Z2如下：当p A时，v(p)=1，否则v(p)=0。下面证明v是满足赋值函数的定义(a)(b)(ck)
Similar presentations
