形式化數(shù)理邏輯

1、1形式化數(shù)理邏輯形式化數(shù)理邏輯n侯越先，, 25-B-510n一般性參考： 離散數(shù)學(xué)，左孝凌等，上?？茖W(xué)技術(shù)出版社 數(shù)學(xué)家的邏輯，哈密爾頓，商務(wù)印書館 元數(shù)學(xué)導(dǎo)論， SC克林，科學(xué)出版社n課程輔助材料： 2重新審視邏輯的本質(zhì)n真與邏輯n經(jīng)驗(yàn)意義上，命題的“真”指命題的斷言符合其所指涉事物的實(shí)際狀態(tài)n邏輯（Logics）研究的是有效的推理方法，數(shù)理邏輯（Mathematical Logics）就是用數(shù)學(xué)化（符號(hào)化）的手段，研究有效的推理方法3重新審視邏輯的本質(zhì)n什么是有效推理方法? a 有效推理方法應(yīng)具備保真性，即如果推理前提真，則推理結(jié)論真 b 有效推理方法的保真性應(yīng)具有普遍意義，即不同的人，

2、在不同的應(yīng)用背景下使用相同的推理過程，可獲得真值相同的結(jié)論n有效推理的例子：三段論4重新審視邏輯的本質(zhì)n兩個(gè)基本問題： 問題1：是否所有真命題都可從特定的邏輯前提出發(fā)，由滿足條件a和b的邏輯推理過程獲得？ 問題2：如果推理前提真，有效推理方法的結(jié)論是否無條件地真？5重新審視邏輯的本質(zhì)n問題1（是否所有真命題都可從特定的推理前提出發(fā)，由滿足條件a和b的邏輯推理過程獲得？）n下面各個(gè)推理結(jié)論（藍(lán)色部分）的真值由何決定？ 例1 因?yàn)樗轻t(yī)生，所以他是大夫 例2 如果下雨，野餐取消； 現(xiàn)在確實(shí)下雨了； 野餐將取消 例3 如果A勝過B； 且B勝過C； 則A勝過C 例4 任何一個(gè)男同學(xué)都不能斷定本語句是真

3、的6重新審視邏輯的本質(zhì)n獲致“真”的途徑： 基于邏輯的真（基于形式的真） 基于語義的真 基于直覺的真n注：4與說謊者悖論的區(qū)別 4與哥德爾不完備性定理之間的關(guān)系n數(shù)理邏輯的研究目的：研究形式有效的推理，用形式手段地刻畫人們對形式真的樸素理解。7重新審視邏輯的本質(zhì)n問題2（如果推理前提真，有效推理方法的結(jié)論是否無條件地真？）n例子（量子物理的雙縫實(shí)驗(yàn)）：電子e通過左縫隙或右縫隙達(dá)到屏幕，且通過縫隙時(shí)的動(dòng)量是pn小練習(xí)：將以上例子用命題邏輯符號(hào)化n量子邏輯：刻畫量子世界的命題邏輯1 G. Birkhoff and J. von Neumann, The Logic of Quantum Mecha

4、nics2 http:/wapedia.mobi/en/Quantum_logic8重新審視邏輯的本質(zhì)nRemark 1：形式邏輯系統(tǒng)本質(zhì)上是一種形式約定系統(tǒng)，系統(tǒng)內(nèi)的真命題（永真式）只在形式約定的意義下為真，而并不必然對應(yīng)于實(shí)際物理狀態(tài)。nRemark 2：只有當(dāng)形式邏輯系統(tǒng)的解釋（即模型）確定之后，才可能討論形式命題（在特定解釋下的）“物理真實(shí)性”。一般來說，古典邏輯系統(tǒng)適用于經(jīng)典物理世界，因此在日常情況下，基于古典邏輯系統(tǒng)得出的真命題對應(yīng)于事物的實(shí)際狀態(tài)。以下我們約定已給出合適的模型，使得形式真等價(jià)于真9形式化數(shù)理邏輯的研究目的形式化數(shù)理邏輯的研究目的n1 研究邏輯（形式）有效的推理，用

