命題邏輯公理化_第1頁
命題邏輯公理化_第2頁
命題邏輯公理化_第3頁
命題邏輯公理化_第4頁
命題邏輯公理化_第5頁
已閱讀5頁,還剩10頁未讀 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報(bào)或認(rèn)領(lǐng)

文檔簡介

命題邏輯公理化第1頁,共15頁,2023年,2月20日,星期一形式化與公理化此前我們討論命題邏輯,是從語義角度,非形式化地、不嚴(yán)謹(jǐn)?shù)剡M(jìn)行解釋性的討論.而數(shù)學(xué)傳統(tǒng)追求的是嚴(yán)格的形式化、公理化系統(tǒng).形式化:符號化,只有語法定義,并無語義解釋.公理化:從初始符號串(公理)出發(fā),根據(jù)符號變換規(guī)則,推導(dǎo)出其他符號串(定理).具體的公理化系統(tǒng):語法+語義形式的公理化系統(tǒng):語法.歐氏幾何就是一個(gè)經(jīng)典的公理化系統(tǒng).LuChaojun,SJTU2第2頁,共15頁,2023年,2月20日,星期一形式系統(tǒng)的組成形式系統(tǒng)組成:初始符號:可用符號的集合.形成規(guī)則(wff定義):規(guī)定如何構(gòu)成合法的符號串(wff).初始公式(公理):進(jìn)行推導(dǎo)的出發(fā)點(diǎn).變形規(guī)則(推理規(guī)則):規(guī)定如何從幾個(gè)wff經(jīng)過符號變換得出另一wff.建立了形式系統(tǒng),即可進(jìn)行推理,從老wff產(chǎn)生新的wff(定理).不是所有wff都是定理.LuChaojun,SJTU3第3頁,共15頁,2023年,2月20日,星期一例:一個(gè)形式系統(tǒng)形式系統(tǒng):初始符號:,,形成規(guī)則:,,的任意有限序列都是wff.初始公式:令x是任一串,系統(tǒng)有唯一公理(模式) A1:xx變形規(guī)則:令x,y,z表示任意串. R1:若xyz是定理,則

xyz也是定理.在此系統(tǒng)里可以證明是定理.證明: (1)

A1[x/] (2). (1)R1此系統(tǒng)有意義嗎?試試這個(gè)解釋:解釋為+,解釋為=.LuChaojun,SJTU4第4頁,共15頁,2023年,2月20日,星期一命題邏輯的重言式公理系統(tǒng)命題邏輯的重言式可組成一個(gè)公理系統(tǒng).后面給出這個(gè)形式化公理系統(tǒng).該系統(tǒng)的語義可以是:初始符號表示有真假的命題及真值聯(lián)結(jié)詞;初始命題是重言式;從公理出發(fā),利用推理規(guī)則,可以推導(dǎo)出定理.定理都是重言式該系統(tǒng)推出的都是重言式,而且能推出所有重言式.LuChaojun,SJTU5第5頁,共15頁,2023年,2月20日,星期一命題邏輯公理系統(tǒng)初始符號命題符號:A,B,C,……聯(lián)結(jié)詞:,輔助符號:(,)可證符號:|(后接公式,表示該公式在系統(tǒng)中是可證明的)LuChaojun,SJTU6第6頁,共15頁,2023年,2月20日,星期一命題邏輯公理系統(tǒng)(續(xù))形成規(guī)則(1)命題符號是公式;(2)若是公式,則是公式;(3)若和是公式,則是公式;(4)公式僅限于此.LuChaojun,SJTU7第7頁,共15頁,2023年,2月20日,星期一命題邏輯公理系統(tǒng)(續(xù))定義D1.定義為(

)D2.定義為D3.定義為()()這是為了簡化公式表達(dá).也可將作為初始符號,并增加相應(yīng)形成規(guī)則.LuChaojun,SJTU8第8頁,共15頁,2023年,2月20日,星期一命題邏輯公理系統(tǒng)(續(xù))公理A1.|

(P

P

)PA2.|

P

(P

Q

)A3.|

(P

Q

)(Q

P

)A4.|

(Q

R

)((P

Q

)(P

R

))LuChaojun,SJTU9第9頁,共15頁,2023年,2月20日,星期一命題邏輯公理系統(tǒng)(續(xù))變形規(guī)則(推理規(guī)則)R1.代入規(guī)則:若|,則|[p/]. (將公式中的某符號p處處代以公式,稱為代入,結(jié)果記作[p/].)R2.分離規(guī)則:若|,|,則|.R3.置換規(guī)則:定義的左右方可互相替換.設(shè)對公式施以置換后得到公式.若|,則|.LuChaojun,SJTU10第10頁,共15頁,2023年,2月20日,星期一定理的證明設(shè)有公式序列1,2,…,n.如果每個(gè)i

(1in)

(1)或者是公理之一; (2)或者是由前面的一個(gè)或兩個(gè)h和k(h,k<i)實(shí)施推理規(guī)則而得;

則稱此公式序列是定理n的一個(gè)證明.LuChaojun,SJTU11第11頁,共15頁,2023年,2月20日,星期一例:定理證明定理1:|

(QR

)((PQ

)(PR

))(1)

|(QR)((PQ

)(PR

)) A4(2)|(QR)((PQ

)(PR

)) (1)代入[P/P](3)|

(QR

)((PQ

)(PR

)) (2)置換D2定理2:|

PP(1)P(PQ) A2(2)P(PP)

(1)代入[Q/P](3)

(PP)P A1(4)(QR

)((PQ

)(PR

)) 定理1(5)((PP)P)((P(PP))(PP)) (4)代入[Q/PP,R/P](6)(P(PP))(PP) (3)(5)分離(7)PP (2)(6)分離LuChaojun,SJTU12第12頁,共15頁,2023年,2月20日,星期一公理系統(tǒng)的性質(zhì)協(xié)調(diào)性(相容性,一致性,不矛盾性)推出的定理都是真的;或和不都是定理.完備性(完全性)所有定理均能在系統(tǒng)中推出.獨(dú)立性公理不能被其他公理推出.LuChaojun,SJTU13第13頁,共15頁,20

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

最新文檔

評論

0/150

提交評論