高級數(shù)理邏輯第11講全解

1、總復(fù)習(xí)本章對高級數(shù)理邏輯所講述的內(nèi)容總結(jié)， 并對已經(jīng)學(xué)習(xí)的內(nèi)容進(jìn)行回顧。 在對所講述的 內(nèi)容回顧之前，首先對整個數(shù)理邏輯學(xué)科的組成進(jìn)行回顧，從而使大家有更深刻的認(rèn)識。數(shù)理邏輯學(xué)科學(xué)科發(fā)展從數(shù)理邏輯學(xué)中衍生出來的學(xué)科有很多，如：遞歸論、可計算理論、模型論、機(jī)器證明、知 識工程、布爾代數(shù)等。這些理論都是以數(shù)理邏輯學(xué)為基礎(chǔ)的。 針對數(shù)理邏輯本身， 由于這些 學(xué)科的需求產(chǎn)生了很多不同種類的邏輯系統(tǒng)。數(shù)理邏輯的不同種類， 基本上都是從經(jīng)典的邏輯系統(tǒng)中擴(kuò)展而來的。 這種擴(kuò)展通常有語 法擴(kuò)展和語義擴(kuò)展。語法擴(kuò)展： 在經(jīng)典邏輯系統(tǒng)中， 擴(kuò)充一些符號，從而衍生出新的邏輯系統(tǒng)。 如模態(tài) 邏輯，二階謂詞邏輯等。語義

2、擴(kuò)展：對邏輯系統(tǒng)中語義的范圍等進(jìn)行擴(kuò)展，如模糊邏輯等。 數(shù)理邏輯通常劃分成以下不同種類的邏輯系統(tǒng)：1、經(jīng)典邏輯：傳統(tǒng)的命題邏輯、一階謂詞邏輯等。認(rèn)為世界是黑白的，對于一個命題 非真既假。2、模態(tài)邏輯：認(rèn)為世界上任何事情的真假是與時間有著密切的關(guān)系的。3、多值邏輯：認(rèn)為世界上的對與錯是沒有絕對的，命題的真假是可以是多個甚至連續(xù) 值的。4、非單調(diào)邏輯：討論如何將人類的常識加入到邏輯系統(tǒng)中去。經(jīng)典邏輯是單調(diào)邏輯， 既事實越多，已有的結(jié)論不會消失；而單調(diào)邏輯中，可能隨著事實的增加原有的結(jié) 論被否定。體系構(gòu)成在高級數(shù)理邏輯 （計算邏輯）中，每一種邏輯都自成體系。邏輯的體系過程主要包括以 下幾個方面：1、

3、形式系統(tǒng)：用符號的方式來描述一個邏輯系統(tǒng)的構(gòu)成。類似于形式語言系統(tǒng)。2、語義系統(tǒng)：針對形式進(jìn)行解釋的一套體系，這套體系確定了符號的含義的解釋方法 和規(guī)則。3、元理論：對形式系統(tǒng)組成、語義系統(tǒng)特性和形式與語義之間關(guān)系進(jìn)行研究。從而保 證了數(shù)理邏輯的初衷（利用數(shù)學(xué)演算的方法來研究人類思維過程） 。4、自動化推理：在形式系統(tǒng)的基礎(chǔ)上，研究利用計算機(jī)自動進(jìn)行推理的理論和方法。 以及自動推理的效率提高方法和自動推理完備性研究。形式系統(tǒng)形式系統(tǒng)構(gòu)成形式系統(tǒng)由 , TERM, FORMULA, AXIOM, RULE 等 5個部分構(gòu)成，其中 稱為符號 表， TERM 為項集； FORUMULA 為公式集；

4、AIXIOM 為公理集； RULE 為推理規(guī)則集。 ：1、符號表為非空集合，其元素稱為符號。2、設(shè) * 為上全體字的組合構(gòu)成的集合。 項集 TERM 為 * 的子集， 其元素稱為項； 項集 TERM 有子集 VARIABLE 稱為變量集合，其元素稱為變量。3、設(shè) * 為上全體字的組合構(gòu)成的集合。公式結(jié)FORMULA 為 * 的子集，其元素稱為公式；公式集有子集 ATOM ，其元素稱為原子公式。4、公理集 AXIOM 是公式集 FROMULA 的子集，其元素稱為公理。5、推 理 規(guī) 則 集 RULE 是 公 式 集 FORMULA 上 的 n 元 關(guān) 系 集 合 ， 即nRULE= r | n（