5、形式手段刻畫人們對邏輯（形式）真的樸素理解n2 研究形式邏輯系統(tǒng)的元性質(zhì)：可靠性、可判定性、完備性等n形式化命題邏輯、形式化謂詞邏輯、形式化非古典邏輯n思考題：是否有可能對基本的形式邏輯系統(tǒng)加以擴(kuò)張，使其可把握其他類型的真？詳細(xì)說明你的意見10形式數(shù)理邏輯的主要研究內(nèi)容n3 擴(kuò)展研究目的n模型論、證明論、遞歸論、公理化集合論 模型論：用數(shù)理邏輯和集合論的方法解釋、分析形式的（數(shù)學(xué)或物理）概念和系統(tǒng) 證明論：用數(shù)理邏輯的方法研究數(shù)學(xué)證明的過程 遞歸論：研究解決問題的可行的計(jì)算方法和計(jì)算的復(fù)雜程度11形式化命題邏輯系統(tǒng)Ln（非形式）命題邏輯系統(tǒng)的能力和局限 命題邏輯系統(tǒng)的結(jié)論都是真的嗎？（考慮命題

6、邏輯中真的定義） 命題邏輯系統(tǒng)的能力是否足夠強(qiáng)，使得我們可由命題邏輯系統(tǒng)（算法地）推出所有的邏輯真命題？n引入形式化命題邏輯系統(tǒng) 理論方面：澄清命題邏輯系統(tǒng)的元性質(zhì)(一致性、完備性和可判定性等）、澄清基本的數(shù)學(xué)哲學(xué)問題（例如數(shù)學(xué)是否可以形式化） 應(yīng)用方面，形式化邏輯系統(tǒng)在人工智能、軟件工程等領(lǐng)域有著深入的應(yīng)用。n命題邏輯的形式系統(tǒng)L定義如下 1 符號(hào)字母表： ，（，），p1，p2，p3， 問題：為何只有兩個(gè)邏輯聯(lián)結(jié)詞和？12形式化命題邏輯系統(tǒng)L2 命題公式的集合：如下3條遞歸規(guī)則確定命題公式的集合（1）對每個(gè)i=1，pi是命題公式（2）若A和B是命題公式，則（A）和（AB）是命題公式（3）所有

7、命題公式由遞歸應(yīng)用（1）和（2）產(chǎn)生 注：在不引起歧義的情況下，括號(hào)可省略3 公理模式： L1: （A（BA） L2: （A（BC）（AB）（AC） L3: （ A）（B）（BA） 注：A、B和C可以是任意命題公式 顯然，公理L1-L3是永真式 13形式化命題邏輯系統(tǒng)L4 演繹規(guī)則（分離規(guī)則，記為MP)：從A和（AB），可以獲得Bn定義1：L中的一個(gè)證明是命題公式的一個(gè)序列A1，A2，An，使得對每個(gè)i（1=i1時(shí)，假設(shè)L中證明序列長度小于n的定理都是重言式（歸納假設(shè)）。由于定理A在L中存在一個(gè)證明，則A或者是L的公理，或者由MP規(guī)則獲得。當(dāng)A是L的公理時(shí)，A顯然是重言式。當(dāng)A是由MP規(guī)則獲得

8、時(shí)，其證明序列中必存在兩個(gè)命題公式，不失一般性，記為B和BA。由于B和BA的證明序列長度小于n，由歸納假設(shè)，它們是重言式。這樣A必然是重言式。 綜上，L是可靠的。17形式化命題邏輯系統(tǒng)Ln定理2（一致性定理）：L是一致的 證明：反證法，若L是不一致的，則存在命題公式A，使得A和A均為L的定理。由L的可靠性定理，L的定理必是重言式，矛盾。n定理3（完備性定理）：L是完備的18定理4證明概要（數(shù)學(xué)家的邏輯）n引理1: (AA)是L的定理n證明: 1) (A(AA)A) L1 2) (A(AA)A) (A(AA)(AA) L2 3) (A(AA)(AA) MP 4) (A(AA) L1 5) (AA

9、) MP 19定理4證明概要（數(shù)學(xué)家的邏輯）n定義6：L* 稱為L的擴(kuò)張，如果L*是通過改變或擴(kuò)大L的公理集合而得到的一個(gè)形式系統(tǒng)，使得L的所有定理仍是L*的定理。n問題：增加L的公理，是否必然增加L的定理？是否可能采用完全不同的公理集，但導(dǎo)出完全相同的定理集？n注：若L*是通過在L中增加公理集合X獲得的，則L*可記為L+X；n注：以下兩個(gè)說法是等價(jià)的 1)命題公式A在L+X中可證 2)命題公式A可在L中由前提X推演（證明）出 3)可記為X|-A 或 |-A L L+X20定理4證明概要（數(shù)學(xué)家的邏輯）n定義7：L的擴(kuò)張L*是一致的，如果不存在命題公式A，使得A和A均為L*的定理n演繹定理：若

