定义5.1 设A, B是两个谓词公式, 如果AB是永真式, 则称A与B等值, 记作AB, 并称AB是等值式
基本等值式
第一组 命题逻辑中16组基本等值式的代换实例以及推理定律的代换实例
第二组
(1) 消去量词等值式
设D ={a1, a2, … , an}
① x A(x) A(a1)A(a2)…A(an)
② x A(x) A(a1)A(a2)…A(an)
(2) 量词否定等值式
① xA(x) x A(x)
② x A(x) x A(x)
(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(BA(x)) BxA(x)
关于存在量词的:
① x(A(x)B) xA(x)B
② x(A(x)B) xA(x)B
③ x(A(x)B) xA(x)B
④ x(BA(x)) BxA(x)
(4) 量词分配等值式
① x(A(x)B(x)) xA(x)xB(x)
② x(A(x)B(x)) xA(x)xB(x)
注意:对,对无分配律
进行等值演算,还要注意以下规则
1. 置换规则
设(A)是含A的公式, 那么, 若AB, 则(A)(B).
2. 换名规则
设A为一公式,将A中某量词辖域中个体变项的所有约束出现及相应的指导变元换成该量词辖域中未曾出现过的个体变项符号,其余部分不变,设所得公式为A',则A'A.
3. 代替规则
设A为一公式,将A中某个个体变项的所有自由出现用A中未曾出现过的个体变项符号代替,其余部分不变,设所得公式为A',则A'A.
推理的形式结构
1. A1A2Ak B
若次式是永真式, 则称推理正确, 记作A1A2Ak B
2. 前提: A1, A2,, Ak
结论: B
推理定理: 永真式的蕴涵式
推理规则 :
P规则、T规则、CP规则
消去和添加量词的规则:
1)US规则(全称指定规则)
2)UG规则(全称推广规则)
3)ES规则(存在指定规则)
4)EG规则(存在推广规则)
定义5.3 自然推理系统NL 定义如下:
1. 字母表. 同一阶语言L 的字母表
2. 合式公式. 同L 的合式公式
3. 推理规则:
(1) 前提引入规则 P
(2) 结论引入规则 T
(3) 置换规则
(4) 假言推理规则
(5) 附加规则 CP
(6) 化简规则
(7) 拒取式规则
(8) 假言三段论规则
(9) 析取三段论规则
(10) 构造性二难推理规则
(11) 合取引入规则
(12) US规则
(13) UG规则
(14) ES规则
(15) EG规则
- 定义5.2 一个公式,如果量词均在公式的开头且它们的辖域都延伸到整个公式的末尾,则该公式称为前束范式。
- 前束范式的一般形式为Q1x1Q2x2…QnxnA。其中,A是一个没有量词的谓词公式,Qi(1≤i≤n)或为或为,xi是个体变元。
- 没有量词的谓词公式称为平凡的前束范式。
- 定理5.1(前束范式存在定理) 对于任一谓词公式,都存在着与它逻辑等价的前束范式。
-
定义5.4 一个前束范式如果具有如下形式: Q1x1Q2x2…Qnxn((A11∨A12∨…∨A1k1)∧(A21∨A22∨…∨A2k2)∧…(Am1∨Am2∨…∨Amkm))
其中Qi(1≤i≤n)或为或为,xi是个体变元,Aij(1≤j≤km)是原子谓词公式或其否定,则该前束范式称为前束合取范式。
- 例: xzv((﹁P(x)∨﹁R(x, v))∧(﹁Q(y, z)∨﹁R(x, v)))是一个前束合取范式。
- 定理5.2(前束合取范式存在定理) 每一个谓词公式都有与之逻辑等价的前束合取范式。
- 定义5.5 一个前束范式如果具有如下形式: Q1x1Q2x2…Qnxn((A11∧A12∧…∧A1k1)∨(A21∧A22∧…∧A2k2)∨…(Am1∧Am2∧…∧Amkm)),其中Qi(1≤i≤n)或为或为,xi是个体变元,Aij(1≤j≤km)是原子谓词公式或其否定,则该前束范式称为前束析取范式。
- 例: xvz((P(x)∧﹁Q(x,y))∨(P(v)∧Q(y,z)))是一个前束析取范式。
- 定理5.3 每一个谓词公式都有与之逻辑等价的前束析取范式。
- 注意:每个谓词公式都可存在与之逻辑等价的前束范式、前束合取范式和前束析取范式,但并不是唯一的。
-
求前束范式的步骤一般如下:
- 第一步:消去冗余量词,且通过换名或代入规则使不同的个体变元不同名。
- 第二步:利用逻辑等价公式
(AB)(AB)∧(BA)
将公式中的联结词去掉。
-
第三步:利用逻辑等价式
﹁﹁AA
﹁(A∨B)﹁A∧﹁B;﹁(A∧B)﹁A∨﹁B
﹁xP(x)x﹁P(x);﹁xP(x)x﹁P(x)
进行否定深入,将﹁号深入到命题变元和原子谓词公式的前面。
- 第四步:利用量词轄域的扩张与收缩逻辑等价式和量词分配逻辑等价式将所有的量词移到公式的最前面。
四条消去和添加量词特别提示:
(1)当既要使用规则US又要使用规则ES消去公式中的量词,而且选用的个体是同一个符号,则必须先使用规则ES,再使用规则US。然后再使用命题演算中的推理规则,最后使用规则UG或规则EG引入量词,得到所要的结论。
(2)如一个变量是用规则ES消去量词,对该变量在添加量词时,则只能使用规则EG,而不能使用规则UG;如使用规则US消去量词,对该变量在添加量词时,则可使用规则EG和规则UG。
(3)如有两个含有存在量词的公式,当用规则ES消去量词时,不能选用同样的一个常量符号来取代两个公式中的变元,而应用不同的常量符号来取代它们。
(4)在用规则US和规则ES消去量词时,此量词必须位于整个公式的最前端(一般化为前束范式)。
题型
1、由已知的等值式证明新的等值式
2、在有限的个体域内消去公式中的量词
一般先将公式进行简化,即缩小量词辖域,然后再消量词,注意消去量词后可能还会含有自由出现的个体变项。
3、求给定公式的前束范式
注意公式的前束范式不唯一,但是等值的,具体的方法上面已经总结了。
4、在自然推理系统中构造推理的证明
直接法、附加前提法、归谬法(反证法)、注意US、UG、ES、EG规则的正确使用