1
2.3 一阶逻辑等值式
?等值式
?基本等值式
?量词否定等值式
?量词辖域收缩与扩张等值式
?量词分配等值式
?前束范式
2
等值式与基本等值式
基本等值式,
命题逻辑中 16组基本等值式的代换实例
如,?xF(x)??yG(y) ? ??xF(x)??yG(y)
?(?xF(x)??yG(y)) ? ??xF(x)???yG(y) 等
消去量词等值式 设 D={a1,a2,…,an}
?xA(x)?A(a1)?A(a2)?… ?A(an)
?xA(x)?A(a1)?A(a2)?… ?A(an)
定义 若 A?B为逻辑有效式,则称 A与 B是 等值 的,
记作 A?B,并称 A?B为 等值式,
3
基本等值式 (续 )
量词辖域收缩与扩张等值式
设 A(x)是含 x自由出现的公式, B中不含 x的出现
关于全称量词的,
?x(A(x)?B)??xA(x)?B
?x(A(x)?B)??xA(x)?B
?x(A(x)?B)??xA(x)?B
?x(B?A(x))?B??xA(x)
关于存在量词的,
?x(A(x)?B)??xA(x)?B
?x(A(x)?B)??xA(x)?B
?x(A(x)?B)??xA(x)?B
?x(B?A(x))?B??xA(x)
4
基本的等值式 (续 )
量词分配等值式
?x(A(x)?B(x))??xA(x)??xB(x)
?x(A(x)?B(x))??xA(x)??xB(x)
注意,?对 ?无分配律,?对 ?无分配律
5
基本的等值式 (续 )
例 将下面命题用两种形式符号化
(1) 没有不犯错误的人
(2) 不是所有的人都爱看电影
解 (1) 令 F(x),x是人, G(x),x犯错误,
??x(F(x)??G(x))
??x(F(x)?G(x))
请给出演算过程, 并说明理由,
(2) 令 F(x),x是人, G(x):爱看电影,
??x(F(x)?G(x))
??x(F(x)??G(x))
给出演算过程,并说明理由,
6
前束范式
例如, ?x?y(F(x)?(G(y)?H(x,y)))
?x?(F(x)?G(x))
是前束范式,而
?x(F(x)??y(G(y)?H(x,y)))
??x(F(x)?G(x))
不是前束范式,
定义 设 A为一个一阶逻辑公式,若 A具有如下形式
Q1x1Q2x2… QkxkB,则称 A为 前束范式,其中 Qi (1?i?k)
为 ?或 ?,B为不含量词的公式,
7
公式的前束范式
定理 ( 前束范式存在定理 ) 一阶逻辑中的任何公
式都存在与之等值的前束范式
注意,
公式的前束范式不惟一
求公式的前束范式的方法, 利用重要等值式,
置换规则, 换名规则, 代替规则进行等值演算,
8
换名规则与代替规则
换名规则, 将量词辖域中出现的某个约束出现的
个体变项及对应的指导变项, 改成另一个辖域中未
曾出现过的个体变项符号, 公式中其余部分不变,
则所得公式与原来的公式等值,
代替规则, 对某自由出现的个体变项用与原公式
中所有个体变项符号不同的符号去代替,则所得公
式与原来的公式等值,
9
公式的前束范式 (续 )
例 求下列公式的前束范式
(1) ??x(M(x)?F(x))
解 ??x(M(x)?F(x))
? ?x(?M(x)??F(x)) ( 量词否定等值式 )
? ?x(M(x)??F(x))
两步结果都是前束范式, 说明前束范式不惟一,
10
例 (续 )
(2) ?xF(x)???xG(x)
解 ?xF(x)???xG(x)
??xF(x)??x?G(x) ( 量词否定等值式 )
??x(F(x)??G(x)) ( 量词分配等值式 )
另有一种形式
?xF(x)???xG(x)
??xF(x)??x?G(x)
??xF(x)??y?G(y) ( 代替规则 )
??x?y(F(x)??G(y)) ( 量词辖域扩张 )
两种形式是等值的
11
例 (续 )
(3) ?xF(x)???xG(x)
解 ?xF(x)???xG(x)
??xF(x)??x?G(x)
??x(F(x)??G(x)) ( 为什么? )
或 ??x?y(F(x)??G(y)) ( 为什么? )
(4) ?xF(x)??y(G(x,y)??H(y))
解 ?xF(x)??y(G(x,y)??H(y))
??zF(z)??y(G(x,y)??H(y)) ( 换名规则 )
??z?y(F(z)?(G(x,y)??H(y))) ( 为什么? )
12
例 (续 )