10、B是在L+X中增加公理A后形成的擴(kuò)張系統(tǒng)的定理，則(AB)是L+X的定理n證明：數(shù)學(xué)歸納法并利用引理1的結(jié)果n注：逆定理成立n推論：對于任意的A、B和C，在L中可由(AB)和(BC)證得(AC)n證明：在L+(AB),(BC),A中易證C，由演繹定理， L+(AB),(BC)中可證(AC)n注：此推論可進(jìn)一步擴(kuò)展；此推論在邏輯推演中的使用稱為HS規(guī)則21定理4證明概要（數(shù)學(xué)家的邏輯）n引理2：A（AB）和(AA)A是L的定理n一致性判定：由引理2，L的一個(gè)擴(kuò)張L*是一致的，當(dāng)且僅當(dāng)存在一個(gè)命題公式A，A不是L*的定理n引理3：設(shè)L*是L的一致擴(kuò)張，又A是L的命題公式，且A不是L*的定理，那么由

11、L*增加A而得到的擴(kuò)張L*也是一致的n證明：反證法，利用演繹定理和引理2的兩個(gè)定理。n定義8：L的一致擴(kuò)張是完全的，如果對于任意A，A或A是此擴(kuò)張的定理n注：注意這里的“完全”與前面提到的完備性之間的區(qū)別n引理4：設(shè)L*是L的一致擴(kuò)張，則存在L*的一致完全擴(kuò)張22定理4證明概要（數(shù)學(xué)家的邏輯）n定義9：L的一個(gè)賦值是一個(gè)函數(shù)v，它的定義域是L的命題公式集合，它的值域是T,F，使得對L的任意命題公式A和B，有 1) v(A) v(A) 2) v(AB) = F iff v(A)=T 且 v(B)=Fn注：對L的命題符號(hào)p1,p2,的真值指派與L的賦值之間存在一一對應(yīng)關(guān)系。一個(gè)真值指派可決定一個(gè)賦

12、值；反之，合法的賦值對應(yīng)著一個(gè)真值指派。n引理5：若L*是L的一致擴(kuò)張，則存在一個(gè)賦值，使得L*中的所有定理取值Tn證明：賦值由L*的完全一致擴(kuò)張J給出。只需證此賦值滿足定義9中的1)和2)即可23定理4證明概要（數(shù)學(xué)家的邏輯）n定理：L是完備的（L的完備性定理）n證明：反證法，假設(shè)L不完備，則可在L的公理集中增加了某個(gè)永真式Ak的否定，形成一致擴(kuò)張L*。由引理5，存在賦值v使得L*中所有定理為真，則Ak在此賦值下也為真。這意味著永假式Ak在某個(gè)真值指派下為真，矛盾24形式化命題邏輯系統(tǒng)Ln定理4（可判定性定理）：L是可判定的。 證明：真值表法。n問題：真值表法能否作為一般方法在實(shí)際自動(dòng)推理系

13、統(tǒng)中應(yīng)用？n總結(jié)：L具有我們所期望的性質(zhì)（可靠性、一致性、完備性等）n問題：是否可能存在其他的形式命題邏輯系統(tǒng)（不同的聯(lián)結(jié)詞、不同的公理），也具有L的性質(zhì)？n思考題（作業(yè)）：構(gòu)造一個(gè)使用邏輯聯(lián)結(jié)詞、和的形式命題邏輯系統(tǒng)：說明你構(gòu)造的系統(tǒng)公理和推演規(guī)則；證明其具有L的性質(zhì)（可靠性、一致性、可判定性和完備性）。25形式化命題邏輯系統(tǒng)Ln思考題：既然利用形式命題邏輯系統(tǒng)可以中肯把握（命題的）邏輯真，可否擴(kuò)展的形式命題邏輯系統(tǒng)，以中肯地把握特定意義下的數(shù)學(xué)真（Hilbert方案）？例如，構(gòu)造形式化數(shù)論系統(tǒng)。這樣的系統(tǒng)是否也具有系統(tǒng)L的良好性質(zhì)？n思考題：如果上一個(gè)問題的回答是肯定的，這樣的數(shù)學(xué)系統(tǒng)的全