5、n是正整數(shù) n 2 r FORMULA n） ，其元素稱為形式系統(tǒng)的 推理規(guī)則。其中公式集和項集之間沒有交叉， 即 TERM FORMULA = ，公式和項統(tǒng)稱為表達(dá)式。由定義可知，符號表、項集TERM 、公式集 FORMULA 是形式系統(tǒng)的語言部分。而 公理集 AXIOM 、推理規(guī)則集 RULE 為推理部分。形式系統(tǒng)的重要問題1、符號表 為非空、可數(shù)集合（有窮、無窮都可以） 。2、項集 TERM 、公式集 FORMULA 、公理集 AXIOM 和推理規(guī)則集 RULE 是遞歸集合， 即必須存在一個算法能夠判定給定符號串是否屬于集合。3、形式系統(tǒng)中的項是用來描述研究的對象，或者稱為客觀世界的。而

6、公式是用來描述 這些研究對象的性質(zhì)的。這個語言被稱為對象語言。定義公式和項產(chǎn)生方法的規(guī)則 稱為詞法。4、用來描述形式系統(tǒng)中各個部分性質(zhì)的語言稱為元語言。用于研究形式系統(tǒng)的元語言又被稱為元數(shù)學(xué)。形式推導(dǎo)1、基本概念演繹結(jié)果與定理 ：設(shè) A為FSPC上一公式， 集合 為 FSPC上一公式集合。 稱A 為 的 演繹結(jié)果，記為 A ，如果存在一個公式序列：A1,A2,A3, ,AL( A) 使得 Ai 或者為形式系統(tǒng) FSPC 的公理，或者為公式集合 中的元素，或者或者為Aj1,Aj2,Aj3, ,Ajn 1（j1,j2, j3, , jn 1 i ）由推理規(guī)則 r得到；則稱 A 為 FSPC的演 繹

7、結(jié)果。當(dāng) 時，稱 A 為定理 FSPC上的定理。稱 A1,A2,A3, ,AL（ A）為 A 的 證明序列。邏輯等價： 公式 A 和 B 分別為兩個公式，如果 A,B 滿足 B A，且 AB 同時成立，則 稱公式 A和 B為邏輯等價公式，記為 A B。即 A,B互為演繹結(jié)果。例如： A| A， A B| B A， A B | B A。對偶：設(shè) A 為 FSPC 上由聯(lián)結(jié)詞 , , 和原子公式構(gòu)成的公式。 在 A 中交換 和 ， 以及原子公式和他的否定公式，得到公式A' ，則稱 A' 為 A 的對偶。2、推理基礎(chǔ)（1）公理代入原理：設(shè) A（P）為含有變元 P 的公理（定理同樣適用

8、） ，如果將公式 A 中 的變元 P替換為命題變元 B，則 A（B）仍為公理（定理） ；C （B C） C）（2）等價替換原理：設(shè)命題公式 A 含有子公式 C（C 為命題公式） ，如果 C D，那 么將 A 中子公式 C提換為命題公式 D（不一定全部） ，所得公式 B滿足 AB。（3）對偶原理：設(shè) A 為 FSPC上的公式， A' 為其對偶，則 A A'。（4）演繹定理：設(shè) 為任一公式集合 , A,B 為任意公式 ,那么：，A B 當(dāng)且僅當(dāng) A B，A B 當(dāng)且僅當(dāng) A B（5）（變量 ） 改名原理如果公式 A 中至少一個量詞的指導(dǎo)變元和相應(yīng)的約束變元都改名為另一個相同變 元后

9、得到公式 A '，則 A '為 A 的改名式；如果 A '是 A 的改名式，且 A '改用的變元在 A 中無任何出現(xiàn)，那 A A'3、其他推理方法 根據(jù)形式系統(tǒng)的性質(zhì)，給出一些專用推理規(guī)則。語義系統(tǒng)語義系統(tǒng)定義形式語義：設(shè) FS 是已經(jīng)存在的形式系統(tǒng)， FS的語義有語義結(jié)構(gòu)和賦值兩個部分組成：a）語義結(jié)構(gòu)： 當(dāng) FS 的項集 TERM 不為空時，由非空集合 U 和規(guī)則組 I 所組成二 元組（ U，I），稱為形式系統(tǒng) FS的語義結(jié)構(gòu)。其中 U和 I的性質(zhì)如下：i. U 為非空集合，稱為論域或者個體域；ii. 規(guī)則組 I，稱為解釋，根據(jù)規(guī)則組的規(guī)定對項集TE

