1、 第四章 命题逻辑的自然演绎系统2022年4月30日星期六2自然演绎系统自然演绎系统NP命题逻辑的自然演绎系统NP是由形式语言形式语言L L 和一组推导（变形）规则构成的。其中形式语言L L 包括初始符号、形成规则和定义。 构建命题逻辑的形式系统，可以采用公理化方法，构建命题逻辑的形式系统，可以采用公理化方法，也可采用自然演绎的方法。为接近人们日常思维的实也可采用自然演绎的方法。为接近人们日常思维的实践，采用自然演绎的方法来构建命题逻辑的一个形式践，采用自然演绎的方法来构建命题逻辑的一个形式系统系统NPNP。2022年4月30日星期六3初始符号初始符号(1)甲类符号：p1, p2, p3, ；
2、(2)乙类符号：，；(3)丙类符号：(，)。这些符号构成的有穷长的序列叫做符号串，例如:p, pq，pq, pq；(pq)r，p(qr)，；(pqpq)，(pqr)， 按照形成规则形成的符号串称为合式公式。2022年4月30日星期六4形成规则形成规则(1)任何单个的命题变元p是合式公式；(2)如果A是合式公式，则(A)是合式公式；(3)如果A和B是合式公式，则(AB)、(AB)、(AB)是合式公式；只有（1）-到（3）形成的符号串是合式公式。2022年4月30日星期六5定义定义定义是用来表示缩写的，定义两边的符号串可以相定义是用来表示缩写的，定义两边的符号串可以相互代替。互代替。如：(AB)=
3、df(AB)(BA)。形式语言L L 的全体合式公式记为Form(L L )。形式语言L L 是我们研究对象，叫对象语言。讨论对象语言的语言叫元语言或语法语言。2022年4月30日星期六6形成规则的作用形成规则的作用（1）以递归的方式定义合式公式。（2）提供一种能行、可判定的方法判定任一符号串是不是合式公式。（3）检验合式公式的性质。如:(pq)(p)q)的形成过程是：p，q，(pq)，(p)，(pq)(p)，q ，(pq)(p)q)。这个字符串是反复运用形成规则而形成的，因此它是合式公式。2022年4月30日星期六7合式公式的子公式合式公式的子公式合式公式的子公式：合式公式的子公式：在生成合
4、式公式的过程中，每一步所生成的公式都是这一生成的合式公式的子公式。如： A的子公式是A和A； AB 的子公式是A、B和AB； AB 的子公式是A、B和AB； AB 的子公式是A、B和AB。如：p，q，（pq），(p)，(pq)(p)，(pq)(p)q)都是(pq)(p)q)的子公式。主联结词：主联结词：辖域最大的联结词。(pq)(p)q)的主联结词是。省略括号的约定：省略括号的约定：(1)公式最外层的括号可以省略。(2)联结词的结合力依下列次序递减：，。如：(pq)(p)q)可简记为(pq)pq。2022年4月30日星期六8推演规则（1）整推规则整推规则（2）置换规则置换规则（3）条件证明规则
5、条件证明规则（4）间接证明规则间接证明规则2022年4月30日星期六9整推规则1.合取引入规则(记为+)： 从A和B推出AB；2.合取消去规则(记为_): 从AB推出A；从AB推出B；3.析取引入规则(记为+)： 从A推出AB；从B推出AB；4.析取消去规则(记为_): 从AB和A推出B；从AB和B推出A；5.肯定前件（记为MP) 从AB和A推出B;6.否定后件规则（记为MT); 从AB和B推出A;2022年4月30日星期六10条件证明规则条件证明规则5.蕴涵引入规则(记为+)： 条件证明 如果从公式集和A推出B，则从推出AB；2022年4月30日星期六11例例1： R（HT） RH TS H
6、 HS R（HT） 前提前提 RH 前提前提 TS 前提前提 H 前提前提 R 否后否后 HT 肯前肯前 HS 假言三段论假言三段论2022年4月30日星期六12例例2：BA B（CD） AC D BA BA 前提前提 B（CD） 前提前提 AC 前提前提 B 化简化简 CD 化简化简 A 肯前肯前 C 否析否析 D 肯前肯前2022年4月30日星期六13例例3：FG（H（IK） HI HMF IK FG（H（IK） 前提前提 HI 前提前提 HMF 前提前提 H 化简化简 HM 附加附加 F 肯前肯前 FG 附加附加 H（IK） 肯前肯前 IK 肯前肯前2022年4月30日星期六14练习：1
7、. M（NL） JK M M（NJ） LK 2022年4月30日星期六15 M（NL） 前提前提 JK 前提前提 M 前提前提 M（NJ） 前提前提 NL 肯前肯前 NJ 否析否析 LK 二难推理二难推理2022年4月30日星期六162. P（RQ） PQ SRQ S R 2022年4月30日星期六17 P（RQ） 前提前提 PQ 前提前提 SRQ 前提前提 S 前提前提 SR 附加附加 Q 肯前肯前 P 否后否后 RQ 肯前肯前 R 否后否后2022年4月30日星期六183. PQ（RS） P （RS）（TU） U T 2022年4月30日星期六19 PQ（RS） 前提前提 P 前提前提 （
8、RS）（TU） 前提前提 U 前提前提 PQ 附加附加 （RS） 肯前肯前 TU 否析否析 T 否后否后2022年4月30日星期六20条件证明规则条件证明规则 步步 骤：骤： 1 1.引入假设引入假设 2.2.撤销假设撤销假设 （适用于蕴含式）（适用于蕴含式）2022年4月30日星期六21蕴涵引入规则(记为+) 又称条件证明规则或演绎定理条件证明规则或演绎定理，是把从推出AB的推理转化为从和临时的假设A推出B的推理。即：（AB）（AB） 本规则实质就是条件输入（输出）规则的运用本规则实质就是条件输入（输出）规则的运用 最适于证明最适于证明结论为蕴涵式结论为蕴涵式的推论。的推论。 前提集前提集结
9、论结论假设前提假设前提2022年4月30日星期六22蕴涵引入规则(记为+)例1：FG HF GH FG 前提前提 HF 前提前提 G 条件假设条件假设 G 双重否定双重否定 F 否析律否析律 F 双重否定双重否定 H 否后律否后律 H 双重否定双重否定 GH 条件证明条件证明2022年4月30日星期六23蕴涵引入规则(记为+)例2：AB CB(DE) A(DE) AB 前提 CB(DE) 前提 A 条件假设 B 肯前律 CB 附加 DE 肯前律 A(DE) 条件证明2022年4月30日星期六24间接证明规则间接证明规则 否定消去规则(记为_)： 间接证明 如果从和A推出BB，则从推出A。 步骤
10、： 1.否定结论 2.提出矛盾 3.肯定结论2022年4月30日星期六25否定消去规则(记为_) 又称间接证明或反证法间接证明或反证法，是把由推出A的推理转化为由和临时的假设A推出BB的推理。 最适于证明最适于证明结论不是蕴涵式结论不是蕴涵式的推论。的推论。2022年4月30日星期六26否定消去规则(记为_)例1：AB AB A(1) AB 前提(2) AB 前提 (3) A 间接假设 (4) A (3)，_ (5) B (1)，(4)，_ (6) B (2)，(4)，_ (7) BB (5)，(6)，+(8) A (3)(7)，间接证明2022年4月30日星期六27否定消去规则(记为_)例2
11、：A(BC)(CD)，CD / A(1) A(BC) (CD) A1(2)CD A2(3) C (2)_ (4) D (2)_ (5) A H1 (6) A (5)_ (7) (BC)(CD) (1)，(6)_ (8) CD (7)_ (9) D (3)，(8)_ (10) DD (4)，(9)+(11)A (5)(10) - - (消去H1) 2022年4月30日星期六28蕴涵引入（条件证明）规则与 否定消去（间接证明）规则在做题过程中二者可以交替使用，既可以先用蕴涵引入（条件证明）规则再用否定消去（间接证明）规则，也可以先用否定消去（间接证明）规则再用蕴涵引入（条件证明）规则。2022年4
12、月30日星期六29练习1 1、XYZ ZX XY 2022年4月30日星期六30 XYZ 前提前提 ZX 前提前提 X 条件假设条件假设 YZ 肯前律肯前律 X 双重否定双重否定 Z 否后率否后率 Y 否析律否析律 XY 条件证明条件证明2022年4月30日星期六31练习：2. E(JK) J(KE) E2022年4月30日星期六32 E(JK) 前提前提 J(KE) 前提前提 E 间接假设间接假设 JK 否析律否析律 J 化简化简 KE 肯前律肯前律 E 化简化简 EE 合取合取 E 间接证明间接证明2022年4月30日星期六33作业：1. XY XZ ZW YW 2. EFG EH IK
13、FJI K 2022年4月30日星期六343. FG HF GH4. E(JK) J(KE) E2022年4月30日星期六35置换规则的涵义置换规则的涵义 对于任何命题P，无论它是以整个命题出现，还是作为一个命题的一部分出现，都可用与它重言等值的命题Q来替换。2022年4月30日星期六36置换规则置换规则T18(a) (AB)A B(记为DeM.)T18(b) (AB)A B(记为DeM.)2022年4月30日星期六37德摩根律的证明德摩根律的证明T18(a) (AB) A B的证明的证明先证(AB) AB:(1) (AB) A (2) (AB) H1 (3) A H2 (4) AB (3)，
14、+ (5)(AB)(AB) (2),(4),+ (6) A (3)(5),_(消去H2) (7) B H3 (8)AB (7)，+ (9)(AB)(AB) (2)，(8)，+ (10) B (7)(9)，_(消去H3) (11)AB (6)，(10), + (12)(AB)(AB) (1)，(11), +(13) AB (2)(12)，_(消去H1)2022年4月30日星期六38德摩根律的证明德摩根律的证明T18(a) (AB) A B的证明的证明再证AB (AB)：(1) AB A (2) (AB) H (3) AB (2)，_ (4) A (3)，_ (5) B (3)，_ (6) A (
15、4)，+(7) B (1),(6),_ (8)BB (5),(7),+(9)(AB) (2)(8),_(消去H)2022年4月30日星期六39置换规则置换规则交换律T21(a) ABBAT21(b) ABBA结合律T22(a) A(BC)(AB)CT22(b) A(BC)(AB)C2022年4月30日星期六40置换规则分配律T23(a) A(BC)(AB)(AC)T23(b) A(BC)(AB)(AC)蕴析律（A A B) (AB)德德 摩摩 根根 律律(AB) (A B)(AB) (AB) 2022年4月30日星期六41置换规则的证明置换规则的证明T21(b) ABBA的证明的证明先证AB
16、BA(1) AB A (2) A H1 (3) BA (2)，+ (4) ABA (2)(3)，+（消去H1） (5) B H2 (6) BA (5)，+(7) BBA (5)(6)，+（消去H2）(8) BA (1)，(4)，(7)，D.C.同理，可证BAAB。2022年4月30日星期六42NP系统中的语法系统中的语法(语形语形)推出关系推出关系T24(a) (B)AB T24(b) AB(AB) T25(a) ABAB (蕴析律)T25(b) ABAT26(a) (AB)AT26(b) A(A)T27(a) A(A)T27(b) A(A)T28(b) AB,AC,BCA(二难推理)T28(
17、c) AC，BD，ABCDT28(d) AC，BD，CDAB2022年4月30日星期六43NP系统中的语法系统中的语法(语形语形)推出关系推出关系T29(a) ABCACB(反三段论)T29(b) ABCBCAT30 ABC A(BC)(条件输出)T31 A(BC) ABC(条件输入)T32 A(BC)B(AC)(条件互易)T33 A(BC)(AB)(AC)（蕴涵分配） T34 A(AB)AB (条件融合)T35(a) AB ACBC (前件附加)T35(b) AB ACBCT35(c) AB (CA)(CB)T36 （AB）C BC 2022年4月30日星期六44NP系统中的语法系统中的语法
18、(语形语形)推出关系推出关系T37 AB，BA AB (+)T38(a) AB AB (_)T38(b) AB BAT39 AC,BC ABC (前件合取) T40 AB,AC ABC (后件合取) T41 ABC(AC)(BC)T42 ABC(AC)(BC)T43 ABC(AB)(AC)T44 ABC(AB)(AC)2022年4月30日星期六45NP系统中的语法系统中的语法(语形语形)推出关系推出关系应用实例应用实例(一一)如果不换8号上场（p）或者12号上场(q)，甲队的形势不会好转(r)。教练没有换8号上场，也没有换12号上场。所以，甲队的形势不会好转。首先，将前提和结论形式化： A1：
19、(pq)r A2：pq B：r(1) (pq)r A1(2) pq A2(3) (pq) (2)，DeM.(4) r (1)，(3)，_2022年4月30日星期六46NP系统中的语法系统中的语法(语形语形)推出关系推出关系应用实例应用实例(二二)如果线段L有存在无穷多个点，那么，如果这些点有长度，则线段L将无穷长，而且，如果这些点都没有长度,则线段L也不会有长度。但是，一条线段既不会无穷长,也不会没有长度。所以L上不会有无穷多个点。前题和结论符号化：A1：p(qr)(qs)A2：rsB：p2022年4月30日星期六47( (1) p(qr)(qs) A1(2) rs A2 (3) p H (4
20、) p (3), _ (5) (qr)(qs) (1)，(4)，_ (6) qr (5),_ (7) qs (5),_ (8) r (2),_ (9) s (2),_ (10) q (6),(8), M.T. (11) q (7),(9), M.T. (12) qq (10),(11),+(13) p (3)(12)，_,(消去H)2022年4月30日星期六48NP系统中的语法系统中的语法(语形语形)推出关系推出关系应用实例应用实例(三三)如果货币供应量保持现状，而货币需求量增加，则银行利率就会上升。如果货币需求量增加导致银行利率上升，则在银行存款更被看好。主管部门已宣布货币供应总是保持不变。
21、因此，在银行存款更被看好。A1：pqrA2：(qr)sA3： pB： s2022年4月30日星期六49NP系统中的语法系统中的语法(语形语形)推出关系推出关系应用实例应用实例(三三)方法一：（1） pqr A1（2）（qr）s A2（3） p A3 (4) q H1 (5) pq (3)，(4)，+ (6) r (1)，(5)，_(7)qr (4)(6)，+(消去H1)(8)s (2)，(7)，_2022年4月30日星期六50NP系统中的语法系统中的语法(语形语形)推出关系推出关系应用实例应用实例(三三)方法二：（1） pqr A1（2）（qr）s A2（3） p A3(4)s H(5)（qr
22、） (2),(4)M.T.(6)qr (5),R.P.(7)r (6)，_(8)(pq) (1),(7)M.T.(9)pq (8),R.P.(10)q (6)，_(11)q (10),+(12)p (9),(11),_(13)pp (3),(12),+(14)s (4)(13),_(消去H)2022年4月30日星期六51证明公式集不一致证明公式集不一致包括逻辑矛盾的公式包括逻辑矛盾的公式(命题命题)集称为不相容集称为不相容(不一致不一致,不协调不协调)的的公式集公式集.判定公式集ABC，CD，AD是否为不一致的公式集.(1)ABC A1(2)CD A2(3)AD A3(4)A (3)，_(5)
23、D (3)，_(6)AB (4)，+(7)C (1)，(6)，_(8)D (2)，(7)，_(9)DD (5)，(8)，+2022年4月30日星期六521. XY XZ ZW YW Z 化简化简 X 否后否后 Y 肯前肯前 W 化简化简 YW 合取合取2022年4月30日星期六532. EFG EH IK FJI K E 化简化简 FG 肯前肯前 F 化简化简 FJ 附加附加 I 肯前肯前 K 否析否析2022年4月30日星期六543. FG HF GH G 条件假设条件假设 G 双否引入双否引入 F 否析律否析律 F 双否引入双否引入 H 否后律否后律 H 双否消去双否消去 GH 条件证明条件证明2022年4月30日星期六554 E(JK) J(KE) E E 间接假设间接假设 JK 否析律否析律 J 化简化简 KE 肯前律肯前律 E 化简化简 EE 合取合取 E 间接证明间接证明