14、部內(nèi)涵即可由形式系統(tǒng)囊括，至少在原則上，我們可以編寫一個(gè)計(jì)算機(jī)程序，利用簡單地窮盡搜索，逐步獲得一個(gè)又一個(gè)定理，數(shù)學(xué)發(fā)現(xiàn)的過程可以還原為計(jì)算機(jī)程序操作，這個(gè)思路是否可行？26形式化命題邏輯系統(tǒng)Ln 線索：這樣的前景不會(huì)發(fā)生。絕大多數(shù)實(shí)際數(shù)學(xué)系統(tǒng)的形式化是不完備的（哥德爾第一不完備性定理），甚至其一致性也無法在系統(tǒng)之內(nèi)得到證明（哥德爾第二不完備性定理）。數(shù)學(xué)真理不可能由包括程序在內(nèi)的任何機(jī)械過程所窮盡，而必然包含直覺和洞察的成份。存在著對于人的直覺來說明顯為真，但無法形式證明的良定義數(shù)學(xué)命題（Godel命題；Goodstein定理等）；存在無限多不可由“機(jī)械過程”計(jì)算的函數(shù)（圖靈）；存在著具有重

15、要實(shí)際意義，但無法被機(jī)械過程解決的判定問題（停機(jī)問題圖靈；丟番圖方程解的存在性問題（希爾伯特第十問題）。27形式化命題邏輯系統(tǒng)Ln注：機(jī)械過程現(xiàn)代數(shù)字計(jì)算機(jī)程序算法圖靈機(jī) 所謂的“機(jī)械過程”，應(yīng)廣義理解，指可實(shí)現(xiàn)的經(jīng)典物理過程。 “機(jī)械過程”涉及到數(shù)學(xué)之外的物理的內(nèi)涵。量子計(jì)算的某些最新理論研究結(jié)果似乎暗示，某種理論上的量子計(jì)算模型似乎可以實(shí)現(xiàn)某些經(jīng)典物理過程無法實(shí)現(xiàn)的計(jì)算任務(wù)（如等價(jià)于停機(jī)問題的丟番圖方程解的存在性判定問題），但是上述結(jié)果尚未形成定論。n思考題：某些人認(rèn)為，形式數(shù)學(xué)系統(tǒng)的不完備性意味著人工智能的不可能性，存在著直覺上為真但形式系統(tǒng)內(nèi)無法證明的真理，說明人心比機(jī)器和程序更優(yōu)越，

16、程序不可能充分模擬人類智能。談?wù)勀銓υ搯栴}的看法。 28思考題：考試佯謬n邏輯課老師在周末放學(xué)時(shí)對學(xué)生說： 條件a：下周要進(jìn)行一次考試； 條件b：到底哪天考試，你們在考試之前的任何一天都不能確知。 注：每周上課5天（周一至周五），每天都上一節(jié)邏輯課 只有在邏輯課時(shí)才可能考試。 一個(gè)聰明的學(xué)生做出了以下推理： 推論一：周五不可能考試，因?yàn)槿绻芤恢林芩亩疾豢?，那么周四下課時(shí)我們就事先知道了明天（周五）一定考試，這不符合條件b。但根據(jù)條件a，下周肯定考試，因此考試時(shí)間只能是周一至周四的某一天，周五可以排除。29思考題：考試佯謬n推論二：周四也不可能考試，因?yàn)槿绻芤恢林苋疾豢?，那么周三放學(xué)時(shí)我們

17、就事先知道了明天考試，這不符合條件b。但根據(jù)條件a，下周肯定考試，因此考試時(shí)間只能是周一至周三的某一天，周四可以排除。 推論三：周三也不可能考試，推理過程同上。 推論四：周二也不可能考試，推理過程同上。 推論五：周一也不可能考試，推理過程同上。 結(jié)論：下周不可能有考試30思考題：考試佯謬n下周的某一天老師突然考試了，這個(gè)聰明同學(xué)感到非常意外。問題究竟出在哪里？n練習(xí)：將推理過程符號(hào)化（不失一般性，考慮簡化問題的版本：每周只有兩次邏輯課，分別在周一和周四。教師在本周四下課時(shí)宣布下周將有一次邏輯考試。）31思考題：考試佯謬n考試佯謬的一個(gè)符號(hào)化表述n命題常元 P: 考試在下周一的邏輯課上舉行 Q:

