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

§3谓词演算的形式证明 ■一、形式证明 P(Y)上的一阶谓词演算用Pred(Y)表示 定义2114:称A=A1UA2UA3UA4UA5中的所有元 素为Pred(Y)上的公理集。其中: A1={p→(q→p川|pq∈P(Y)}; A2=(p→(q→r)→(p→q)(p→r)p,q,r∈P(Y} A3={→→p→p|p∈P(Y)} A4={vX(|p→q)→(p→Vxq)|p,q∈P(Y Xgvar(p) A5={vXp(x)p(t)p(x)∈P(Y)项划对p(x)中的x是自由的

§3 谓词演算的形式证明  一、形式证明  P(Y)上的一阶谓词演算用Pred(Y)表示  定义21.14：称A=A1∪A2∪A3∪A4∪A5 中的所有元 素为Pred(Y)上的公理集。其中： A1={p→(q→p)|p,qP(Y)}； A2={(p→(q→r))→((p→q)→(p→r))|p,q,rP(Y)}； A3={p→p|pP(Y)}。 A4={x(p→q)→(p→xq)|p,qP(Y),xvar(p)} A5={xp(x)→p(t)|p(x)P(Y),项t对p(x)中的x是自由的}

除了MP规则外,还要用一个推理规则, 这个规则在以后的论证中常会用到:对 任意的x证明了p(x),则有xp(x)成立。 这个推理规则称为全称推广规如,它使 得在对一般的x证明了p(x)后,可推出 xp(x)。在使用全称推广规则时必须仔 细地陈述限制。全称推广规则也称为G 规则

 除了MP规则外，还要用一个推理规则， 这个规则在以后的论证中常会用到：对 任意的x证明了p(x)，则有xp(x)成立。 这个推理规则称为全称推广规则，它使 得在对一般的x证明了p(x)后，可推出 xp(x)。在使用全称推广规则时必须仔 细地陈述限制。全称推广规则也称为G 规则

定义21.15:设p∈PY),AP(Y),由假设 A寻出的长度为的证明是一组有限序 列p1…,Pn,这里p∈PY)(i=1,,n), pn=p,而p1…,pn1是长度为n1的由A导 出pn的证明序列,并且:对所有k≤n, (1)pk∈AUA,或者 (2)存在(k),有P=(p1→p。或者 (3)pk=Vxw(x),并且P1…,pk的某个子序 列pk,,pk是一个由A的子集 A( XEvar(A导出W(x)的证明长度小于

 定义21.15:设pP(Y)，AP(Y)，由假设 A导出p的长度为n的证明是一组有限序 列 p1 ,…,pn，这里piP(Y)(i=1,…,n)， pn=p，而p1 ,…,pn-1是长度为n-1的由A导 出pn-1的证明序列，并且：对所有kn， (1)pkA∪A，或者 (2)存在i,j(i,j<k)，有pi=(pj→pk )。或者 (3)pk=xw(x)，并且p1 ,…,pk-1的某个子序 列pk1 ,…,pkr 是一个由A的子集 A0 (xvar(A0 ))导出w(x)的证明(长度小于 n)

如果存在一个由A导出p的证明,则记为 AFp,且用DedA)表示满足AFp所有p的全 体。对于D}p,简写为卜p,并称p为 Pred)的定理。 a例3 K-p)lVxp,pePY 根据定义,3X→p就是Vx-p p1=1VX-1-p 假设 p2=VXp→X-p p3=VX-1-p p1, p2 MP p4=yX_→p→-p p5=-m"p p3, P4 MP pe p→→p 3 p7=p 5,p6 MP pa=VXp p7G规则(Xvar({x→P})

 如果存在一个由A导出p的证明，则记为 A┣p，且用Ded(A)表示满足A┣p所有p的全 体 。 对 于 Ø ┣ p， 简写为 ┣ p， 并 称 p 为 Pred(Y)的定理。  例:{xp}┣xp, pP(Y)  根据定义，xp就是xp。  p1=xp 假设  p2=xp→xp A3  p3=xp p1 , p2 MP  p4=xp→p A5  p5=p p3 , p4 MP  p6=p→p A3  p7=p p5 , p6 MP  p8=xp p7 G规则(xvar({xp}))

例:设 yEar(p(x),且p(x)中的自由变元 x不会出现在0y的辖域中。证明: vxp(xvyp(y),这里p(x)∈P(Y

 例: 设yvar(p(x))，且p(x)中的自由变元 x不会出现在y的辖域中。证明： {xp(x)}┣yp(y)，这里p(x)P(Y)

定理21.5:(演绎定理设AcP=P2设 p,q∈P。则AF→q当且仅当AU{p}a 证明:()由AFp→q,证明AU{p}q 存在A导出p→q的有限证明序列 p13…-n=p>q n由MP规则即得 a(2)若AU{p}q 对证明序列长度用归纳法 其他与命题逻辑类似,主要考虑q=vxr(x) 设A是导出r(x)的假设集 (pAO (i)p∈A

 定理21.5:(演绎定理)设AP=P(Y)，设 p,qP。则A┣p→q当且仅当A∪{p}┣q  证明:(1)由A┣p→q,证明A∪{p}┝q  存 在 A 导 出 p→q 的 有 限 证 明 序 列 p1 ,…,pn=p→q，  由MP规则即得.  (2)若A∪{p}┣q  对证明序列长度用归纳法  其他与命题逻辑类似,主要考虑q=xr(x)  设A0是导出r(x)的假设集  (i)pA0  (ii)pA0

■二、等价替换定理与代换定理 m定义21.16:设pq∈PY,若{Pq且 q}Fp,则称p语法等价,记为pHq。 引理212若pHq,则 / Vxd a因为{p}hq由演绎定理知hp→q,同样有 q→p 然后分别证明xp}xq,xq}vxp

 二、等价替换定理与代换定理  定义21.16：设p,qP(Y)，若{p}┣q且 {q}┣p，则称p,q语法等价，记为p┣┫q。  引理21.2:若p┣┫q，则xp┣┫xq  因为{p}┣q,由演绎定理知┣ p→q,同样有  ┣ q→p  然后分别证明{xp}┣xq, {xq}┣xp

定理21.6(等价替换定理:设pp1p2∈P(Y),p1 Hp2,现在p中将p的某些(不一定所有)出现替 换为p2而得到的结果记为p,则pHp 证明:对p在PY)中的层次用归纳法 al=0则p是原子公式或p=F 因此p=p1当用p1替换为p2而得到p, 则pHp2得pHp,成立 ■对l>0假设对一切l<k结论成立, 对k除p=p1这种平凡情况外, ■分以下几种情况 (1)p=(q→r) (2)p=VXd

 定理21.6(等价替换定理):设p,p1 ,p2P(Y)，p1 ┣┫p2，现在p中将p1的某些(不一定所有)出现替 换为p2而得到的结果记为p'，则p┣┫p'。  证明:对p在P(Y)中的层次l用归纳法  l=0,则p是原子公式或p=F,  因此p=p1 ,当用p1替换为p2而得到p',  则p1┣┫p2得p┣┫p',成立  对l >0,假设对一切l <k结论成立,  对l=k,除p=p1这种平凡情况外,  分以下几种情况  (1)p=(q→r)  (2)p=xq

定理217(约束变元符可替换性):设在p中 将θxq(x)的某些(不一定所有)出现替换为 eyq(y)而得到p"(这里 ye var(q(x),且 p(x)中的自由变元x不会出现在θy的辖域 中),则pHp 定理218:在PY)中有 (1)p→q→pvq (2)p>(pvq)(pv-a); (3)p4>q(p~q(→p入q) (4)→pHp;

 定理21.7(约束变元符可替换性):设在p中 将xq(x)的某些(不一定所有)出现替换为  yq(y)而得到p'(这里yvar(q(x))，且 p(x)中的自由变元x不会出现在y的辖域 中)，则p┣┫p'。  定理21.8:在P(Y)中有：  (1)p→q┣┫pq；  (2)pq┣┫(pq)(pq)；  (3)pq┣┫(pq)(pq)；  (4)p┣┫p；

(5)-xp(x)Hex-p(x),这里我们约定:用v 和彐分别表示和v; (6)pA0xq(x)Hex(pAq(x)), xevar(p (7pvexq(x)Hex(pva(x)), xEvar(p (8)Vxp(x)AVx(x)HVx(p(x)aq(x)) (93xp(x)v3Xq(x)H=x(p(x)vq(x)) (10)01xp(x)入2yq(y)H6xe2y(p(x)入qy), Xgvar(qly),y gvar(p(x)); (11)01 xp(x)ve2yq(y)H 81x02y(p(xvq(y) Xgvar(q)),y g var(p(x))

(5)xp(x)┣┫'xp(x)，这里我们约定：用' 和'分别表示和； (6)pxq(x)┣┫x(pq(x))，xvar(p)； (7)pxq(x)┣┫x(pq(x))，xvar(p) ； (8)xp(x)xq(x)┣┫x(p(x)q(x))； (9)xp(x)xq(x)┣┫x(p(x)q(x))； (10)1xp(x)2yq(y)┣┫1x2y(p(x)q(y))， xvar(q(y)),yvar(p(x))； (11)1xp(x)2yq(y)┣┫1x2y(p(x)q(y))， xvar(q(y)),yvar(p(x))