10、RM 中的成員指稱到 U中的個體；規(guī)定對原子公式如何指稱到 U 中的個體性質(zhì)（ U 的子集）、關(guān) 系（ U n 的子集）。b）指派： 若形式系統(tǒng) FS中的變量集合 Variables 非空，那么下列映射稱為指派： s： varibles >U。對于給定的語義結(jié)構(gòu)，可以將指派擴(kuò)展到項集TERM 上：s ：TERM >U ；s S（t）當(dāng) t 為變元S 指派 t 中變元由解釋確定當(dāng) t 為非變元c）賦值：是指一組給公式賦值的規(guī)則， 據(jù)此規(guī)則可對每一結(jié)構(gòu) U 和指派 S 確定一 由原子公式到值域的映射 v：atomic >value。根據(jù)這個賦值規(guī)則， 可以將賦值 映射進(jìn)行擴(kuò)展：

11、v 為 v ：Formula >value 。元理論語法構(gòu)成（1）獨(dú)立性： 如果形式系統(tǒng)中每一個公理都是獨(dú)立的，即把任一公里A 從形式系統(tǒng)中刪除后，所得形式系統(tǒng) FS不滿足 FSA（即 A 不是 FS的定理），則稱形式系統(tǒng)為獨(dú) 立的；獨(dú)立形式系統(tǒng)是簡潔的；（ 2）一致性： 形式系統(tǒng) FS稱為一致性，或相容的（ consistent ）如果不存在 FS的公 式 A，使得 A， A 同時成立；所有形式系統(tǒng)都應(yīng)該是一致的；（ 3）完全性： 形式系統(tǒng)為完全的，如果對形式系統(tǒng)中任意公式A，或者 A 成立，或者 A 成立；完全性的形式系統(tǒng)，一切都是可知的；因此，幾乎沒有價值；FS 對的任一公式4）可

12、判定性： 形式系統(tǒng) FS 稱為可判定的，如果存在一個算法，對A ，可確定 A是否成立， 否則稱 FS 是不可判定的； 如果上述算法對定理能作出判 斷，而對于非定理未必終止（作判斷） ，稱 FS 為半可判定的；FS 為可判定的，當(dāng)且僅當(dāng)定理集合為遞歸集；( 5)公式集合一致性： 稱形式系統(tǒng)的公式集合 為一致的，如果形式系統(tǒng)是一致的， 且不存在公式 A 使 A ， A 同時成立。語義系統(tǒng)基本上沒有。語法語義關(guān)系研究語法語義關(guān)系， 首先關(guān)心的問題是在語法上的形式演算， 在語義的邏輯推論上是否 成立。這個問題被稱作合理性( Soundness)。其次，是對于語義上的邏輯推理，在形式 演算上是否成立。這

13、個問題是完備性(Completeness)。這兩個問題是語法語義關(guān)系的核心。1) 合理性( soundness)：稱形式系統(tǒng) FS是合理的， FS的任意公式 A 有：FS A， 則 M A ， M為所有結(jié)構(gòu)；2) 完備性( Completeness)：稱形式系統(tǒng) FS 是完備的，如果對 FS 的任意公式 A 有：若 M A，則 FS A ，這里 M為 FS所討論的一類結(jié)構(gòu)；3) 緊致性：稱形式系 FS是緊致的， 如果對 FS的任意公式集 有：如果公式集 的所有窮子集是可滿足的，那么公式集 也是可滿足的；歸結(jié)原理歸結(jié)方法二元?dú)w結(jié)： 設(shè) C1 和 C2 分別含有文字 L1和 L2 的子句，并且 L

14、1 和 L2 有最一般合一 ， 那么下列推理規(guī)則稱為歸結(jié)原理：C1,C2(C1L1 ) (C2 L2 )歸結(jié)過程公式集 前束范式 skolem 標(biāo)準(zhǔn)形 子句集 合一 歸結(jié) 合一與代換：子句集合一后與原子句集之間的邏輯關(guān)系； 合一是代換( t1/x1 tn/x n)將子句集中的變量 xi 代換為項 ti; 歸結(jié)合理與完備：在合一后的子句集上歸結(jié)是一種推理，那么推理能否保證合 理性與完備性；提高效率的策略： 刪除策略；支持集策略；線性策略；在歸結(jié)過程中， 注意： 代換過程如果出現(xiàn) P(a), P(b) 的情況就很可能是代換出現(xiàn)的問題；元定理在歸結(jié)原理中，我們給定的形式系統(tǒng)是： 形式系統(tǒng)是子句集，其