18、 考試在下周四的邏輯課上舉行 K： 學(xué)生在考試所在的那天之前知道考試的時(shí)間n系統(tǒng)公理： A1： （PQ）（PQ） A2： K A3： PK A4： QK 32思考題：考試佯謬n論證過程：用間接證法證明A1-A4和Q矛盾，推出Q；再用間接證法證明A1-A4和P矛盾，推出P （1）1 Q 附加前提 2（PQ）（PQ） P 3（PQ）（PQ） T (2) 4 PQ T (3) 5 P T (1)(4) 6 PK P 7 K T (5)(6) 8 K P 所以，有Q33思考題：考試佯謬(2) 1 P 附加前提 2（PQ）（PQ） P 3（PQ）（PQ） T (2) 4 PQ T (3) 5 Q T (

19、1)(4) 6 QK P 7 K T (5)(6) 8 K P 所有，有Pn綜合（1）和（2），有PQ34思考題：考試佯謬n兩個(gè)觀察：1 學(xué)生推理的沒有錯(cuò)誤 2 教師的兩個(gè)條件符合事實(shí)，故應(yīng)視為真命題n問題：似乎正確的前提和正確的推理導(dǎo)致了錯(cuò)誤的結(jié)論（即與教師宣稱的真命題矛盾的結(jié)論），為什么？n回答：佯謬之所以出現(xiàn)，是因?yàn)樵噲D將一個(gè)廣義哥德爾型命題（可粗略地理解為涉及系統(tǒng)元知識(shí)的命題）顯式地作為系統(tǒng)公理，來建構(gòu)系統(tǒng)的完備性。不幸的是，一旦這個(gè)原本是直覺真的廣義哥德爾型命題在系統(tǒng)中被作為公理顯式地表達(dá)出來，系統(tǒng)在一致性方面就產(chǎn)生了新的問題。n“There are truths of silenc

20、e, when spoken, no longer true anymore.” Ludwig Wittgenstein35進(jìn)一步的參考書目n較為通俗的讀物： 皇帝新腦，彭羅斯，胡南科技出版社 哥德爾、埃舍爾、巴赫，D. Hofstadter， 商務(wù)印書館n技術(shù)性文章/wiki/G%C3%B6dels_incompleteness_theorems 數(shù)學(xué)家的邏輯36應(yīng)用例子n搜索引擎的查詢擴(kuò)展（查詢結(jié)果的精化）n項(xiàng)目背景：QONTEXT (Quantification of quantum entanglements in contextual IA

21、R and towards a non-Kolmogorovian probability model for contextual IAR), MARIE CURIE ACTIONS, International Joint Research Project of The Council of the European Union (FP7) 37形式化一階謂詞演算系統(tǒng)Kn這里討論一個(gè)形式化的一階謂詞演算系統(tǒng)K。通過對K的形式化研究，回答下列問題： 在一階謂詞邏輯（簡稱為一階邏輯）中，有效推理的含義？ 一階邏輯的有效推理如何完全形式化地執(zhí)行？ 在此基礎(chǔ)上，討論系統(tǒng)K的元性質(zhì)。n形式化一階謂詞

22、演算系統(tǒng)Kn符號(hào)字母表： x1,x2,x3, 客體變元 a1,a2,a3, 客體常元 A11,A12,A21,A22, 謂詞字母，其中Aij表示第j個(gè)i元謂詞 f11,f12,f21,f22, 函數(shù)字母，其中fij表示第j個(gè)i元函數(shù)38形式化一階謂詞演算系統(tǒng) （，），, 輔助技術(shù)性符號(hào) ， 邏輯聯(lián)結(jié)詞 量詞 n注1：引入了函數(shù)符號(hào)（即客體函元）。客體常元、客體變元以及函數(shù)符號(hào)作用于客體常元和變元的結(jié)果可以作為謂詞的項(xiàng) K的項(xiàng)的遞歸定義： 1）客體變元和客體常元是項(xiàng) 2）若fij是函數(shù)符號(hào)， x1,xi 是項(xiàng)，則 fij（x1,xi)是項(xiàng) 3）所有的項(xiàng)通過有限次使用1）和2）生成39形式化一階謂

