命题逻辑自然演绎系统课件.ppt

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