15、上的推理方法不在是分離規(guī)則，而是歸結(jié)； 語義系統(tǒng)是 Herbrand 結(jié)構(gòu)。在這樣的推理環(huán)境中， 我們還是要考慮形式推理 (子句集上的歸結(jié)) 與形式語義之間的 關(guān)系。這些關(guān)系中，我們重點考慮的是合理性和完備性。1、合理性：合理性的表現(xiàn)有兩個定理，前面已經(jīng)敘述過，下面重復(fù)一下： 設(shè)子句集 c為子句 c1和 c2的歸結(jié)結(jié)果，則 c為 c1和 c2的邏輯結(jié)果； 設(shè)子句 c 為子句集 S 的歸結(jié)結(jié)果，即存在一個歸結(jié)序列，得到c，則 c 為 S 的邏輯結(jié)果；2、完備性：若子句集 S 為不可滿足的，那么必定存在一個否證，即存一個導(dǎo)出空子句口的 歸結(jié)序列。模態(tài)邏輯正規(guī)系統(tǒng)模態(tài)邏輯是研究各種不同的正規(guī)系統(tǒng)，這

16、些正規(guī)系統(tǒng)中，最簡單的是 NSK 系統(tǒng)。下面 我們給出 NSK 系統(tǒng)的構(gòu)成。1、 NSK 系統(tǒng)語言部分符號表： p1 , p2 , , , ,(,) ；其中 pi 為原子命題， , 為聯(lián)接詞， , 為模態(tài)詞， (,) 技術(shù)符號。項集：空集。 公式集：由以下遞歸定義：1) pi為公式 (i=1,2,3,4 )2) 如A,B 為公式,那么( A B),( A),( A),( A )都是公式3) 除由 1,2 得到外 , 無其它公式2、NSK推理部分 公理集：包含以下公理：A1 : A AA2 :(AB)( A B) ；通常被成為 K公理A3 : 全部重言式A4 : A （ 當(dāng) A為公理）推理規(guī)則：

17、分離規(guī)則 A B, A, B其他概念與 FSPC 的概念相同，如定理、證明序列等。語義結(jié)構(gòu)1、正規(guī)結(jié)構(gòu)定義我們知道， 對于每個命題的真假都是和可能世界之間有著密切的關(guān)系。 對于正規(guī)系統(tǒng)的 語義，必須考慮可能世界?？赡苁澜缡欠浅６嗟模赡苁澜鐦?gòu)成一個集合。每個可能世界對應(yīng)于不同的場合， 可能世界之間是可變換的。 能夠從一個可能變換到另 一個可能世界。從一個可能世界，能否變換到另一個可能世界在賦予真值時是非常重要的。 例如，如果一個可能世界不能變換到其他的可能世界上，那么在這個可能世界所討論的 A 和A 真都是指 A真這一個概念（當(dāng)然，我們假設(shè)這種關(guān)系具有自反性的條件下）?？赡苁澜缰g的這種關(guān)系，

18、實際上是可能世界的集合中的元素之間的關(guān)系。有了這種可能世界的集合和可能世界之間的關(guān)系， 那么我們就可以對正規(guī)系統(tǒng)中任何公 式賦予一定的真值。正規(guī)結(jié)構(gòu)： 有以上分析可知，對于正規(guī)系統(tǒng)語義被成為正規(guī)結(jié)構(gòu)，正規(guī)結(jié)構(gòu)是指三元組 <U,R,I> ， 其中：U 為一非空集合，稱為宇宙；其成員為可能世界，可能世界用wi 來標(biāo)記；R為 U 上的一個二元關(guān)系，稱為可能世界間的可達(dá)關(guān)系；I 為賦值映射，是U P1P .到 0,1 上的映射； 即對在每一個可能世界中，對原子命題 Pi 賦值；2、 正規(guī)結(jié)構(gòu)的一些解釋 我們對正規(guī)系統(tǒng)中的一些公式進(jìn)行解釋，從而能夠更加了解可能世界的概念。 kw A 表示：指在宇宙中 k 的 w 可能世界中， A 為假 kw A 表示：對于所有 w' U ， w'Rw， kw 'A ，即 A 為真；kw A表示：存在 w' U ，且 w