(2) 存在推理定理
如果有
△A1，…，△An，△xP(x)，△P(e)├△Q， 其中Q中不含有自由的e，且在推理过程中不对假设中的自由 变元和额外假设中的自由变元实施全规则和存在规则，则有： △A1，△A2，…，△An，△xP(x)├△Q
去“存在 量词”
二、假设推理过程的证明方法
(1) 把待证公式的前件作为假设一一列出，假 设中的全称量词可用全称量词消去规则 消去，存在量词可引入额外假设删除，并 在式子后注明它为额外假设。
假设
(3) P(a)y(D(y)L(a，y)) 额外假设 (4)(P(a)y(D(y)L(a，y))) P(a)
先将（ 1 ）、（ 2 ）化简 (5)(P(a)y(D(y)L(a，y)))y(D(y)L(a,y))
(6) P(a)
(7) y(D(y) L(a，y))
公理8 公理9
例1 (p44) 求证：
x(P(x) Q(x))(xP(x)xQ(x))
解： (1) x(P(x) Q(x)) 假设 (2) x P(x) 假设 (3) P(e) Q(e) 额外假设 (4) P(e) 全称量词消去规则 (5) Q(e) (3)(4)分离 (6) Q(e)x Q(x) 公理21+全称量词消去规则 (7) x Q(x) (6)(5)分离 由存在推理定理得： x(P(x) Q(x))，x P(x)├xQ(x) 由假设推理定理得： x(P(x) Q(x))(xP(x)xQ(x))
xA( x ) A(t )
规则成立的条件： （1）t是任意个体变项或常项。
例 考察∀x∃yF（x，y）全称量词消去能不能得 到下式: ∃y F（y，y）
✘
存在量词消去规则
xA( x ) A(c)
规则成立的条件： （1）c是使A（c）为真的特定的个体常元。 （2）xA（x）是闭式。
例 考察∃yF（x，y）存在量词消去能不能得到下 式: F（x，c）
则已知知识翻译为：
(1) x(P(x)y(D(y)L(x，y))) (2) x(P(x)y(Q(y) L(x，y))) 结论翻译为： x(D(x) Q(x))
(1) x(P(x)y(D(y)L(x，y))) 假设 (2) x(P(x)y(Q(y) L(x，y)))
4.1 谓词演算的永真推理系统 4.2谓词演算的假设推理系统 4.2.1 假设推理系统的组成及证明方法 4.2.2 推理过程的推导过程 4.3谓词演算的归结推理系统
例 求证苏格拉底三段论
凡人要死，苏格拉底是人，所以苏格拉底要死。
解： P(e): e是人 D(e): e要死 a:苏格拉底 (1) x(P(x) D(x)) 假设 (2) P(a) 假设 (3) P(a) D(a) 全称量词消去规则 (4) D(a) (2)(3)分离 由存在推理定理得： x(P(x) Q(x))，P(a)├Q(a) 由假设推理定理得： x(P(x) D(x))(P(a)D(a))
例2 (p44) 已知知识：
(1)有些病人喜欢所有的医生； (2)所有的病人均不喜欢庸医； 试证明结论：所有的医生均不是庸医。
例2 (p44)
证明：先把知识翻译为符号公式,
令P(e)表示“e为病人”； D(e)表示“e为医生”； Q(e)表示“e为庸医”； L(e1，e2)表示“e1喜欢e2”；
例 下面推理是否正确？
设前提为∀x∃yF（x，y）， （1） ∀x∃yF（x，y） （2） ∃yF（t，y） （3） F（t，c） （4） ∀xF（x，c） （5） ∃yxF（x，y）
前பைடு நூலகம்引入 全称量词消去 存在量词消去 全称量词引入 存在量词引入
解： 推理并不正确。 如果给定解释I：个体域为实数集，F(x,y)：x＞y。 则 x∃yF（x，y）为真， ∃y xF（x，y）意为“存在着最小实数”，是假命题 ，故知推理不正确。 之所以出现这样的错误，是在第（3）步中， ∃yF（t，y ）非闭式（含有自由变元t)。
✘
全称量词引入规则
A(t ) xA( x )
规则成立的条件： （1）A（t）在任何解释I及I中对t的任何赋 值下均为真。 （2）x不在A（t）中约束出现。
存在量词引入规则
A(c) xA( x )
规则成立的条件： （1）c是特定的个体常元。 （2）x不在A（c）中出现。
第四章 谓词演算的推理理论
全称量词消去规则(7) 全称量词消去规则(9) 公理14
(13)L(a，b) Q(b)
(12)(11)分离 (14)(D(b) L(a,b))((L(a,b)Q(b))(D(b) Q(b))) 公理3 (15)(L(a，b) Q(b))(D(b) Q(b)) (14)(10)分离 (16)D(b) Q(b) (15)(13)分离 (17)x(D(x) Q(x)) 全0规则(16) 最后，把公式翻译为日常语句得结论：所有的医生均不是庸医。
第四章 谓词演算的推理理论
4.1 谓词演算的永真推理系统 4.2谓词演算的假设推理系统 4.2.1 假设推理系统的组成及证明方法 4.2.2 推理过程的推导过程 4.3谓词演算的归结推理系统
一、假设推理系统的组成
(1) (附加前提证明法) 如果Γ，△A├△B， 则Γ├△(AB)， 也可表示为： 如果△A1，△A2，…，△An，△A├△B， 则△A1，△A2，…，△An├△(AB)。 依次类推可得定理： ├△(A1(A2(…(An(AB)))…)
xA( x ) A(t )
xA( x ) A(c)
二、假设推理过程的证明方法
(2) 按永真的证明方法进行证明，但此时不能对 假设实施代入。 (3) 待证公式的后件中若有全称量词，可用全0 规则引入，存在量词可由公理21引入。
A(t ) xA( x )
A(c) xA( x )
全称量词消去规则
例 下面推理是否正确？
设前提为∀x∃yF（x，y）， （1） ∀x∃yF（x，y） （2） ∃y F（y，y） 解 前提引入 全称量词消去
推理并不正确。 如果给定解释I：个体域为实数集， F（x，y）：x＞y。 则 ∀x∃yF（x，y）意为“对于每个实数x，均存在着 比之更小的实数y”，这是一个真命题。 ∃yF（y，y）意为“存在着比自己小的实数”，是 假命题。 之所以出现这样的错误,是因为∃yF（x，y） 中有1个自 由变元x, 而∃y F（y，y）中无自由变元。
例 所有羊都吃草,所有死羊都不吃草. 所以,所有死羊都不是羊.
解: 推理如下: (1) ∀x(羊(x) →吃草(x)) (2) ∀x(死羊(x) →吃草(x)) (3) 羊(x) →吃草(x) (4) 死羊(x) →吃草(x) (5) (羊(x) →吃草(x)) →(吃草(x)→羊(x)) 定理 (6) 吃草(x)→羊(x) (7) (死羊(x) →吃草(x)) 传递公理 →((吃草(x)→羊(x)) →(死羊(x) →羊(x))) (8) (吃草(x)→羊(x)) →(死羊(x) →羊(x)) (9) 死羊(x) →羊(x) (10) ∀x(死羊(x) →羊(x))
去掉（7）、（9）中全称量词
(4)(3)分离 (5)(3)分离 全称量词消去规则(2) (8)(6)分离
(8) P(a)y(Q(y) L(a，y))
(9) y(Q(y) L(a，y))
(10)D(b) L(a，b)
(11)Q(b) L(a，b)
(12)(Q(b) L(a，b))(L(a，b) Q(b))
第四章 谓词演算的推理理论
4.1 谓词演算的永真推理系统 4.2谓词演算的假设推理系统 4.2.1 假设推理系统的组成及证明方法 4.2.2 推理过程的推导过程 4.3谓词演算的归结推理系统