23、詞演算系統(tǒng)n問題：函數(shù)是一種特殊的關(guān)系，而（多元）謂詞也可以看作關(guān)系。這樣，允許函數(shù)作為謂詞的項(xiàng)，會(huì)不會(huì)破壞形式謂詞演算系統(tǒng)K的一階性？ 例子：任意比x大5的數(shù)大于比x大1的數(shù) (x)G(g5(x),g1(x) (x)(y)(z)(G5（y,x）G1(z,x)G(y,z)40形式化一階謂詞演算系統(tǒng)n注3：K中只有兩個(gè)聯(lián)結(jié)詞，為什么？n注4：K中只有一個(gè)全稱量詞，為什么？n原子公式：形如A(t1, t2, , tn)的公式稱為K的原子公式，其中t1, t2, , tn是K的項(xiàng)n謂詞公式（合式公式）： 1） K的每一原子公式是K的謂詞公式 2） 若A和B是謂詞公式，則（A），（AB）和（xi）A是

24、謂詞公式，這里xi是任意客體變元 3） 只有經(jīng)過有限次應(yīng)用步驟1）2）所獲得的公式才是謂詞公式41形式化一階謂詞演算系統(tǒng)n下面將給出K的公理。但是在此之前，需要澄清一個(gè)問題：K的公理在何種意義上是真的？為了討論謂詞邏輯的真性問題，需要引入解釋的概念。n定義1：K的解釋I是指一個(gè)對象域集合DI、常元的集合SI，DISI上函數(shù)的集合FI和關(guān)系的集合RI。n注：K中的客體變元x1，x2，的具體取值在DI中產(chǎn)生；K中的客體常元在SI上中產(chǎn)生；K中的函數(shù)和謂詞分別由FI和RI產(chǎn)生 K的解釋（以及賦值）類似于L的真值指派，K的謂詞公式的真性需要基于解釋（以及賦值）加以討論。n例子：初等算術(shù)系統(tǒng)42形式化一

25、階謂詞演算系統(tǒng)n例子：(x1)(x3)A21(x1,x3) 當(dāng)DI是正整數(shù)集合，A21(x1,x3)被解釋為x1x30時(shí)？ 當(dāng)DI是整數(shù)集合，A21(x1,x3)被解釋為x1x30時(shí)？n定義2：K的解釋I的一個(gè)賦值是從K的項(xiàng)到DISI的函數(shù)v，滿足： 客體變元取值于DI，客體常元取值于SI 對于K的每個(gè)常元：v(xi)=xi* 對于K的每個(gè)常元：v(ai)=ai* 對于K的任意函數(shù)fij： v(fij(t1,ti)=f*ij(v(t1),v(ti) 這里：xi*,ai* 和f*ij分別是xi,ai和fij在I中的對應(yīng)物43形式化一階謂詞演算系統(tǒng)n注：上述定義保證了任意復(fù)雜函數(shù)的賦值可遞歸確定

26、解釋I的賦值v將由對基本客體常元和變元的賦值，以及函數(shù)的解釋完全確定 賦值起到了進(jìn)一步的真值指派作用，解釋和賦值共同確定了K中所有謂詞公式的真值 注意K的賦值與L的賦值的區(qū)別n例子： A11(x1) 解釋I的DI是整數(shù)集合，A11(x1)被解釋為x1大于0。對于這個(gè)給定的解釋I，當(dāng)賦予x1不同的值時(shí)，上式有不同真值。 A31(f11(x1),x1,a1)A11(x1)44形式化一階謂詞演算系統(tǒng)n定義3：兩個(gè)賦值 u、v是i-等價(jià)的，如果對于任意j不等于i，u(xj)=v(xj)n定義4：設(shè)A、B、C是K的謂詞公式，I是K的一個(gè)解釋。I的賦值v滿足A，如果可由如下四種情形歸納證明v滿足A： 1）

27、v滿足A(t1,ti) A*(v(t1),v(ti)真 2）v滿足B v不滿足B 3）v滿足BC v滿足B或v滿足C 4）v滿足(xi)B 任何i-等價(jià)于v的賦值均滿足Bn注：上述定義保證了賦值v相對于任意謂詞公式的可滿足性可遞歸判定45形式化一階謂詞演算系統(tǒng)n定義4：K的謂詞公式A在解釋I下是真的，如果I中每一賦值均滿足A； K的謂詞公式A在解釋I下是假的，如果I中每一賦值均不滿足An問題：對于特定解釋I： 是否可能存在既不真又不假的謂詞公式？ 是否可能存在既真又假的謂詞公式？n命題1：在K的解釋I下，若AB和A真，則B也真n命題2：在K的解釋I下，A真當(dāng)且僅當(dāng)(xi)A真，xi是任意變元n

28、命題3：在K的解釋I下，A真當(dāng)且僅當(dāng)(x1)(xk)A真，x1xk是任意變元n注：命題2、3意味著對A中的變元增加全稱量詞，不改變其真值46形式化一階謂詞演算系統(tǒng)n定義5：K的謂詞公式A是重言式，如果A是L的重言式在K中的一個(gè)代換實(shí)例n例子：X(YX)代換為(xi)A(xj)B(xi)A)n命題4：K的重言式在K的任意解釋下都是真的（反之未必成立）n定義6：K的謂詞公式A稱為封閉的，如果其中無自由變元n命題5：若A是K的封閉謂詞公式，I是K的解釋，則在I下，或者A為真，或者A為假n注：對于多數(shù)重要的系統(tǒng)，特別是數(shù)學(xué)系統(tǒng)，謂詞公式A通常中并不會(huì)出現(xiàn)自由變元n定義7：K的謂詞公式A是邏輯有效的，如

29、果A在K的每一種解釋下都是真的；A是邏輯無效的，如果A在K的每一種解釋下都是假的。n回顧：真、假、非真非假、滿足、重言、邏輯有效、永假、邏輯無效、解釋、賦值、封閉公式47形式化一階謂詞演算系統(tǒng)n公理：設(shè)A、B和C是任意謂詞公式，則以下為K的公理模式 K1:（A（BA） K2:（A（BC）（AB）（AC） K3:（AB）（BA） K4: (xi)AA),xi不在A中自由出現(xiàn) 注： K4的作用是消除無用的量詞，例如： (xi)(xi)A(xi)是否可以應(yīng)用K4？ (xi)A(xj)是否可以應(yīng)用K4？ (xi)A(f(xj)是否可以應(yīng)用K4？ (xi)A(xi)是否可以應(yīng)用K4？ K5: (xi)A

30、(xi)A(t),t是K的項(xiàng)，它對A(xi)中的xi是自由的48形式化一階謂詞演算系統(tǒng) 定義：設(shè)A是K的任意謂詞公式，項(xiàng)t對A中的xi是自由的，如果xi在A中自由出現(xiàn)，且不在A的任何一個(gè)（xj）的轄域中，這里xj是在t中出現(xiàn)的任意客體變元 注：粗略地說，項(xiàng)t對A中的xi是自由的，意味著t可以對A中的xi的每一自由出現(xiàn)做代入，而不會(huì)引起與A中量詞的相互作用 K5例子:xj對于(xi)A(xi,xj)中的xi是否可用K5？ xj對于(xi)(xj)A(xi,xj)中的xi是否可用K5？ f(xj)對于(xi)A(xi,xj,xk)中的xi是否可用K5？ xi對于(xi)A(xi)中的xi是否可用K

31、5？ xi對于(xi)(xi)A(xi)中的xi是否可用K5？ 49形式化一階謂詞演算系統(tǒng)注：K4和K5用于去除演繹過程中產(chǎn)生的無用的量詞或?qū)崿F(xiàn)特殊化。例如，對于(xi)A這樣的命題，xi可是也可不是A中自由出現(xiàn)的變元。若xi在A中自由出現(xiàn)，可把A記作A（xi），因?yàn)閤i對A(xi)中的xi是自由的，于是由K5可獲得A(xi)。若xi不在A中自由出現(xiàn)，則由K4可獲得AK6: (xi)(AB)（A(xi)B），若A不包含變元xi的自由出現(xiàn)50形式化一階謂詞演算系統(tǒng)n命題6：K的公理模式的所有實(shí)例都是邏輯有效的nK6： (xi)(AB)（A(xi)B），若A不包含變元xi的自由出現(xiàn) 證明：若（A(

32、xi)B）|v = F，即有A|v = T和(xi)B|v = F，則存在一個(gè)與v i-等價(jià)的u，有B|u = F；又因A中不包括xi的自由出現(xiàn)，故有A|u = T； 所以u(píng)不滿足AB 所以u(píng)不滿足(xi)(AB) 所以v不滿足(xi)(AB)51形式化一階謂詞演算系統(tǒng)nK的演繹規(guī)則： 1）分離規(guī)則，即從A和（AB），可以獲得B 2）全稱概括規(guī)則（UG）：由A獲得（xi）An問題：全程概括規(guī)則是合理的嗎？n注：K的公理模式和演繹規(guī)則包括了L的公理模式和演繹規(guī)則，增加的公理和規(guī)則對于涉及量詞的演繹是必要的52形式化一階謂詞演算系統(tǒng)n定義8：K中的一個(gè)證明是謂詞公式的序列A1,A2,An，使得對每

33、一個(gè)Ai（1=i1)的證明，而K的所有長度小于n步的定理都是邏輯有效的。n命題9（K的一致性定理）：K是一致的，即不存在K的謂詞公式A，使得A和A都是K的定理nK的完備性定理(Godel 1930) ：若K的謂詞公式A是邏輯有效的，則A是K的定理54模型和模態(tài)邏輯n系統(tǒng)K要求推理是邏輯有效的，即在任意解釋下是均保真的。此要求使K具備邏輯上的可靠性。但系統(tǒng)的可靠性和能力之間常存在內(nèi)在的沖突。這促使人們重新審視邏輯有效性，嘗試放寬對可靠性的限制以獲得更強(qiáng)有力的系統(tǒng)。n邏輯有效性被定義為對于任何解釋均為真，但通常情況下，并非每個(gè)解釋都令我們感興趣，甚至有些解釋是不可形式定義的（可形式定義的解釋是可數(shù)

34、的，而所有可能的解釋是不可數(shù)的）n例子：若確知日?？臻g可以由歐幾里得幾何精確地刻畫，是否有必要讓應(yīng)用于日?？臻g中的形式系統(tǒng)也適用于黎曼幾何或羅巴切夫斯基幾何世界？ 可否擴(kuò)展K的公理集，保證其具有相對于特定解釋的良好性質(zhì)，并使其功能更強(qiáng)？例如，將歐幾里得幾何的公理和公設(shè)加入系統(tǒng)K。 這就是形式系統(tǒng)的基本思想。55模型和模態(tài)邏輯n定義1：設(shè)X是K的謂詞公式集合，X的一個(gè)解釋（世界）稱為A的模型，如果X中每個(gè)謂詞公式在此解釋下是真的n定義2：若S是一階系統(tǒng)，S的一個(gè)模型是一個(gè)解釋，在這個(gè)解釋中，S的每個(gè)定理都是真的n定理1：設(shè)S是一階系統(tǒng)，I是使S的每個(gè)公理均為真且推理規(guī)則保真的解釋，則I是S的一個(gè)

35、模型n注：定義1給出了公式集的模型的定義；定義2給出了一階系統(tǒng)的模型的定義。由模型的定義可知，任何一個(gè)解釋都是一階謂詞系統(tǒng)K的模型 由定理1，一個(gè)一階系統(tǒng)的解釋，只需使其所有公理真且推理規(guī)則保真，即可成為其模型n思考題：可否建構(gòu)現(xiàn)實(shí)有效系統(tǒng)，即以所有可形式定義解釋為模型的系統(tǒng)？56模型和模態(tài)邏輯n模態(tài)邏輯：關(guān)于可能世界（即解釋）的邏輯n單世界和多世界 我們的世界是所有可能世界中的最完美者萊布尼茨 量子力學(xué)的多宇宙（multiverse）解釋Everettn模態(tài)詞 ：讀作可能，p指命題p在某個(gè)（或某些）解釋中為真，即在某個(gè)（或某些）可能世界中為真 ：讀作必然，p指命題p在所用可能的解釋中均為真，

36、即在所有可能世界中為真。n模態(tài)邏輯對于蘊(yùn)含悖論的解決方案 例子：A(BA)與SP(S:太陽西升, P：有最大的質(zhì)數(shù)) （A(BA)）與（SP） 57模型和模態(tài)邏輯n模態(tài)（命題）邏輯的重言式集合S是古典命題邏輯重言式集合的超集S，S滿足以下條件 1) (pq)(pq)S 2) S在分離規(guī)則下封閉：若AS，ABS ，則BS 3) S在代入規(guī)則下封閉：若AS，則AS，這里A是A的代入特例 4) S在弱必然化規(guī)則下封閉：若A是命題邏輯重言式，則AS 5) S在必然化規(guī)則下封閉：若AS，則ASn注：若一個(gè)模態(tài)邏輯系統(tǒng)滿足1)-4)，則稱它為古典模態(tài)邏輯。 若一個(gè)模態(tài)系統(tǒng)滿足1)-3)和5)，則稱它為正規(guī)

37、模態(tài)邏輯。 是否有必然化規(guī)則（記為N），是正規(guī)系統(tǒng)區(qū)別于非正規(guī)系統(tǒng)的的主要標(biāo)志。N是說：如果一個(gè)公式是在系統(tǒng)內(nèi)是可證的，則它是邏輯必然的。58模型和模態(tài)邏輯n命題模態(tài)邏輯系統(tǒng)的實(shí)例：S5nS5以代入規(guī)則（記為US）和分離規(guī)則（記為MP）作為推理規(guī)則nS5系統(tǒng)公理 M1(A2)：pp M2(T): pp M3(K): (pq)(pq) M4(N)：若A可證，則有A M5(4): pp M6(E): pp， pp (Becker假定） M7(A1)：所有真值函項(xiàng)重言式59模型和模態(tài)邏輯n例子：安瑟倫的上帝存在性本體論證明的Descartes版本 “God could not be so complete if he werent. So he is.” Descartes 擴(kuò)展表述： 定義上帝為具有所有積極屬性者，則上帝必存在 證明：（反證法）假設(shè)上帝不存在，則我們可以設(shè)想一個(gè)God*， God*保有上帝的所有其他積極屬性，除了需要額外設(shè)想God*是存在的。由于存在性是比虛