離散數(shù)學(xué)命題演算系統(tǒng)

離散數(shù)學(xué)命題演算系統(tǒng)第1頁(yè)，共30頁(yè)，2023年，2月20日，星期一目錄數(shù)理邏輯集合論圖論抽象代數(shù)第2頁(yè)，共30頁(yè)，2023年，2月20日，星期一數(shù)理邏輯命題演算命題與聯(lián)結(jié)詞重言式范式命題演算形式系統(tǒng)謂詞演算個(gè)體、謂詞和量詞謂詞演算永真式謂詞公式的前束范式一階謂詞演算形式系統(tǒng)第3頁(yè)，共30頁(yè)，2023年，2月20日，星期一上次我們講到……幾種命題公式重言式、矛盾式、可滿足式邏輯等價(jià)、邏輯蘊(yùn)含重言式的代入原理命題公式的替換原理析（合）取范式、主析（合）取范式聯(lián)結(jié)詞的（極?。┕δ芡陚浼?頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)重言式反應(yīng)了人類(lèi)邏輯思維的基本規(guī)律排中律A∨?A╞╡t矛盾律A∧?A╞╡f假言推理A∧(A→B)╞B歸謬推理(A→B)∧?B╞?A窮舉推理(A∨B)∧(A→C)∧(B→C)╞C真值計(jì)算、以代入原理、替換原理進(jìn)行推演難以反應(yīng)人類(lèi)思維推理過(guò)程，需要建立嚴(yán)密的符號(hào)推理體系第5頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)形式系統(tǒng)是一個(gè)符號(hào)體系系統(tǒng)中的概念由符號(hào)表示推理過(guò)程即符號(hào)變換的過(guò)程以若干最基本的重言式作為基礎(chǔ)，稱(chēng)作公理（axioms）系統(tǒng)內(nèi)符號(hào)變換的依據(jù)是若干確保由重言式導(dǎo)出重言式的規(guī)則，稱(chēng)作推理規(guī)則（rulesofinference）公理和推理規(guī)則確保系統(tǒng)內(nèi)由正確的前提總能得到正確的推理結(jié)果第6頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：證明與演繹證明(proof)公式序列A1,A2,…,Am稱(chēng)作Am的一個(gè)證明，如果Ai(1≤i≤m)或者是公理，或者由Aj1,…,Ajk(j1,…,jk<i)用推理規(guī)則推得。當(dāng)這樣的證明存在時(shí)，稱(chēng)Am為系統(tǒng)的定理(theorem)，記作┠*Am（*是形式系統(tǒng)的名稱(chēng)），或者簡(jiǎn)記為┠Am第7頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：證明與演繹演繹(deduction)設(shè)Γ為一公式集合。公式序列A1,A2,…,Am稱(chēng)作Am的以Γ為前提的演繹，如果Ai(1≤i≤m)或者是Γ中的公式，或者是公理，或者由Aj1,…,Ajk(j1,…,jk<i)用推理規(guī)則推得。當(dāng)有這樣的演繹時(shí)，Am稱(chēng)作Γ的演繹結(jié)果，記作Γ┠*Am（*是形式系統(tǒng)的名稱(chēng)），或者簡(jiǎn)記為Γ┠Am稱(chēng)Γ和Γ的成員為Am的前提(hypothesis)證明是演繹在Γ為空集時(shí)的特例第8頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC命題演算形式系統(tǒng)PC(PropositionCalculus)PC的符號(hào)系統(tǒng)命題變?cè)簆,q,r,s,p1,q1,r1,s1,…命題常元：t,f聯(lián)結(jié)詞：?,→（注意是完備集）括號(hào)：(,)命題公式命題變?cè)兔}常元是公式如果A,B是公式，則(?A)，(A→B)均為公式（結(jié)合優(yōu)先級(jí)和括號(hào)省略約定同前）只有有限次使用上面兩條規(guī)則得到的符號(hào)串才是命題公式第9頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PCPC的公理（A,B,C表示任意公式）A1:A→(B→A)A2:(A→(B→C))→((A→B)→(A→C))A3:(?A→?B)→(B→A)PC的推理規(guī)則（A,B表示任意公式）A,A→B/B（分離規(guī)則）第10頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PCPC的合理性(soundness)如果公式A是系統(tǒng)PC的定理，則A是重言式（如果┠PCA，則╞A）如果A是公式集合Γ的演繹結(jié)果，那么A是Γ的邏輯結(jié)果（如果Γ┠PCA，則Γ╞A）PC合理性的證明PC中的公理A1,A2,A3都是重言式；PC的分離規(guī)則是“保真”的，就是如果A真，A→B真，總有B真。這樣，由公理和規(guī)則導(dǎo)出的所有定理都是重言式由Γ、公理和規(guī)則導(dǎo)出的公式，在Γ中的公式都為真時(shí)也為真第11頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PCPC的一致性(consistency)沒(méi)有公式A，使得┠PCA和┠PC?A同時(shí)成立由PC的合理性容易證明PC的完備性(completeness)如果公式A是重言式，則A一定是PC中的定理（如果╞A，則┠PCA）如果公式A是公式集合Γ的邏輯結(jié)果，則A一定是Γ的演繹結(jié)果（如果Γ╞A，則Γ┠PCA）證明很難，略。第12頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC證明定理：┠PCA→A1](A→((A→A)→A))→((A→(A→A))→(A→A))：公理A22]A→((A→A)→A)：公理A13](A→(A→A))→(A→A)：對(duì)1,2使用分離規(guī)則4]A→(A→A)：公理A15]A→A：對(duì)3,4使用分離規(guī)則第13頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC證明：{A,B→(A→C)}┠B→C1]A：前提2]B→(A→C)：前提3]A→(B→A)：公理A14]B→A：對(duì)1,3用分離規(guī)則5](B→(A→C))→((B→A)→(B→C))：公理A26](B→A)→(B→C)：對(duì)2,5用分離規(guī)則7]B→C：對(duì)4,6用分離規(guī)則第14頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC演繹定理對(duì)任意公式集合Γ和公式A,B，Γ┠A→B當(dāng)且僅當(dāng)?！葅A}┠B當(dāng)Γ=?時(shí)，┠A→B當(dāng)且僅當(dāng){A}┠B，或A┠B歸謬定理對(duì)任何公式集合Γ和公式A,B，若?！葅?A}┠B，Γ∪{?A}┠?B，那么Γ┠A窮舉定理對(duì)任何公式集合Γ和公式A,B，若?！葅?A}┠B，?！葅A}┠B，那么Γ┠B第15頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC證明：┠??A→A??A→(?A→??A)：公理A1，由演繹定理證明了：{??A,?A}┠??A?A→(??A→?A)：公理A1，由演繹定理證明了：{?A,??A}┠?A，也就是{??A,?A}┠?A上面兩個(gè)前提，用歸謬定理得到{??A}┠A再用演繹定理，有┠??A→A第16頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：形式系統(tǒng)PC證明：┠(A→C)→(((B→C)→((?A→B)→C))根據(jù)演繹定理，只需要證明{A→C,B→C,?A→B}┠C因?yàn)閧A→C,B→C,?A→B,A}┠C是顯然的{A→C,B→C,?A→B,?A}┠C是易證的根據(jù)窮舉定理{A→C,B→C,?A→B}┠C得證第17頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題一個(gè)形式系統(tǒng)本質(zhì)上說(shuō)是一個(gè)符號(hào)串的集合形式系統(tǒng)的定義就是符號(hào)串集合的構(gòu)造性定義符號(hào)體系規(guī)定了符號(hào)串可能包含的字符（或字符的合法組合模式，詞）如PC中的命題變?cè)?、常元和公式的定義公理規(guī)定了幾個(gè)集合中的符號(hào)串（或者這種符號(hào)串的模式）如PC中的公理，實(shí)質(zhì)是公理模式推理規(guī)則規(guī)定了從集合中已知符號(hào)串轉(zhuǎn)換生成集合中其它符號(hào)串的方法如PC中的分離規(guī)則第18頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題形式系統(tǒng)中的定理本質(zhì)上就是在集合中的符號(hào)串定理的證明過(guò)程就是符號(hào)串的構(gòu)造過(guò)程這個(gè)過(guò)程需要在有限步內(nèi)結(jié)束定理判定問(wèn)題給定一個(gè)符號(hào)串，判定是否形式系統(tǒng)中的定理能否單靠形式系統(tǒng)本身的公理和推理規(guī)則在有限步驟內(nèi)判定定理和非定理？第19頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題例子：一個(gè)簡(jiǎn)單的形式系統(tǒng)MIU符號(hào)系統(tǒng)：M,I,U組成的串初始串：MI公理：MI規(guī)則1：如果串的最后一個(gè)符號(hào)是I，則可以加上一個(gè)U如果xI是定理，那么xIU也是定理規(guī)則2：如果串符合Mx，則可以再加上x(chóng)而生成Mxx，x代表任何一個(gè)由M,I,U組成的串如果Mx是定理，那么Mxx也是定理第20頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題一個(gè)簡(jiǎn)單的形式系統(tǒng)MIU規(guī)則3：如果串中出現(xiàn)連續(xù)3個(gè)I，則可以用U代替III得到新串如果xIIIy是定理，那么xUy也是定理規(guī)則4：如果串中出現(xiàn)UU，則可以將UU刪去得到新串如果xUUy是定理，那么xy也是定理判定問(wèn)題：MU是否系統(tǒng)中的串？MU是否定理？第21頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題一個(gè)簡(jiǎn)單的形式系統(tǒng)MIU由公理和推理規(guī)則，我們?nèi)菀讟?gòu)造定理樹(shù)MIMIUMII12MIUIUMIUIUIUIU22MIIUMIIUIIU12MIIIIMIIIIUMIIIIIIIIMUIMIU1233MU??????2第22頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題一個(gè)簡(jiǎn)單的形式系統(tǒng)MIU用構(gòu)造系統(tǒng)中所有定理的方法并不能保證在有限的步驟內(nèi)能夠判定定理到底MU是不是定理？我們需要利用同構(gòu)機(jī)制求助于系統(tǒng)之外的自然數(shù)運(yùn)算定律第23頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題MIU的一種同構(gòu)M對(duì)應(yīng)3，I對(duì)應(yīng)1，U對(duì)應(yīng)0自然數(shù)31在集合中規(guī)則1：如果集合中有數(shù)以1結(jié)尾，則添一個(gè)0也是集合中的數(shù)規(guī)則2：如果集合中有數(shù)以3開(kāi)始，則把3后面的數(shù)再重復(fù)一次添在末尾也是集合中的數(shù)規(guī)則3：如果集合中有數(shù)包含111，則把111替換成0也是集合中的數(shù)規(guī)則4：如果集合中有數(shù)包含00，則去掉00的數(shù)也是集合中的數(shù)問(wèn)：30是不是集合中的數(shù)？第24頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題MIU的一種同構(gòu)通過(guò)分析數(shù)的構(gòu)造規(guī)則，我們發(fā)現(xiàn)集合中的數(shù)都不可能被3整除31不能被3整除規(guī)則1～4都不能從不能被3整除的數(shù)生成能被3整除的數(shù)30可以被3整除，所以30不屬于這個(gè)集合結(jié)論：MU不是MIU系統(tǒng)中的定理第25頁(yè)，共30頁(yè)，2023年，2月20日，星期一命題演算：定理判定問(wèn)題形式系統(tǒng)PC定理判定問(wèn)題一個(gè)符合PC符號(hào)體系定義的命題公式，是否是PC中的定理？同樣，用PC系統(tǒng)中公理和分離規(guī)則不能保證能在有限步驟判定一個(gè)命題公式是否定理但是，PC有一個(gè)非常重要的同構(gòu)：真值函數(shù)運(yùn)算系統(tǒng)只需要用真值表判定命題公式對(duì)應(yīng)的真值函數(shù)是否重言式，即可判定是否PC中的定理，真值表的運(yùn)算是有限步驟可以完成的。（注意：真值表并不是PC中的成分）第26頁(yè)，共30頁(yè)，2023年，2月20日，星期一下次我們講……謂詞演算個(gè)體、謂詞和量詞謂詞公式永真式一階謂詞演算形式系統(tǒng)FC自然推理系統(tǒng)ND第27頁(yè)，共30頁(yè)，2023年，2月20日，星期一數(shù)理邏輯教學(xué)進(jìn)程第1課：概論和課程介紹（07.02.27）第2課：命題和聯(lián)結(jié)詞（07.03.01）第3課：重言式和范式（07.03.06）第4課：命題演算系統(tǒng)（07.03.13）第5課：謂詞演算和永真式（07.03.15）第6課：謂詞演算形式系統(tǒng)（四）第28頁(yè)，共30頁(yè)，2023年，2月20日，星期一關(guān)于課程教材[O158/75]計(jì)算機(jī)科學(xué)中的離散結(jié)構(gòu)王元元,張桂蕓編著，機(jī)械工業(yè)出版社2004