??xF(x)??y(G(z,y)??H(y)) ( 代替规则 )
??x?y(F(x)?(G(z,y)??H(y)))
(5) ?x(F(x,y)??y(G(x,y)?H(x,z)))
解 用换名规则,也可用代替规则,这里用代替规则
?x(F(x,y)??y(G(x,y)?H(x,z)))
??x(F(x,u)??y(G(x,y)?H(x,z)))
??x?y(F(x,u)?G(x,y)?H(x,z)))
注意,?x与 ?y不能颠倒
13
2.4 一阶逻辑推理理论
?推理的形式结构
?判断推理是否正确的方法
?重要的推理定律
?推理规则
?构造证明
?附加前提证明法
14
推理
推理的形式结构 有两种,
第一种 A1?A2?… ?Ak?B (*)
第二种 前提,A1,A2,…, Ak
结论,B
其中 A1,A2,…,Ak,B为一阶逻辑公式,
若 (*)为永真式,则称 推理正确,否则称 推理不正确,
判断方法,
真值表法,等值演算法,主析取范式法及构造证
明法, 前 3种方法采用第一种形式结构,构造证明
法采用第二种形式结构,
15
重要的推理定律
第一组 命题逻辑推理定律代换实例
如 ?xF(x)??yG(y)??xF(x)为化简律代换实例,
第二组 由基本等值式生成
如 由 ??xA(x)??x?A(x) 生成
??xA(x)??x?A(x),?x?A(x)???xA(x),…
第三组
?xA(x)??xB(x)??x(A(x)?B(x))
?x(A(x)?B(x))??xA(x)??xB(x)
16
推理规则
(1)前提引入规则 (2)结论引入规则
(3)置换规则 (4)假言推理规则
(5)附加规则 (6)化简规则
(7)拒取式规则 (8)假言三段论规则
(9)析取三段论规则 (10)构造性二难推理规则
(11)合取引入规则
17
推理规则 (续 )
(12) 全称量词消去规则 ( 简记为 UI规则或 UI)
两式成立的条件是,
在第一式中, 取代 x的 y应为任意的不在 A(x)中
约束出现的个体变项,
在第二式中, c为任意个体常项,
用 y或 c去取代 A(x)中的自由出现的 x时, 一定要
在 x自由出现的一切地方进行取代,
)(
)(
)(
)(
cA
xxA
yA
xxA
?
?
?
?

18
推理规则 (续 )
(13) 全称量词引入规则 ( 简记为 UG规则或 UG)
该式成立的条件是,
无论 A(y)中自由出现的个体变项 y取何值, A(y)
应该均为真,
取代自由出现的 y的 x,也不能在 A(y)中约束出
现,
)(
)(
xxA
yA
??
19
推理规则 (续 )
(14) 存在量词引入规则 ( 简记为 EG规则或 EG)
该式成立的条件是,
c是使 A为真的特定个体常项,
取代 c的 x不能在 A(c)中出现过,
)(
)(
xxA
cA
??
20
推理规则 (续 )
(15) 存在量词消去规则 ( 简记为 EI规则或 EI)
该式成立的条件是,
c是使 A为真的特定的个体常项,
c不在 A(x)中出现,
若 A(x)中除自由出现的 x外, 还有其他自由出现
的个体变项, 此规则不能使用,
)(
)(
cA
xxA
?
?
21
构造推理证明
例 1 证明苏格拉底三段论,,人都是要死的,苏格拉
底是人, 所以苏格拉底是要死的,”
令 F(x),x是人,G(x),x是要死的,a,苏格拉底
前提,?x(F(x)?G(x)),F(a)
结论,G(a)
证明,① F(a) 前提引入
② ?x(F(x)?G(x)) 前提引入
③ F(a)?G(a) ② UI
④ G(a) ①③ 假言推理
注意:使用 UI时,用 a取代 x,
22
构造推理证明 (续 )
例 2 乌鸦都不是白色的, 北京鸭是白色的, 因此,
北京鸭不是乌鸦,
令 F(x),x是乌鸦,G(x),x是北京鸭,
H(x),x是白色的
前提,?x(F(x)??H(x)),?x(G(x)?H(x))
结论,?x(G(x)??F(x))
23
例 2(续 )
证明,
① ?x(F(x)??H(x)) 前提引入
② F(y)??H(y) ① UI
③ ?x(G(x)?H(x)) 前提引入
④ G(y)?H(y) ③ UI
⑤ ?H(y)??G(y) ④ 置换
⑥ F(y)??G(y) ②⑤ 假言三段论
⑦ G(y)??F(y) ⑥ 置换
⑧ ?x(G(x)??F(x)) ⑦ UG
24
构造推理证明 (续 )
例 3 构造下述推理证明
前提,?x(F(x)?G(x)),?xF(x)
结论,?xG(x)
证明,① ?xF(x) 前提引入
② ?x(F(x)?G(x)) 前提引入
③ F(c) ① EI
④ F(c)?G(c) ② UI
⑤ G(c) ③④ 假言推理
⑥ ?xG(x) ⑤ EG
注意:必须先消存在量词
25
构造推理证明 (续 )
例 4 构造下述推理证明
前提,?xF(x)??xG(x)
结论,?x(F(x)?G(x))
证明,① ?xF(x)??xG(x) 前提引入
② ?x?y(F(x)?G(y)) ① 置换
③ ?x(F(x)?G(z)) ② UI
④ F(z)?G(z) ③ UI
⑤ ?x(F(x)?G(x)) ④ UG
说明,
不能对 ?xF(x)??xG(x)消量词,因为它不是前束范式,
对此题不能用附加前提证明法,
26
构造推理证明 (续 )
例 5 构造下述推理证明
前提,?x(F(x)?G(x))
结论,?xF(x)??xG(x)
证明,① ?xF(x) 附加前提引入
② F(y) ① UI
③ ?x(F(x)?G(x)) 前提引入
④ F(y)?G(y) ③ UI
⑤ G(y) ②④ 假言推理
⑥ ?xG(x) ⑤ UG
本题可以使用附加前提证明法