命題邏輯的形式系統(tǒng).ppt

《命題邏輯的形式系統(tǒng).ppt》由會(huì)員分享，可在線閱讀，更多相關(guān)《命題邏輯的形式系統(tǒng).ppt（39頁(yè)珍藏版）》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

第五章命題邏輯的形式系統(tǒng),第一節(jié)公理演算—P系統(tǒng)的出發(fā)點(diǎn)第二節(jié)P系統(tǒng)定理的證明第三節(jié)P系統(tǒng)定理的演繹第四節(jié)自然演算—NP系統(tǒng)第五節(jié)命題邏輯的系統(tǒng)特征,第一節(jié)公理演算—P系統(tǒng)的出法點(diǎn)（1）,（一）語(yǔ)法部分，關(guān)于對(duì)象語(yǔ)言的理論。1．初始符號(hào)：（1）p，q，r，s…（2），∨（3）（，）2．形成規(guī)則（π，A，B，C等為元變項(xiàng)）：（１）初始符號(hào)（1）中的任意符號(hào)π是一合式公式；（２）如果符號(hào)序列A是合式公式，則（A）是合式公式；（３）如果符號(hào)序列A和B是合式公式，則（A∨B）是合式公式；（４）只有符合以上三條的符號(hào)序列是合式公式。,第一節(jié)公理演算—P系統(tǒng)的出法點(diǎn)（2）,3．定義（用D表示）：D1（A→B）=Df（A∨B）；（蘊(yùn)涵）D2（A∧B）=Df（A∨B）；（合?。〥3（A?B）=Df（A∨B）∧（B∨A）；（等值）4．公理（用A表示公理，用元符號(hào)?表示其跟隨的公式是本系統(tǒng)要肯定的）：A1├（（p∨p）→p）；（重言律，或去析公理）A2├（p→（p∨q））；（析取引入律，或加析公理）A3├（（p∨q）→（q∨p））；（析取交換律，或交析公理）A4├（（q→r）→（（p∨q）→（p∨r）））。（附加律，或蘊(yùn)析公理）,第一節(jié)公理演算—P系統(tǒng)的出法點(diǎn)（3）,5．推理規(guī)則（或變形規(guī)則，用R表示）：R1（代入規(guī)則）：在一個(gè)合式公式A中，用一合式公式B代替A中某變項(xiàng)π的每一次出現(xiàn)（或?qū)中的π全部代以B），從而得到合式公式A（π/B）。即從?A可得?A（π/B）。R2（分離規(guī)則）：從A和A→B（或（A∨B））可得B。R3（定義置換規(guī)則）：定義兩邊的定義項(xiàng)可以互相替換。設(shè)B=DfC，A（B）為包含公式B的A公式，A（B/C）為在A中用公式C置換B的公式。即從├A（B），可得├A（B/C）。１．符號(hào)結(jié)合力規(guī)則：（1）公式最外面的一對(duì)括號(hào)可省略，若有不能省略的括號(hào)，其結(jié)合力最優(yōu)先；（2）真值聯(lián)結(jié)詞的結(jié)合力依下列次序遞減：，∧、∨，→，?,(二）語(yǔ)義部分，關(guān)于符號(hào)和公式解釋的理論,2．關(guān)于形成規(guī)則例：判定（q∨r）∨（p∨q）∨（p∨r）是否為公式。根據(jù)規(guī)則（1），p，q，r是公式，因?yàn)樗鼈兌际亲帜副碇械淖帜?，都屬于π，進(jìn)而屬于A。根據(jù)規(guī)則（2），q是公式，因?yàn)閝為A。根據(jù)規(guī)則（3），q∨r，p∨q，p∨r是公式，因?yàn)樗鼈兙鶠锳∨B。再根據(jù)規(guī)則（2），（q∨r），（p∨q）是公式，它們可看作是A。再兩次根據(jù)規(guī)則（3），最后判定（q∨r）∨（p∨q）∨（p∨r）是公式，因?yàn)樗鼈兛煽醋魇茿∨B。,對(duì)公理的解釋,每一條公理都是本系統(tǒng)最基本的重言式，其真值，可用真值表方法判定。,關(guān)于推理規(guī)則（1）,（1）關(guān)于代入規(guī)則（R1）該規(guī)則要求只有命題變項(xiàng)π才能被代入，而其他多于一個(gè)符號(hào)的公式，例如p都不能被代入。但是，對(duì)于代入的公式B是沒有限制的。另外，如果在A中的π出現(xiàn)不止一次，那么在代入時(shí)必須到處都用同一公式B代替，不能用不同的公式代替，也不能有的不代替。,舉例：,設(shè)公式├A為：├p∨q→q∨pA中被代入的變項(xiàng)π為：q代入的公式B為：q合法代入（├A（π/B））：├p∨q→q∨p不合法代入：p∨q→q∨p（未對(duì)π在A中的所以出現(xiàn)即每一個(gè)q進(jìn)行代替）,關(guān)于定義置換規(guī)則（R3）,這里的置換和前面的代入是不同的。置換要求置換公式和被置換公式是等值（或可互相定義）的，而且是在被置換公式出現(xiàn)的某些位置上進(jìn)行替換。代入則不要求代入公式和被代入公式等值，但必須在被代入公式出現(xiàn)的所有位置上進(jìn)行替換。,舉例：,設(shè)公式├A為：├p→p∨qA中被置換的公式B為：P∨q置換的公式C為：q→p（要求：B=dfC即p∨q?q→p）置換后所得公式（├A（B/C））：├p→（q→p）,關(guān)于符號(hào)省略規(guī)則,根據(jù)形成規(guī)則所構(gòu)造的公式，其符號(hào)過多也過于復(fù)雜。我們可以作些簡(jiǎn)化。本規(guī)則是在保證不影響原公式固有層次的前提下，對(duì)公式的簡(jiǎn)化。例如根據(jù)本規(guī)則，P公理可簡(jiǎn)化為：A1．├p∨p→pA2．├p→p∨qA3．├p∨q→q∨pA4．├（q→r）→（p∨q→p∨r）,3．2P系統(tǒng)定理的證明,所謂P定理的證明，乃是一有窮的公式序列A1，…，An，其中每一公式Ai（1≤i≤n）都適合以下條件之一：（1）Ai是一公理；（2）Ai是一已證定理；（3）Ai由本序列在先的一個(gè)公式經(jīng)代入或置換所得到；（4）Ai由本序列在先的兩個(gè)公式Aj和Ak（其形式分別為B和B→Ai，j?i，k?i）經(jīng)分離所得到；（5）最后一個(gè)公式An是要證明的定理。,,定理的證明,T1├（q→r）→（（p→q）→（p→r））證：1.├（q→r）→（p∨q→p∨r）公理42.├（q→r）→（p∨q→p∨r）1代入p/p3.├（q→r）→（（p→q）→（p→r））2定義1置換,T2├p→p,證：1．├p→p∨q公理22．├p→p∨p1代入q/p3．├p∨p→p公理14、├（q→r）→（（p→q）→（p→r））定理15、├（p∨p→p）→（（p→p∨p）→（p→p））4代入q/p∨p，r/p6．├（p→p∨p）→（p→p）5，3分離7．├p→p6，2分離,T3├p∨p（略）T4├p∨p,證：1．├p∨q→q∨p公理32．├p∨p→p∨p1代入p/p，q/p3．├p∨p定理34．├p∨p3，2分離,T5├p→p（略）T6├p→p,證：1．├p→p定理52．├p→p1代入p/p3．├（q→r）→（p∨q→p∨r）公理44．├（p→p）→（p∨p→p∨p）3代入q/p，r/p5．├p∨p→p∨p4，2分離6．├p∨p定理47．├p∨p5，6分離8．├p∨q→q∨p公理39．├（p∨p）→（p∨p）8代入q/p10．├p∨p9，7分離11．├p→p10定義1置換,T7├（p→q）→（q→p）,證：1．├p→p定理52．├q→q1代入p/q3．├（q→r）→（p∨q→p∨r）公理44．├（q→q）→（p∨q→p∨q）3代入r/q，p/p5．├p∨q→p∨q4，2分離6．├p∨q→q∨p公理37．├（p∨q）→（q∨p）6代入p/p，q/q8．├（q→r）→（（p→q）→（p→r））定理19├（p∨q→q∨p）→（（p∨q→p∨q）→（p∨q→q∨p）8代入q/p∨q，r/q∨p，p/p∨q10．├（p∨q→p∨q）→（p∨q→q∨p）9，7分離11．├p∨q→q∨p10，5分離12．├（p→q）→（q→p）11定義1置換,T8├（p∧q）→p∨q（略）T9├p∨q→（p∧q）,證：1．├p→p定理52．├p∨q→（p∨q）1代入p/p∨q3．├p∨q→（p∧q）2定義2置換,定理的簡(jiǎn)化證明,使證明簡(jiǎn)化的一個(gè)主要方法是把本系統(tǒng)中的公理和已證定理當(dāng)作推理規(guī)則使用。這些規(guī)則稱作導(dǎo)出規(guī)則。列舉如下：1.析取交換規(guī)則：從├A∨B可得├B∨A公理32.附加規(guī)則：從├B→C可得├A∨B→A∨C。公理43.三段論規(guī)則：從├B→C和├A→B可得├A→C。定理14.假言易位規(guī)則：從├A→B可得├B→A。定理75.等值構(gòu)成規(guī)則：從├A→B和├B→A可得├A?B。定義36.等值置換規(guī)則：如果A和B等值，即├A?B，則從├φA可得├ΦB。Φ表示任意合式公式，其中A（或B）是Φ的子公式。A，B可相互置換。這是定義置換規(guī)則的擴(kuò)充。,導(dǎo)出規(guī)則2,7．結(jié)合括號(hào)省略規(guī)則：（1）從├（A∨B）∨C可得├A∨B∨C；（2）從├（A∧B）∧C可得├A∧B∧C。8.條件互易規(guī)則：從├A→（B→C）可得├B→（A→C）。9．合取構(gòu)成規(guī)則：從├A→（B→C）可得├A∧B→C。10．條件融合規(guī)則：從├A→（A→B）可得├A→B。以上8，9，10三條規(guī)則都是相應(yīng)定理的概括。11．求否定規(guī)則：設(shè)A為一公式，A中沒有→和?出現(xiàn)（或已定義為，∨或∧），其否定式（記為A-）用以下方法可得：將∨，∧互換，同時(shí)π將和π互換（π為任一命題變項(xiàng)）。例如，p∧（q∨r）∧r，其否定式為p∨（q∧r）∨r。12．對(duì)偶規(guī)則：設(shè)A，B為兩個(gè)公式，在其中→和?不出現(xiàn)。A~和B~是在A和B中把∨和∧互換的結(jié)果。我們可有：（1）從├A→B可得├B~→A~；（2）從├A?B可得├A~?B~。,一些已證或待證定理的簡(jiǎn)化證明,T2├p→p證：1．├p→p∨q公理22．├p→p∨p1代入q/p3．├p∨p→p公理14．├p→p2，3三段論T4├p∨p證：1．├p∨p公理32．├p∨p1析取交換,簡(jiǎn)化證明（2）,T6├p→p證：1．├p→p定理52．├p→p1代入p/p3．├p∨p→p∨p2附加4．├p∨p定理45．├p∨p3，4分離6．├p∨p5析取交換7．├p→p6定義1置換T10├p?p證：1．├p→p定理52．├p→p定理63．├p?p1，2等值構(gòu)成,簡(jiǎn)化證明（3）,T7├（p→q）→（q→p）證：1．├p∨q→q∨p公理32．├p∨q→q∨p1代入p/p3．├p∨q→q∨p2等值置換4．├（p→q）→（q→p）3定義置換1T11├（p∧q）?p∨q證：1．├（p∧q）→p∨q定理82．├p∨q→（p∧q）定理93．├（p∧q）?p∨q1，2等值構(gòu)成T12├（p∨q）?p∧q證：1．├（p∧q）?p∨q定理112．├（p∨q）?p∧q1對(duì)偶,簡(jiǎn)化證明（4）,T13├p→q∨pT14├p∧q→q∧pT15├p∧q→pT16├p∧q→qT17├p∨（q∨r）→q∨（p∨r）T18├p∨（q∨r）→（p∨q）∨rT19├（p∨q）∨r→p∨（q∨r）T20├p∧（q∧r）→（p∧q）∧rT21├q∧（p∧r）→p∧（q∧r）T22├p→（q→p∧q）T23├（p→（q→r））→（q→（p→r））,簡(jiǎn)化證明（5）,T24├（p→（q→r））?（p∧q→r）T25├（p→（p→q））?（p→q）T26├p∨（q∧r）?（p∨q）∧（p∨r）T27├p∧（q∨r）?（p∧q）∨（p∧r）T28├（p→q）∧（p→r）?（p→q∧r）T29├p?p∨（q∧q∧r）T30├p?p∧（q∨q∨r）T31├（p?q）?（p?q）T32├（p?q）?（p∨q）∧（q∨p）T33├（p?q）?（p∧q）∨（p∧q）T34├（p?q）?（p∧q）∨（p∧q）以上只是P系統(tǒng)的部分定理，請(qǐng)讀者自證。,3．3P系統(tǒng)定理的演繹,令?是P中的一組公式，它們可以是P中的公理或定理，也可以不是。P中以?為前提的演繹是一有窮的公式序列A1，…，An，其中每一公式Ai（1≤i≤n）都適合下列條件之一：（1）Ai是一公理或定理；（2）Ai是Γ中的一個(gè)公式（記為Hyp）；（3）Ai由本序列在先的一個(gè)或兩個(gè)公式根據(jù)推理規(guī)則（系統(tǒng)內(nèi)的基本變形規(guī)則和導(dǎo)出規(guī)則，但對(duì)假設(shè)前提公式不得使用代入規(guī)則）而得到。如果這樣一個(gè)演繹存在，我們就稱該序列最后的一個(gè)公式An以?為前提是可演繹的，或稱An為P中?的后承，記為?├An。當(dāng)假設(shè)前提集為空集時(shí)，P中關(guān)于空前提的演繹就是P中的一個(gè)證明。A是P中的定理，記作?├A，簡(jiǎn)記成├A。,演繹定理,令A(yù)、B為P中任意公式，?為P中任何公式集，如果{?，A}├B，那么?├A→B。意即如P中一前提集?和另一前提A能推出B，那么，由?本身可推出A→B。當(dāng)?為空集時(shí)，如果由一前提A能推出B，那么，A→B可無前提推出，即為P的定理（├A→B）。,反證定理,令A(yù)為P中任意公式，?為P中任何公式集，如果{?，A}├?∧?，那么?├A。意即如果從P的一前提公式集和一命題公式A的否定推出了矛盾，則從該前提集可推出A。當(dāng)?為空集時(shí)，如果由一前提A能推出?∧?，那么，A可無前提推出，即A為P的定理（├A）。,對(duì)P系統(tǒng)部分定理的演繹證明（1）,T13├p→q∨p證：1．pHyp2．p→p∨q公理23．p∨q2，1分離4．p∨q→q∨p公理35．q∨p4，3分離6．├p→q∨p1，5演繹定理（又一附加的導(dǎo)出規(guī)則：從p可得q∨p）,演繹證明（2）,T14├p∧q→q∧p證：1．p∧qHyp2．（p∨q）1定義2置換3．p∨q→q∨p公理34．（q∨p）→（p∨q）3假言易位5．（p∨q）→（q∨p）4代入p/q，q/p6．（q∨p）5，2分離7．q∧p6定義2置換8．├p∧q→q∧p1，7演繹定理（合取交換的導(dǎo)出規(guī)則：從p∧q可得q∧p）,演繹證明（3）,T15├p∧q→p證：1．p∧qHyp2．（p∨q）1定義2置換3．p→p∨q公理24．p→p∨q3代入p/p，q/q5．（p∨q）→p4假言易位（R導(dǎo)4）6．p5，2分離7．p6等值置換（R導(dǎo)6）8．├p∧q→p1，7演繹定理（導(dǎo)出規(guī)則：從p∧q可得p。與此相同的方法，可證定理T16├p∧q→q，得導(dǎo)出規(guī)則：從p∧q可得q。它們是合取分解規(guī)則）,演繹證明（4）,T22├p→（q→p∧q）證：1．pHyp2．p→p定理23．p∧q→p∧q2代入p/p∧q4．（p∧q）∨（p∧q）3定義1置換5．（p∨q）∨（p∧q）4等值置換6．p∨（q∨（p∧q））5析取結(jié)合（R導(dǎo)7）7．q∨（p∧q）6，1分離8．q→p∧q7定義置換9．├p→（q→p∧q）1，8演繹定理（合取組合的導(dǎo)出規(guī)則：從p和q可得p∧q）,演繹證明（5）,T23├（p→（q→r））→（q→（p→r））證：1．p→（q→r）Hyp2．qHyp3．pHyp4．q→r1，3分離5．r4，2分離6．p→r3，5演繹定理7．q→（p→r）2，6演繹定理8．├（p→（q→r））→（q→（p→r））1，7演繹定理（由于演繹定理的引入，所有已證定理都可看作是一導(dǎo)出規(guī)則，而且象上節(jié)導(dǎo)出規(guī)則中前提與結(jié)論前的斷定符都可去掉。如“換頭”可表示為：從p→（q→r）可得q→（p→r）。）,演繹證明（6）,T24├（p→（q→r））?（p∧q→r）該定理的證明分兩步，先證前件蘊(yùn)涵后件，再證后件蘊(yùn)涵前件。即：證：├（p→（q→r））→（p∧q→r）1．p→（q→r）Hyp2．p∧qHyp3．p2合取分解4．q2合取分解5．q→r1，3分離6．r5，4分離7．p∧q→r2，6演繹定理8．├（p→（q→r））→（p∧q→r）1，7演繹定理（合取構(gòu)成的導(dǎo)出規(guī)則：從p→（q→r）可得p∧q→r）,演繹證明（7）,再證：├（p∧q→r）→（p→（q→r））1．p∧q→rHyp2．pHyp3．qHyp4．p∧q2，3合取組合5．r1，4分離6．q→r3，5演繹定理7．p→（q→r）2，6演繹定理8．├（p∧q→r）→（p→（q→r））1，7演繹定理,3．5命題邏輯的系統(tǒng)特征,當(dāng)我們把命題演算系統(tǒng)作為研究對(duì)象時(shí)，我們考察的是形式不同的各命題邏輯系統(tǒng)共同的特征，也稱元邏輯問題，即一命題邏輯系統(tǒng)的所有可證公式或者說定理是否都是重言式，即可證的是否都是真的？這個(gè)問題稱作系統(tǒng)的一致性問題。另一個(gè)問題是，是否所有命題邏輯的重言式都在一命題邏輯系統(tǒng)中可證，即真的是否都可證？這個(gè)問題稱作系統(tǒng)的完全性問題。另外還有公理獨(dú)立性問題，即一公理系統(tǒng)的每條公理，彼此應(yīng)該互相獨(dú)立，不能由一個(gè)公理而推出另一個(gè)公理；各演算系統(tǒng)間的關(guān)系問題，如P系統(tǒng)和NP系統(tǒng)是等價(jià)的，即兩系統(tǒng)的定理集是相同的，相對(duì)于某些給出的推理規(guī)則，能彼此證明對(duì)方的公理和定理的是自己的公理或定理。以下我們僅考察一致性、完全性和獨(dú)立性問題。,（一）一致性,一命題邏輯的形式系統(tǒng)是一致的，即該系統(tǒng)的所有定理都是重言式（語(yǔ)義一致）?；蛘哒f并非該系統(tǒng)的一切公式都是定理（語(yǔ)法一致）?；蛘哒f對(duì)于該系統(tǒng)的任一公式A而言，A和A至少有一個(gè)不是該系統(tǒng)中的定理（古典的語(yǔ)法一致）。如何能確定或證明一個(gè)命題演算系統(tǒng)的所有定理都是重言式？通常的方法是為該系統(tǒng)找到一個(gè)解釋，使得：（1）命題演算的公理都是真命題（重言式）；（2）應(yīng)用命題演算的推理規(guī)則和定義，都能保證從重言式只能推出重言式。如果條件（1）、（2）都滿足了，應(yīng)用該推理規(guī)則從公理所推出的所有定理也是重言式，則證明了該系統(tǒng)是（語(yǔ)義）一致的。,（二）完全性,一命題邏輯的形式系統(tǒng)是完全的，即一切重言式都在該系統(tǒng)中可證（廣義的、相對(duì)的或語(yǔ)義的完全性）?；蛘哒f，如果把在該系統(tǒng)不可證的公式作為新公理引進(jìn)該系統(tǒng)，就會(huì)導(dǎo)致矛盾而使該系統(tǒng)不一致（狹義的、絕對(duì)的或語(yǔ)法的完全性）?；蛘哒f，對(duì)于該系統(tǒng)任一合式公式A而言，或者A是可證的，或者A是可證的（古典的完全性）?？梢宰C明P系統(tǒng)是語(yǔ)義完全的和語(yǔ)法完全的。,（三）獨(dú)立性,所謂獨(dú)立性就是公理的不可推出性。根據(jù)給定的推理規(guī)則，如果從一類公式推不出某一特定公式，那么這一公式對(duì)于那一類公式就是獨(dú)立的。不過，若應(yīng)用某些推理規(guī)則推不出來，而用另一些推理規(guī)則就可能推出來。所以，獨(dú)立性總是相對(duì)于已給定的推理規(guī)則而言的?？梢宰C明P系統(tǒng)的公理都是獨(dú)立的。,