第四章命题逻辑的自然演绎系统

第四章命题逻辑的自然演绎系统2020年2月18日星期二2自然演绎系统NP命题逻辑的自然演绎系统NP是由形式语言L′和一组推导（变形）规则构成的。其中形式语言L′包括初始符号、形成规则和定义。构建命题逻辑的形式系统，可以采用公理化方法，也可采用自然演绎的方法。为接近人们日常思维的实践，采用自然演绎的方法来构建命题逻辑的一个形式系统NP。2020年2月18日星期二3初始符号(1)甲类符号：p1,p2,p3,…(2)乙类符号：，∧，∨，→；(3)丙类符号：(，)。这些符号构成的有穷长的序列叫做符号串，例如:p,p∧q，p∨q,p→q(p∧q)→r，p∧(q→r)，…((p→∨q→pq)，(((p→q∧r)∨)，…按照形成规则形成的符号串称为合式公式。2020年2月18日星期二4形成规则(1)任何单个的命题变元p是合式公式；(2)如果A是合式公式，则(A)是合式公式；(3)如果A和B是合式公式，则(A∧B)、(A∨B)、(A→B)是合式公式；只有（1）----到（3）形成的符号串是合式公式。2020年2月18日星期二5定义定义是用来表示缩写的，定义两边的符号串可以相互代替。如：(AB)=df(A→B)∧(B→A)。形式语言L′的全体合式公式记为Form(L′)。形式语言L′是我们研究对象，叫对象语言。讨论对象语言的语言叫元语言或语法语言。2020年2月18日星期二6形成规则的作用（1）以递归的方式定义合式公式。（2）提供一种能行、可判定的方法判定任一符号串是不是合式公式。（3）检验合式公式的性质。如:(((p∨q)∧(p))→q)的形成过程是：p，q，(p∨q)，(p)，((p∨q)∧(p))，q，(((p∨q)∧(p))→q)。这个字符串是反复运用形成规则而形成的，因此它是合式公式。2020年2月18日星期二7合式公式的子公式合式公式的子公式：在生成合式公式的过程中，每一步所生成的公式都是这一生成的合式公式的子公式。如：A的子公式是A和A；A∧B的子公式是A、B和A∧B；A∨B的子公式是A、B和A∨B；A→B的子公式是A、B和A→B。如：p，q，（p∨q），(p)，((p∨q)∧(p))，(((p∨q)∧(p))→q)都是(((p∨q)∧(p))→q)的子公式。主联结词：辖域最大的联结词。(((p∨q)∧(p))→q)的主联结词是→。省略括号的约定：(1)公式最外层的括号可以省略。(2)联结词的结合力依下列次序递减：，∧，∨，→，。如：(((p∨q)∧(p))→q)可简记为(p∨q)∧p→q。2020年2月18日星期二8推演规则（1）整推规则（2）置换规则（3）条件证明规则（4）间接证明规则2020年2月18日星期二9整推规则1.合取引入规则(记为∧+)：从A和B推出A∧B；2.合取消去规则(记为∧_):从A∧B推出A；从A∧B推出B；3.析取引入规则(记为∨+)：从A推出A∨B；从B推出A∨B；4.析取消去规则(记为∨_):从A∨B和A推出B；从A∨B和B推出A；5.肯定前件（记为MP)从A→B和A推出B;6.否定后件规则（记为MT);从A→B和B推出A;2020年2月18日星期二10条件证明规则5.蕴涵引入规则(记为→+)：条件证明如果从公式集Γ和A推出B，则从Γ推出A→B；2020年2月18日星期二11例1：┐R→（H→T）R→HT→S┐H∴H→S⑴┐R→（H→T）前提⑵R→H前提⑶T→S前提⑷┐H前提⑸┐R⑵⑷否后⑹H→T⑴⑸肯前⑺H→S⑶⑹假言三段论2020年2月18日星期二12例2：B→┐AB∧（C→D）A∨C∴D⑴B→┐A⑴B→┐A前提⑵B∧（C→D）前提⑶A∨C前提⑷B⑵化简⑸C→D⑵化简⑹┐A⑴⑷肯前⑺C⑶⑹否析⑻D⑸⑺肯前2020年2月18日星期二13例3：F∨G→（H→（I↔K））H∧IH∨M→F∴I↔K⑴F∨G→（H→（I↔K））前提⑵H∧I前提⑶H∨M→F前提⑷H⑵化简⑸H∨M⑷附加⑹F⑶⑸肯前⑺F∨G⑹附加⑻H→（I↔K）⑴⑺肯前⑼I↔K⑷⑻肯前2020年2月18日星期二14练习：1.┐M→（N→L）J→K┐MM∨（N∨J）∴L∨K2020年2月18日星期二15⑴┐M→（N→L）前提⑵J→K前提⑶┐M前提⑷M∨（N∨J）前提⑸N→L⑴⑶肯前⑹N∨J⑶⑷否析⑺L∨K⑵⑸⑹二难推理2020年2月18日星期二162.┐P→（R→┐Q）P→┐Q┐S∨┐R→┐┐Q┐S∴┐R2020年2月18日星期二17⑴┐P→（R→┐Q）前提⑵P→┐Q前提⑶┐S∨┐R→┐┐Q前提⑷┐S前提⑸┐S∨┐R⑷附加⑹┐┐Q⑶⑸肯前⑺┐P⑵⑹否后⑻R→┐Q⑴⑺肯前⑼┐R⑹⑻否后2020年2月18日星期二183.┐P∨┐Q→┐（R→S）┐P（R→S）∨（T→U）┐U∴┐T2020年2月18日星期二19⑴┐P∨┐Q→┐（R→S）前提⑵┐P前提⑶（R→S）∨（T→U）前提⑷┐U前提⑸┐P∨┐Q⑵附加⑹┐（R→S）⑴⑸肯前⑺T→U⑶⑹否析⑻┐T⑷⑺否后2020年2月18日星期二20条件证明规则步骤：1.引入假设2.撤销假设（适用于蕴含式）2020年2月18日星期二21蕴涵引入规则(记为→+)又称条件证明规则或演绎定理，是把从Γ推出A→B的推理转化为从Γ和临时的假设A推出B的推理。即：（Γ→（A→B））←→（Γ∧A→B）本规则实质就是条件输入（输出）规则的运用最适于证明结论为蕴涵式的推论。前提集结论假设前提2020年2月18日星期二22蕴涵引入规则(记为→+)例1：F∨┐G┐H→┐F∴G→H⑴F∨┐G前提⑵┐H→┐F前提⑶G条件假设⑷┐┐G⑴双重否定⑸F⑴⑷否析律⑹┐┐F⑸双重否定⑺┐┐H⑵⑹否后律⑻H⑺双重否定⑼G→H⑶─⑻条件证明2020年2月18日星期二23蕴涵引入规则(记为→+)例2：A→B┐C∨B→(D→E)∴A→(D→E)⑴A→B前提⑵┐C∨B→(D→E)前提⑶A条件假设⑷B⑴⑶肯前律⑸┐C∨B⑷附加⑹D→E⑵⑸肯前律⑺A→(D→E)⑶─⑹条件证明2020年2月18日星期二24间接证明规则否定消去规则(记为_)：间接证明如果从Γ和A推出B∧B，则从Γ推出A。步骤：1.否定结论2.提出矛盾3.肯定结论2020年2月18日星期二25否定消去规则(记为_)又称间接证明或反证法，是把由Γ推出A的推理转化为由Γ和临时的假设A推出B∧B的推理。最适于证明结论不是蕴涵式的推论。2020年2月18日星期二26否定消去规则(记为_)例1：A→BA→B∴A(1)A→B前提(2)A→B前提(3)A间接假设(4)A(3)，_(5)B(1)，(4)，→_(6)B(2)，(4)，→_(7)B∧B(5)，(6)，∧+(8)A(3)—(7)，间接证明2020年2月18日星期二27否定消去规则(记为_)例2：A→(B→C)∧(¬C→D)，¬C∧¬D/∴¬A(1)A→(B→C)∧(¬C→D)A1(2)¬C∧¬DA2(3)¬C(2)∧_(4)¬D(2)∧_(5)¬¬AH1(6)A(5)_(7)(B→C)∧(¬C→D)(1)，(6)→_(8)¬C→D(7)∧_(9)D(3)，(8)→_(10)¬D∧D(4)，(9)∧+(11)¬A(5)—(10)-(消去H1)2020年2月18日星期二28蕴涵引入（条件证明）规则与否定消去（间接证明）规则在做题过程中二者可以交替使用，既可以先用蕴涵引入（条件证明）规则再用否定消去（间接证明）规则，也可以先用否定消去（间接证明）规则再用蕴涵引入（条件证明）规则。2020年2月18日星期二29练习1、X→Y∨ZZ→┐X∴X→Y2020年2月18日星期二30⑴X→Y∨Z前提⑵Z→┐X前提⑶X条件假设⑷Y∨Z⑴⑶肯前律⑸┐┐X⑶双重否定⑹┐Z⑵⑸否后率⑺Y⑷⑹否析律⑻X→Y⑶─⑺条件证明2020年2月18日星期二31练习：2.E∨(J∧┐K)J→(┐K∧E)∴E2020年2月18日星期二32⑴E∨(J∧┐K)前提⑵J→(┐K∧E)前提⑶┐E间接假设⑷J∧┐K⑴⑶否析律⑸J⑷化简⑹┐K∧E⑵⑸肯前律⑺E⑹化简⑻E∧┐E⑶⑺合取⑼E⑶─⑻间接证明2020年2月18日星期二33作业：1.┐X→YX→┐Z┐┐Z∧W∴Y∧W2.E→F∧GE∧HI∨KF∨J→┐I∴K2020年2月18日星期二343.F∨┐G┐H→┐F∴G→H4.E∨(J∧┐K)J→(┐K∧E)∴E2020年2月18日星期二35置换规则的涵义对于任何命题P，无论它是以整个命题出现，还是作为一个命题的一部分出现，都可用与它重言等值的命题Q来替换。2020年2月18日星期二36置换规则T18(a)(A∧B)├┤A∨B(记为DeM.)T18(b)(A∨B)├┤A∧B(记为DeM.)2020年2月18日星期二37德摩根律的证明T18(a)(A∧B)├┤A∨B的证明先证(A∧B)├A∨B:(1)(A∧B)A(2)(A∨B)H1(3)AH2(4)A∨B(3)，∨+(5)(A∨B)∧(A∨B)(2),(4),∧+(6)A(3)—(5),_(消去H2)(7)BH3(8)A∨B(7)，∨+(9)(A∨B)∧(A∨B)(2)，(8)，∧+(10)B(7)—(9)，_(消去H3)(11)A∧B(6)，(10),∧+(12)(A∧B)∧(A∧B)(1)，(11),∧+(13)A∨B(2)—(12)，_(消去H1)2020年2月18日星期二38德摩根律的证明T18(a)(A∧B)├┤A∨B的证明再证A∨B├(A∧B)：(1)A∨BA(2)(A∧B)H(3)A∧B(2)，_(4)A(3)，∧_(5)B(3)，∧_(6)A(4)，+(7)B(1),(6),∨_(8)B∧B(5),(7),∧+(9)(A∧B)(2)—(8),_(消去H)2020年2月18日星期二39置换规则交换律T21(a)A∧B├┤B∧AT21(b)A∨B├┤B∨A结合律T22(a)A∨(B∨C)├┤(A∨B)∨CT22(b)A∧(B∧C)├┤(A∧B)∧C2020年2月18日星期二40置换规则分配律T23(a)A∧(B∨C)├┤(A∧B)∨(A∧C)T23(b)A∨(B∧C)├┤(A∨B)∧(A∨C)蕴析律（A→B)├┤(A∨B)德摩根律(A∧B)├┤(A∨B)(A∨B)├┤(A∧B)2020年2月18日星期二41置换规则的证明T21(b)A∨B├┤B∨A的证明先证A∨B├B∨A(1)A∨BA(2)AH1(3)B∨A(2)，∨+(4)A→B∨A(2)—(3)，→+（消去H1）(5)BH2(6)B∨A(5)，∨+(7)B→B∨A(5)—(6)，→+（消去H2）(8)B∨A(1)，(4)，(7)，D.C.同理，可证B∨A├A∨B。2020年2月18日星期二42NP系统中的语法(语形)推出关系T24(a)(Ａ→B)├┤A∧BT24(b)A→B├┤(A∧B)T25(a)A→B├┤A∨B(蕴析律)T25(b)A∨B├┤A→ＢT26(a)(A∧B)├┤A→ＢT26(b)A∧Ｂ├┤(A→Ｂ)T27(a)A∧Ｂ├┤(A∨Ｂ)T27(b)A∨Ｂ├┤(A∧Ｂ)T28(b)A→B,A→C,B∨C├A(二难推理)T28(c)A→C，B→D，A∨B├C∨DT28(d)A→C，B→D，C∨D├A∨B2020年2月18日星期二43NP系统中的语法(语形)推出关系T29(a)A∧B→C├┤A∧C→B(反三段论)T29(b)A∧B→C├┤B∧C→AT30A∧B→C├A→(B→C)(条件输出)T31A→(B→C)├A∧B→C(条件输入)T32A→(B→C)├┤B→(A→C)(条件互易)T33A→(B→C)├┤(A→B)→(A→C)（蕴涵分配）T34A→(A→B)├┤A→B(条件融合)T35(a)A→B├A∧C→B∧C(前件附加)T35(b)A→B├A∨C→B∨CT35(c)A→B├(C→A)→(C→B)T36（