形式化數(shù)理邏輯.ppt

1,形式化數(shù)理邏輯,侯越先，, 25-B-510 一般性參考： 離散數(shù)學(xué)，左孝凌等，上?？茖W(xué)技術(shù)出版社 數(shù)學(xué)家的邏輯，哈密爾頓，商務(wù)印書館 元數(shù)學(xué)導(dǎo)論， SC克林，科學(xué)出版社 課程輔助材料：,2,重新審視邏輯的本質(zhì),真與邏輯 經(jīng)驗意義上，命題的“真”指命題的斷言符合其所指涉事物的實際狀態(tài) 邏輯（Logics）研究的是有效的推理方法，數(shù)理邏輯（Mathematical Logics）就是用數(shù)學(xué)化（符號化）的手段，研究有效的推理方法,3,重新審視邏輯的本質(zhì),什么是有效推理方法? a 有效推理方法應(yīng)具備保真性，即如果推理前提真，則推理結(jié)論真 b 有效推理方法的保真性應(yīng)具有普遍意義，即不同的人，在不同的應(yīng)用背景下使用相同的推理過程，可獲得真值相同的結(jié)論 有效推理的例子：三段論,4,重新審視邏輯的本質(zhì),兩個基本問題： 問題1：是否所有真命題都可從特定的邏輯前提出發(fā)，由滿足條件a和b的邏輯推理過程獲得？ 問題2：如果推理前提真，有效推理方法的結(jié)論是否無條件地真？,5,重新審視邏輯的本質(zhì),問題1（是否所有真命題都可從特定的推理前提出發(fā)，由滿足條件a和b的邏輯推理過程獲得？） 下面各個推理結(jié)論（藍(lán)色部分）的真值由何決定？ 例1 因為他是醫(yī)生，所以他是大夫 例2 如果下雨，野餐取消； 現(xiàn)在確實下雨了； 野餐將取消 例3 如果A勝過B； 且B勝過C； 則A勝過C 例4 任何一個男同學(xué)都不能斷定本語句是真的,6,重新審視邏輯的本質(zhì),獲致“真”的途徑： 基于邏輯的真（基于形式的真） 基于語義的真 基于直覺的真 注：4與說謊者悖論的區(qū)別 4與哥德爾不完備性定理之間的關(guān)系 數(shù)理邏輯的研究目的：研究形式有效的推理，用形式手段地刻畫人們對形式真的樸素理解。,7,重新審視邏輯的本質(zhì),問題2（如果推理前提真，有效推理方法的結(jié)論是否無條件地真？） 例子（量子物理的雙縫實驗）：電子e通過左縫隙或右縫隙達(dá)到屏幕，且通過縫隙時的動量是p 小練習(xí)：將以上例子用命題邏輯符號化 量子邏輯：刻畫量子世界的命題邏輯 1 G. Birkhoff and J. von Neumann, The Logic of Quantum Mechanics 2 http:/wapedia.mobi/en/Quantum_logic,8,重新審視邏輯的本質(zhì),Remark 1：形式邏輯系統(tǒng)本質(zhì)上是一種形式約定系統(tǒng)，系統(tǒng)內(nèi)的真命題（永真式）只在形式約定的意義下為真，而并不必然對應(yīng)于實際物理狀態(tài)。 Remark 2：只有當(dāng)形式邏輯系統(tǒng)的解釋（即模型）確定之后，才可能討論形式命題（在特定解釋下的）“物理真實性”。一般來說，古典邏輯系統(tǒng)適用于經(jīng)典物理世界，因此在日常情況下，基于古典邏輯系統(tǒng)得出的真命題對應(yīng)于事物的實際狀態(tài)。以下我們約定已給出合適的模型，使得形式真等價于真,9,形式化數(shù)理邏輯的研究目的,1 研究邏輯（形式）有效的推理，用形式手段刻畫人們對邏輯（形式）真的樸素理解 2 研究形式邏輯系統(tǒng)的元性質(zhì)：可靠性、可判定性、完備性等 形式化命題邏輯、形式化謂詞邏輯、形式化非古典邏輯 思考題：是否有可能對基本的形式邏輯系統(tǒng)加以擴張，使其可把握其他類型的真？詳細(xì)說明你的意見,10,形式數(shù)理邏輯的主要研究內(nèi)容,3 擴展研究目的 模型論、證明論、遞歸論、公理化集合論 模型論：用數(shù)理邏輯和集合論的方法解釋、分析形式的（數(shù)學(xué)或物理）概念和系統(tǒng) 證明論：用數(shù)理邏輯的方法研究數(shù)學(xué)證明的過程 遞歸論：研究解決問題的可行的計算方法和計算的復(fù)雜程度,11,形式化命題邏輯系統(tǒng)L,（非形式）命題邏輯系統(tǒng)的能力和局限 命題邏輯系統(tǒng)的結(jié)論都是真的嗎？（考慮命題邏輯中真的定義） 命題邏輯系統(tǒng)的能力是否足夠強，使得我們可由命題邏輯系統(tǒng)（算法地）推出所有的邏輯真命題？ 引入形式化命題邏輯系統(tǒng) 理論方面：澄清命題邏輯系統(tǒng)的元性質(zhì)(一致性、完備性和可判定性等）、澄清基本的數(shù)學(xué)哲學(xué)問題（例如數(shù)學(xué)是否可以形式化） 應(yīng)用方面，形式化邏輯系統(tǒng)在人工智能、軟件工程等領(lǐng)域有著深入的應(yīng)用。 命題邏輯的形式系統(tǒng)L定義如下 1 符號字母表： ，（，），p1，p2，p3， 問題：為何只有兩個邏輯聯(lián)結(jié)詞和？,12,形式化命題邏輯系統(tǒng)L,2 命題公式的集合：如下3條遞歸規(guī)則確定命題公式的集合 （1）對每個i=1，pi是命題公式 （2）若A和B是命題公式，則（A）和（AB）是命題公式 （3）所有命題公式由遞歸應(yīng)用（1）和（2）產(chǎn)生 注：在不引起歧義的情況下，括號可省略 3 公理模式： L1: （A（BA） L2: （A（BC）（AB）（AC） L3: （ A）（B）（BA） 注：A、B和C可以是任意命題公式 顯然，公理L1-L3是永真式,13,形式化命題邏輯系統(tǒng)L,4 演繹規(guī)則（分離規(guī)則，記為MP)：從A和（AB），可以獲得B 定義1：L中的一個證明是命題公式的一個序列A1，A2，An，使得對每個i（1=i=n)，Ai或者是L的公理，或者是由序列中在前面的兩項利用演繹規(guī)則得到的 注：L中的公理當(dāng)然也是L中的定理，它們在L中的證明是其自身 例子：如下序列是L中的證明 （1）（p1（p2p1） L1 （2）（p1（p2p1）（p1p2）（p1p1） L2 （3）（p1p2）（p1p1） （1），（2），MP,14,形式化命題邏輯系統(tǒng)L,例子：在L中求證QR是P，Q（PR）的邏輯結(jié)論 證明：P P Q（PR） P P（QP） L1 QP (1),(3) MP (Q（PR）)(QP)（QR） L2 (QP)（QR） (2),(5) MP （QR） (4),(6) MP,15,形式化命題邏輯系統(tǒng)L,對于系統(tǒng)L，我們關(guān)心如下一些問題：是否L的每個定理都是重言式；基于L的推演是否可能導(dǎo)致矛盾：即命題公式A和 A是否可能同時被L證明為定理；以及L是否可以證明所有重言式 定義2（可靠性定義）：若L的任意定理都是重言式，則稱L是可靠的 定義3（一致性定義）:若L的任意互為否定的命題公式A和A不同時為L的定理，則稱L是一致的 定義4（完備性定義）：若L中的任意重言式都是L的定理，則稱L是完備的 定義5（可判定性定義）：若存在一個通用的算法，判定任意命題公式是否是L的定理，則稱L是可判定的 問題：以上幾個元性質(zhì)之間的關(guān)系？,16,形式化命題邏輯系統(tǒng)L,定理1（可靠性定理）：L是可靠的 證明：（數(shù)學(xué)歸納法）設(shè)A是L的定理，施歸納于A的證明序列中所含命題公式的個數(shù)n。 當(dāng)n1時，A的證明序列只包含一個命題公式，A是L的公理，即A是重言式 當(dāng)n1時，假設(shè)L中證明序列長度小于n的定理都是重言式（歸納假設(shè)）。由于定理A在L中存在一個證明，則A或者是L的公理，或者由MP規(guī)則獲得。當(dāng)A是L的公理時，A顯然是重言式。當(dāng)A是由MP規(guī)則獲得時，其證明序列中必存在兩個命題公式，不失一般性，記為B和BA。由于B和BA的證明序列長度小于n，由歸納假設(shè)，它們是重言式。這樣A必然是重言式。 綜上，L是可靠的。,17,形式化命題邏輯系統(tǒng)L,定理2（一致性定理）：L是一致的 證明：反證法，若L是不一致的，則存在命題公式A，使得A和A均為L的定理。由L的可靠性定理，L的定理必是重言式，矛盾。 定理3（完備性定理）：L是完備的,18,定理4證明概要（數(shù)學(xué)家的邏輯）,引理1: (AA)是L的定理 證明: 1) (A(AA)A) L1 2) (A(AA)A) (A(AA)(AA) L2 3) (A(AA)(AA) MP 4) (A(AA) L1 5) (AA) MP,19,定理4證明概要（數(shù)學(xué)家的邏輯）,定義6：L* 稱為L的擴張，如果L*是通過改變或擴大L的公理集合而得到的一個形式系統(tǒng)，使得L的所有定理仍是L*的定理。 問題：增加L的公理，是否必然增加L的定理？是否可能采用完全不同的公理集，但導(dǎo)出完全相同的定理集？ 注：若L*是通過在L中增加公理集合X獲得的，則L*可記為L+X； 注：以下兩個說法是等價的 1)命題公式A在L+X中可證 2)命題公式A可在L中由前提X推演（證明）出 3)可記為X|-A 或 |-A L L+X,20,定理4證明概要（數(shù)學(xué)家的邏輯）,定義7：L的擴張L*是一致的，如果不存在命題公式A，使得A和A均為L*的定理 演繹定理：若B是在L+X中增加公理A后形成的擴張系統(tǒng)的定理，則(AB)是L+X的定理 證明：數(shù)學(xué)歸納法并利用引理1的結(jié)果 注：逆定理成立 推論：對于任意的A、B和C，在L中可由(AB)和(BC)證得(AC) 證明：在L+(AB),(BC),A中易證C，由演繹定理， L+(AB),(BC)中可證(AC) 注：此推論可進(jìn)一步擴展；此推論在邏輯推演中的使用稱為HS規(guī)則,21,定理4證明概要（數(shù)學(xué)家的邏輯）,引理2：A（AB）和(AA)A是L的定理 一致性判定：由引理2，L的一個擴張L*是一致的，當(dāng)且僅當(dāng)存在一個命題公式A，A不是L*的定理 引理3：設(shè)L*是L的一致擴張，又A是L的命題公式，且A不是L*的定理，那么由L*增加A而得到的擴張L*也是一致的 證明：反證法，利用演繹定理和引理2的兩個定理。 定義8：L的一致擴張是完全的，如果對于任意A，A或A是此擴張的定理 注：注意這里的“完全”與前面提到的完備性之間的區(qū)別 引理4：設(shè)L*是L的一致擴張，則存在L*的一致完全擴張,22,定理4證明概要（數(shù)學(xué)家的邏輯）,定義9：L的一個賦值是一個函數(shù)v，它的定義域是L的命題公式集合，它的值域是T,F，使得對L的任意命題公式A和B，有 1) v(A) v(A) 2) v(AB) = F iff v(A)=T 且 v(B)=F 注：對L的命題符號p1,p2,的真值指派與L的賦值之間存在一一對應(yīng)關(guān)系。一個真值指派可決定一個賦值；反之，合法的賦值對應(yīng)著一個真值指派。 引理5：若L*是L的一致擴張，則存在一個賦值，使得L*中的所有定理取值T 證明：賦值由L*的完全一致擴張J給出。只需證此賦值滿足定義9中的1)和2)即可,23,定理4證明概要（數(shù)學(xué)家的邏輯）,定理：L是完備的（L的完備性定理） 證明：反證法，假設(shè)L不完備，則可在L的公理集中增加了某個永真式Ak的否定，形成一致擴張L*。由引理5，存在賦值v使得L*中所有定理為真，則Ak在此賦值下也為真。這意味著永假式Ak在某個真值指派下為真，矛盾,24,形式化命題邏輯系統(tǒng)L,定理4（可判定性定理）：L是可判定的。 證明：真值表法。 問題：真值表法能否作為一般方法在實際自動推理系統(tǒng)中應(yīng)用？ 總結(jié)：L具有我們所期望的性質(zhì)（可靠性、一致性、完備性等） 問題：是否可能存在其他的形式命題邏輯系統(tǒng)（不同的聯(lián)結(jié)詞、不同的公理），也具有L的性質(zhì)？ 思考題（作業(yè)）：構(gòu)造一個使用邏輯聯(lián)結(jié)詞、和的形式命題邏輯系統(tǒng)：說明你構(gòu)造的系統(tǒng)公理和推演規(guī)則；證明其具有L的性質(zhì)（可靠性、一致性、可判定性和完備性）。,25,形式化命題邏輯系統(tǒng)L,思考題：既然利用形式命題邏輯系統(tǒng)可以中肯把握（命題的）邏輯真，可否擴展的形式命題邏輯系統(tǒng)，以中肯地把握特定意義下的數(shù)學(xué)真（Hilbert方案）？例如，構(gòu)造形式化數(shù)論系統(tǒng)。這樣的系統(tǒng)是否也具有系統(tǒng)L的良好性質(zhì)？ 思考題：如果上一個問題的回答是肯定的，這樣的數(shù)學(xué)系統(tǒng)的全部內(nèi)涵即可由形式系統(tǒng)囊括，至少在原則上，我們可以編寫一個計算機程序，利用簡單地窮盡搜索，逐步獲得一個又一個定理，數(shù)學(xué)發(fā)現(xiàn)的過程可以還原為計算機程序操作，這個思路是否可行？,26,形式化命題邏輯系統(tǒng)L,線索：這樣的前景不會發(fā)生。絕大多數(shù)實際數(shù)學(xué)系統(tǒng)的形式化是不完備的（哥德爾第一不完備性定理），甚至其一致性也無法在系統(tǒng)之內(nèi)得到證明（哥德爾第二不完備性定理）。數(shù)學(xué)真理不可能由包括程序在內(nèi)的任何機械過程所窮盡，而必然包含直覺和洞察的成份。存在著對于人的直覺來說明顯為真，但無法形式證明的良定義數(shù)學(xué)命題（Godel命題；Goodstein定理等）；存在無限多不可由“機械過程”計算的函數(shù)（圖靈）；存在著具有重要實際意義，但無法被機械過程解決的判定問題（停機問題圖靈；丟番圖方程解的存在性問題（希爾伯特第十問題）。,27,形式化命題邏輯系統(tǒng)L,注：機械過程現(xiàn)代數(shù)字計算機程序算法圖靈機 所謂的“機械過程”，應(yīng)廣義理解，指可實現(xiàn)的經(jīng)典物理過程。 “機械過程”涉及到數(shù)學(xué)之外的物理的內(nèi)涵。量子計算的某些最新理論研究結(jié)果似乎暗示，某種理論上的量子計算模型似乎可以實現(xiàn)某些經(jīng)典物理過程無法實現(xiàn)的計算任務(wù)（如等價于停機問題的丟番圖方程解的存在性判定問題），但是上述結(jié)果尚未形成定論。 思考題：某些人認(rèn)為，形式數(shù)學(xué)系統(tǒng)的不完備性意味著人工智能的不可能性，存在著直覺上為真但形式系統(tǒng)內(nèi)無法證明的真理，說明人心比機器和程序更優(yōu)越，程序不可能充分模擬人類智能。談?wù)勀銓υ搯栴}的看法。,28,思考題：考試佯謬,邏輯課老師在周末放學(xué)時對學(xué)生說： 條件a：下周要進(jìn)行一次考試； 條件b：到底哪天考試，你們在考試之前的任何一天都不能確知。 注：每周上課5天（周一至周五），每天都上一節(jié)邏輯課 只有在邏輯課時才可能考試。 一個聰明的學(xué)生做出了以下推理： 推論一：周五不可能考試，因為如果周一至周四都不考，那么周四下課時我們就事先知道了明天（周五）一定考試，這不符合條件b。但根據(jù)條件a，下周肯定考試，因此考試時間只能是周一至周四的某一天，周五可以排除。,29,思考題：考試佯謬,推論二：周四也不可能考試，因為如果周一至周三都不考，那么周三放學(xué)時我們就事先知道了明天考試，這不符合條件b。但根據(jù)條件a，下周肯定考試，因此考試時間只能是周一至周三的某一天，周四可以排除。 推論三：周三也不可能考試，推理過程同上。 推論四：周二也不可能考試，推理過程同上。 推論五：周一也不可能考試，推理過程同上。 結(jié)論：下周不可能有考試,30,思考題：考試佯謬,下周的某一天老師突然考試了，這個聰明同學(xué)感到非常意外。問題究竟出在哪里？ 練習(xí)：將推理過程符號化（不失一般性，考慮簡化問題的版本：每周只有兩次邏輯課，分別在周一和周四。教師在本周四下課時宣布下周將有一次邏輯考試。）,31,思考題：考試佯謬,考試佯謬的一個符號化表述 命題常元 P: 考試在下周一的邏輯課上舉行 Q: 考試在下周四的邏輯課上舉行 K： 學(xué)生在考試所在的那天之前知道考試的時間 系統(tǒng)公理： A1： （PQ）（PQ） A2： K A3： PK A4： QK,32,思考題：考試佯謬,論證過程：用間接證法證明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 所以，有Q,33,思考題：考試佯謬,(2) 1 P 附加前提 2（PQ）（PQ） P 3（PQ）（PQ） T (2) 4 PQ T (3) 5 Q T (1)(4) 6 QK P 7 K T (5)(6) 8 K P 所有，有P 綜合（1）和（2），有PQ,34,思考題：考試佯謬,兩個觀察：1 學(xué)生推理的沒有錯誤 2 教師的兩個條件符合事實，故應(yīng)視為真命題 問題：似乎正確的前提和正確的推理導(dǎo)致了錯誤的結(jié)論（即與教師宣稱的真命題矛盾的結(jié)論），為什么？ 回答：佯謬之所以出現(xiàn)，是因為試圖將一個廣義哥德爾型命題（可粗略地理解為涉及系統(tǒng)元知識的命題）顯式地作為系統(tǒng)公理，來建構(gòu)系統(tǒng)的完備性。不幸的是，一旦這個原本是直覺真的廣義哥德爾型命題在系統(tǒng)中被作為公理顯式地表達(dá)出來，系統(tǒng)在一致性方面就產(chǎn)生了新的問題。 “There are truths of silence, when spoken, no longer true anymore.” Ludwig Wittgenstein,35,進(jìn)一步的參考書目,較為通俗的讀物： 皇帝新腦，彭羅斯，胡南科技出版社 哥德爾、埃舍爾、巴赫，D. Hofstadter， 商務(wù)印書館 技術(shù)性文章/wiki/G%C3%B6dels_incompleteness_theorems 數(shù)學(xué)家的邏輯,36,應(yīng)用例子,搜索引擎的查詢擴展（查詢結(jié)果的精化） 項目背景：QONTEXT (Quantification of quantum entanglements in contextual IAR 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)K,這里討論一個形式化的一階謂詞演算系統(tǒng)K。通過對K的形式化研究，回答下列問題： 在一階謂詞邏輯（簡稱為一階邏輯）中，有效推理的含義？ 一階邏輯的有效推理如何完全形式化地執(zhí)行？ 在此基礎(chǔ)上，討論系統(tǒng)K的元性質(zhì)。 形式化一階謂詞演算系統(tǒng)K 符號字母表： x1,x2,x3, 客體變元 a1,a2,a3, 客體常元 A11,A12,A21,A22, 謂詞字母，其中Aij表示第j個i元謂詞 f11,f12,f21,f22, 函數(shù)字母，其中fij表示第j個i元函數(shù),38,形式化一階謂詞演算系統(tǒng),（，），, 輔助技術(shù)性符號 ， 邏輯聯(lián)結(jié)詞 量詞 注1：引入了函數(shù)符號（即客體函元）。客體常元、客體變元以及函數(shù)符號作用于客體常元和變元的結(jié)果可以作為謂詞的項 K的項的遞歸定義： 1）客體變元和客體常元是項 2）若fij是函數(shù)符號， x1,xi 是項，則 fij（x1,xi)是項 3）所有的項通過有限次使用1）和2）生成,39,形式化一階謂詞演算系統(tǒng),問題：函數(shù)是一種特殊的關(guān)系，而（多元）謂詞也可以看作關(guān)系。這樣，允許函數(shù)作為謂詞的項，會不會破壞形式謂詞演算系統(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),注3：K中只有兩個聯(lián)結(jié)詞，為什么？ 注4：K中只有一個全稱量詞，為什么？ 原子公式：形如A(t1, t2, , tn)的公式稱為K的原子公式，其中t1, t2, , tn是K的項 謂詞公式（合式公式）： 1） K的每一原子公式是K的謂詞公式 2） 若A和B是謂詞公式，則（A），（AB）和（xi）A是謂詞公式，這里xi是任意客體變元 3） 只有經(jīng)過有限次應(yīng)用步驟1）2）所獲得的公式才是謂詞公式,41,形式化一階謂詞演算系統(tǒng),下面將給出K的公理。但是在此之前，需要澄清一個問題：K的公理在何種意義上是真的？為了討論謂詞邏輯的真性問題，需要引入解釋的概念。 定義1：K的解釋I是指一個對象域集合DI、常元的集合SI，DISI上函數(shù)的集合FI和關(guān)系的集合RI。 注：K中的客體變元x1，x2，的具體取值在DI中產(chǎn)生；K中的客體常元在SI上中產(chǎn)生；K中的函數(shù)和謂詞分別由FI和RI產(chǎn)生 K的解釋（以及賦值）類似于L的真值指派，K的謂詞公式的真性需要基于解釋（以及賦值）加以討論。 例子：初等算術(shù)系統(tǒng),42,形式化一階謂詞演算系統(tǒng),例子：(x1)(x3)A21(x1,x3) 當(dāng)DI是正整數(shù)集合，A21(x1,x3)被解釋為x1x30時？ 當(dāng)DI是整數(shù)集合，A21(x1,x3)被解釋為x1x30時？ 定義2：K的解釋I的一個賦值是從K的項到DISI的函數(shù)v，滿足： 客體變元取值于DI，客體常元取值于SI 對于K的每個常元：v(xi)=xi* 對于K的每個常元：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),注：上述定義保證了任意復(fù)雜函數(shù)的賦值可遞歸確定 解釋I的賦值v將由對基本客體常元和變元的賦值，以及函數(shù)的解釋完全確定 賦值起到了進(jìn)一步的真值指派作用，解釋和賦值共同確定了K中所有謂詞公式的真值 注意K的賦值與L的賦值的區(qū)別 例子： A11(x1) 解釋I的DI是整數(shù)集合，A11(x1)被解釋為x1大于0。對于這個給定的解釋I，當(dāng)賦予x1不同的值時，上式有不同真值。 A31(f11(x1),x1,a1)A11(x1),44,形式化一階謂詞演算系統(tǒng),定義3：兩個賦值 u、v是i-等價的，如果對于任意j不等于i，u(xj)=v(xj) 定義4：設(shè)A、B、C是K的謂詞公式，I是K的一個解釋。I的賦值v滿足A，如果可由如下四種情形歸納證明v滿足A： 1）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-等價于v的賦值均滿足B 注：上述定義保證了賦值v相對于任意謂詞公式的可滿足性可遞歸判定,45,形式化一階謂詞演算系統(tǒng),定義4：K的謂詞公式A在解釋I下是真的，如果I中每一賦值均滿足A； K的謂詞公式A在解釋I下是假的，如果I中每一賦值均不滿足A 問題：對于特定解釋I： 是否可能存在既不真又不假的謂詞公式？ 是否可能存在既真又假的謂詞公式？ 命題1：在K的解釋I下，若AB和A真，則B也真 命題2：在K的解釋I下，A真當(dāng)且僅當(dāng)(xi)A真，xi是任意變元 命題3：在K的解釋I下，A真當(dāng)且僅當(dāng)(x1)(xk)A真，x1xk是任意變元 注：命題2、3意味著對A中的變元增加全稱量詞，不改變其真值,46,形式化一階謂詞演算系統(tǒng),定義5：K的謂詞公式A是重言式，如果A是L的重言式在K中的一個代換實例 例子：X(YX)代換為(xi)A(xj)B(xi)A) 命題4：K的重言式在K的任意解釋下都是真的（反之未必成立） 定義6：K的謂詞公式A稱為封閉的，如果其中無自由變元 命題5：若A是K的封閉謂詞公式，I是K的解釋，則在I下，或者A為真，或者A為假 注：對于多數(shù)重要的系統(tǒng)，特別是數(shù)學(xué)系統(tǒng)，謂詞公式A通常中并不會出現(xiàn)自由變元 定義7：K的謂詞公式A是邏輯有效的，如果A在K的每一種解釋下都是真的；A是邏輯無效的，如果A在K的每一種解釋下都是假的。 回顧：真、假、非真非假、滿足、重言、邏輯有效、永假、邏輯無效、解釋、賦值、封閉公式,47,形式化一階謂詞演算系統(tǒng),公理：設(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(xi)A(t),t是K的項，它對A(xi)中的xi是自由的,48,形式化一階謂詞演算系統(tǒng),定義：設(shè)A是K的任意謂詞公式，項t對A中的xi是自由的，如果xi在A中自由出現(xiàn)，且不在A的任何一個（xj）的轄域中，這里xj是在t中出現(xiàn)的任意客體變元 注：粗略地說，項t對A中的xi是自由的，意味著t可以對A中的xi的每一自由出現(xiàn)做代入，而不會引起與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是否可用K5？ 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），因 為xi對A(xi)中的xi是自由的，于是由K5可獲得A(xi)。若xi 不在A中自由出現(xiàn)，則由K4可獲得A K6: (xi)(AB)（A(xi)B），若A不包含變元xi的自由出現(xiàn),50,形式化一階謂詞演算系統(tǒng),命題6：K的公理模式的所有實例都是邏輯有效的 K6： (xi)(AB)（A(xi)B），若A不包含變元xi的自由出現(xiàn) 證明：若（A(xi)B）|v = F，即有A|v = T 和(xi)B|v = F，則存在一個與v i-等價的u，有 B|u = F；又因A中不包括xi的自由出現(xiàn)，故有 A|u = T； 所以u不滿足AB 所以u不滿足(xi)(AB) 所以v不滿足(xi)(AB),51,形式化一階謂詞演算系統(tǒng),K的演繹規(guī)則： 1）分離規(guī)則，即從A和（AB），可以獲得B 2）全稱概括規(guī)則（UG）：由A獲得（xi）A 問題：全程概括規(guī)則是合理的嗎？ 注：K的公理模式和演繹規(guī)則包括了L的公理模式和演繹規(guī)則，增加的公理和規(guī)則對于涉及量詞的演繹是必要的,52,形式化一階謂詞演算系統(tǒng),定義8：K中的一個證明是謂詞公式的序列A1,A2,An，使得對每一個Ai（1=i=n)，或者Ai是K的公理，或者Ai是由序列中在前面的謂詞公式用分離規(guī)則或全稱概括規(guī)則推出的。K的定理是某個證明序列中的最后一項。 命題7：若K的謂詞公式A是重言式，則A是K的定理 注：逆命題不成立 在K中，邏輯有效的概念相當(dāng)于L中永真的概念。我們關(guān)注于系統(tǒng)K基于邏輯有效性的可靠性、一致性和完備性,53,形式化一階謂詞演算系統(tǒng),命題8（K的可靠性定理）：若K的謂詞公式A是K的定理，則A是邏輯有效的 證明：歸納法，施歸納于定理A的證明序列長度n 奠基步：當(dāng)n1時，A是K的公理，命題成立 歸納步：假設(shè)A有長度為n(n1)的證明，而K的所有長度小于n步的定理都是邏輯有效的。 命題9（K的一致性定理）：K是一致的，即不存在K的謂詞公式A，使得A和A都是K的定理 K的完備性定理(Godel 1930) ：若K的謂詞公式A是邏輯有效的，則A是K的定理,54,模型和模態(tài)邏輯,系統(tǒng)K要求推理是邏輯有效的，即在任意解釋下是均保真的。此要求使K具備邏輯上的可靠性。但系統(tǒng)的可靠性和能力之間常存在內(nèi)在的沖突。這促使人們重新審視邏輯有效性，嘗試放寬對可靠性的限制以獲得更強有力的系統(tǒng)。 邏輯有效性被定義為對于任何解釋均為真，但通常情況下，并非每個解釋都令我們感興趣，甚至有些解釋是不可形式定義的（可形式定義的解釋是可數(shù)的，而所有可能的解釋是不可數(shù)的） 例子：若確知日常空間可以由歐幾里得幾何精確地刻畫，是否有必要讓應(yīng)用于日?？臻g中的形式系統(tǒng)也適用于黎曼幾何或羅巴切夫斯基幾何世界？ 可否擴展K的公理集，保證其具有相對于特定解釋的良好性質(zhì)，并使其功能更強？例如，將歐幾里得幾何的公理和公設(shè)加入系統(tǒng)K。 這就是形式系統(tǒng)的基本思想。,55,模型和模態(tài)邏輯,定義1：設(shè)X是K的謂詞公式集合，X的一個解釋（世界）稱為A的模型，如果X中每個謂詞公式在此解釋下是真的 定義2：若S是一階系統(tǒng)，S的一個模型是一個解釋，在這個解釋中，S的每個定理都是真的 定理1：設(shè)S是一階系統(tǒng)，I是使S的每個公理均為真且推理規(guī)則保真的解釋，則I是S的一個模型 注：定義1給出了公式集的模型的定義；定義2給出了一階系統(tǒng)的模型的定義。由模型的定義可知，任何一個解釋都是一階謂詞系統(tǒng)K的模型 由定理1，一個一階系統(tǒng)的解釋，只需使其所有公理真且推理規(guī)則保真，即可成為其模型 思考題：可否建構(gòu)現(xiàn)實有效系統(tǒng)，即以所有可形式定義解釋為模型的系統(tǒng)？,56,模型和模態(tài)邏輯,模態(tài)邏輯：關(guān)于可能世界（即解釋）的邏輯 單世界和多世界 我們的世界是所有可能世界中的最完美者萊布尼茨 量子力學(xué)的多宇宙（multiverse）解釋Everett 模態(tài)詞 ：讀作可能，p指命題p在某個（或某些）解釋中為真，即在某個（或某些）可能世界中為真 ：讀作必然，p指命題p在所用可能的解釋中均為真，即在所有可能世界中為真。 模態(tài)邏輯對于蘊含悖論的解決方案 例子：A(BA)與SP(S:太陽西升, P：有最大的質(zhì)數(shù)) （A(BA)）與（SP）,57,模型和模態(tài)邏輯,模態(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，則AS 注：若一個模態(tài)邏輯系統(tǒng)滿足1)-4)，則稱它為古典模態(tài)邏輯。 若一個模態(tài)系統(tǒng)滿足1)-3)和5)，則稱它為正規(guī)模態(tài)邏輯。 是否有必然化規(guī)則（記為N），是正規(guī)系統(tǒng)區(qū)別于非正規(guī)系統(tǒng)的的主要標(biāo)志。N是說：如果一個公式是在系統(tǒng)內(nèi)是可證的，則它是邏輯必然的。,58,模型和模態(tài)邏輯,命題模態(tài)邏輯系統(tǒng)的實例：S5 S5以代入規(guī)則（記為US）和分離規(guī)則（記為MP）作為推理規(guī)則 S5系統(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)：所有真值函項重言式,59,模型和模態(tài)邏輯,例子：安瑟倫的上帝存在性本體論證明的Descartes版本 “God could not be so complete if he werent. So he is.” Descartes 擴展表述： 定