模態(tài)邏輯講義（2006年）李小五編著中山大學(xué)邏輯與認(rèn)知研究所第1章公理化系統(tǒng)在本章§1我們給出模態(tài)語言和模態(tài)公式，討論它們的語形特性，引入刻畫模態(tài)的公理和推理規(guī)則，然后定義本書主要關(guān)注的公理化系統(tǒng)，并定義相對模態(tài)系統(tǒng)的形式證明和推演概念。最后我們證明這些系統(tǒng)是協(xié)調(diào)和和諧的。從§2到§5我們分別介紹初等系統(tǒng)、基本系統(tǒng)、退化系統(tǒng)和其他重要系統(tǒng)，著重證明這些系統(tǒng)的內(nèi)定理和導(dǎo)出規(guī)則以及這些系統(tǒng)之間的相互關(guān)系。我們也證明某些系統(tǒng)的元定理，例如，等價置換定理、對偶公式定理、對偶符串定理、演繹定理、歸約定理、Post-完備性定理和模態(tài)合取范式存在定理。這些定理往往是經(jīng)典邏輯相應(yīng)定理的本質(zhì)推廣。§1公理化系統(tǒng)協(xié)調(diào)性和諧性本節(jié)我們給出模態(tài)語言和模態(tài)公式，討論它們的語形特性，引入刻畫模態(tài)的公理和推理規(guī)則，然后定義本書主要關(guān)注的公理化系統(tǒng)，并定義相對模態(tài)系統(tǒng)的形式證明和推演概念。最后我們證明這些系統(tǒng)是協(xié)調(diào)和和諧的。為了簡潔，本書我們用=表示元語言意義上的“…當(dāng)且僅當(dāng)…”，用=表示“若…，則…”，用?表示“并非"，用???表示“因為…”，用...表示“所以…”。定義（1）稱L是（句子型的）模態(tài)語言=L由下列互不相同的符號組成：句符集：At=df{pi，…，P"（，…）};②邏輯符：-1,口，A;③技術(shù)符：（，）o（2）遞歸定義ML是滿足下列條件的最小集合：AtcML；A,BwMLnZ,DA,（4人8）eML。-\說明：（一）上述①表示非空集At是可數(shù)的，即At或是有窮的，或是可數(shù)無窮的。At中的元素稱為句符。句符通常也稱為命題變元或句子變元或原子公式。通常也把ML稱為模態(tài)語言，這似乎更符合我們對語言的直觀理解?！负蚢稱為聯(lián)結(jié)符,「（讀作：非）直觀上表示“否定”，A（讀作：合?。┲庇^上表示“并且”，它們通常稱為真值聯(lián)結(jié)符或命題聯(lián)結(jié)符?！酰ㄗx作：必然）稱為模態(tài)符或（一元）模態(tài)算子。從上述定義看，口也是一個一元聯(lián)結(jié)符，只是在本書我們一般不把它解釋為真值聯(lián)結(jié)符。本書我們用口指稱要討論的模態(tài)概念。這個概念通常理解為某種“必然性”。實際上，人們在日常思維中有各種模態(tài)概念，其直觀語義多種多樣，但本書一般不討論。本書主要研究模態(tài)邏輯的技術(shù)部分，即使在語義方面也著重研究兩種形式語義。當(dāng)然，不同的形式語義，特別是不同的公理化系統(tǒng)，刻畫了不同的模態(tài)符，而這些差異的后面實際上有不同的直觀語義（背景）。請有興趣的讀者參見相關(guān)的文獻(xiàn)。（-）At的基數(shù)是有窮或可數(shù)無窮的。但事實上，本書的絕大部分結(jié)果對任意基數(shù)的句符集皆成立。（三）對任意形如口/的公式，稱4是口的轄域.（四）今后若不特別提到，我們總用元變元p,q,r.-（帶或不帶上下標(biāo)）表示At中的公式，其中p,q,r分別特指P”02，P3；用元變元A,B,C,D,???（?；虿粠舷聵?biāo)）表示ML中的公式；用「，①,甲,0,三，…（帶或不帶上下標(biāo)）表示公式集，即ML的子集。（五）???上述①一③提到的符號互不相同，，通過⑵得到的ML中的句子具有唯一可讀性，并且具有可枚舉性。設(shè)語言L是可數(shù)無窮的，即At是可數(shù)無窮的。?.?由L構(gòu)成的ML中的公式是有窮個符號構(gòu)成的符號串，.??據(jù)集合論的基本事實，可數(shù)無窮集的所有有窮子集的個數(shù)仍是可數(shù)無窮的，.?.我們可以枚舉ML中的所有公式如下：A. ???A???zl], ， ，o關(guān)于這方面的嚴(yán)格表述和證明，請讀者參見Enderton的[1972]O(六)“T”稱為結(jié)束符。用在定義、引理、定理和推論等后面?？s寫定義(Dfv)(4v8)=df-1(-—1B)>(Df->)(A―>S)=df—i(Aa—iff),(Df<^)(46B)=df((4T8)A(8T/)),(DfO)OJ=df->a-v4,(DfT)T=dfSv-jp),(Df_L),L=df->ToT說明：(一)上述定義前面的Dfv,Df7,…分別是相應(yīng)定義的縮寫。這在將來證明系統(tǒng)的內(nèi)定理時是很方便的。(-)V(讀作：析取)直觀上理解為“…或…”，T(讀作：蘊涵)直觀上理解為“若…，貝IJ…”，6(讀作：等價)直觀上理解為“…當(dāng)且僅當(dāng)…”，?(讀作：可能)直觀上理解為”…是可能的”。(三)?也稱為模態(tài)符或模態(tài)算子。以后口和?都簡稱為模態(tài)。約定(1)為了節(jié)省括號，本書我們約定公式最外面的括號可以省略，且公式所含的聯(lián)結(jié)符相對公式的結(jié)合力依次減弱：-1， □, ?，A?V, —>，<->?(2)同類聯(lián)結(jié)符滿足右向結(jié)合律例如，我們用小T…->4表不：小……)。(3)若。力0(0是空集符號)是有窮集，則我們用八。和V0分別指稱0的所有元素(據(jù)某個固定的排序方法)的合取和析取。若。={Z},則八。=dfX，V0=df/t?(4)若。=0,則八。=dfT,V0=df-L?T說明：關(guān)于(4)的定義，直觀解釋如下：考慮八0=dfT。我們知道，A。為真的充要條件是(☆)若Ae。，則4真。而當(dāng)。=0時，Ae<P不成立，；.(☆)空洞成立。.?.我們把八0定義為T。同理可解釋V0=dfJ_。定義A的子公式集Sub.)是最小集合》使得①Aw3;②-.Be￥=BaCw+={B,C}uP；UBeWn加巴(2)我們用Sub(。)表示0的子公式集：Sub(0)=o{Sub(J)：Ae0}?(3)稱0在子公式下封閉<=>Sub(0)=0=(4)若A是Y或口8,則我們稱B是4的實主子公式(propermainsubfbrmula)o這時稱-i和口是A的主聯(lián)結(jié)符。若4是BaC,則我們稱8和C是4的實主子公式。這時稱a是A的主聯(lián)結(jié)符.實主子公式也稱為真主子公式或簡稱主子公式。T1.1.5定義(1)稱c是代入映射是從At到ML中的映射。任給公式A,稱Zo是/的代入特例(substitutioninstance)oZc如下遞歸定義：①PnO—oipn),對所有"V。；'②(-^尸-4郎)；③(8aO=(8o)a(C(t)；④(口8)<7=口(80)。給定A,我們IT；用4(Pn/B)表不Ao使得a(p?)=Bo(2)稱48〃0是用C置換/中某個指定的子公式8得到的公式o4(8〃。如下遞歸定義：①若/是指定的a則4B〃C)=C；②若4=3且指定的8在。中②，貝IJA(B//G)=^(D(B//Q)；③若4=。人￡且指定的8在。中，則A(B〃C)=(D(B〃C))八E；④若4=Z)aE且指定的8在E中，貝U/(8〃0=Oa(E(8〃0)；⑤若/=口。且指定的8在。中，則

48〃0=口(。(8〃0)。~\說明：直觀上說，代入式Z(p“/8)表示用8代入Z中的句符pn的所有出現(xiàn)得到的公式，而置換式4(8〃。表示用C置換A中子公式B的一個特定出現(xiàn)得到的公式。1.1.6定義我們用PC表示由下列公理和推理規(guī)則構(gòu)成的系統(tǒng)：A(l)pTqTp,①①是全體自然數(shù)的集合，〃〈①即〃《①。②即不是情況①。A(2)(p->q—>/")―?(p―>q)―>p—>r,A(3)(rpTq)T(rpTF)—p，(MP)A,AtB/B,(US)A/Aa, 其中◎是任一代入映射。T說明：(一)MP稱為分離規(guī)則，US稱為代入規(guī)則“(二)以后我們把PC看作是最小的(空洞的)模態(tài)系統(tǒng)。在構(gòu)造各種(非空洞的)模態(tài)系統(tǒng)之前，我們先來考慮下列顯表示(除了RER)模態(tài)的公理和推理規(guī)則，它們在后面經(jīng)常用到：1.1.7定義(1)公理：(M)口⑦八夕)一(C)口夕人□夕一口防人4),(N)口「(K)口。均)->□〃一>□今(D)(T)口pTp，(B)/?->□<>/?,Op—?口/?—>□?〃，(McK)□?〃—>?口「，□(pA□p—>4)v□(g人□qTp),(W)(Lem)□(□p—>4)v□(□q—p),(Dum)□(□(p-?□p)—>p)—>O□/?—>po⑵推理規(guī)則(RN)A/OA,(RM)4—8/口/一口8,(RE)/68/口/一口8,(RR)/U8tC/D/aD8tDC,(RK)小a…"”7//口/仆…aDZ”—>口.對所有"<co,(RER)AaB/CcC(A〃B)。-\說明：(一)上述公理和規(guī)則左側(cè)的大寫字母串表示它的名字(通常是英文名稱的縮寫)，其中推理規(guī)則前面都冠以Ro(二)當(dāng)?=0時，據(jù)1.1.3(4),RK是T7//T.口兒而此規(guī)則本質(zhì)上是RN.(三)下面我們對上述部分公理和規(guī)則作些簡要的說明：K是為了紀(jì)念Kripke命名的一條公理，但據(jù)R.A.Bull和K.Segerberg在其[1984](p.20)所說：“Kripke似乎從來沒有關(guān)注過這條公理”。筆者認(rèn)為K是模態(tài)邏輯的一條相當(dāng)重要的公理，用此紀(jì)念Kripke對模態(tài)邏輯做出的奠基性貢獻(xiàn)也是恰當(dāng)?shù)?。D是deontic的縮寫，T最早是由R.Feys提出和命名的。5也記作E,而后者是Euclidean的縮寫。B是Brouwer的縮寫，YT+B與直覺主義邏輯有關(guān)聯(lián)。McK是McKinsey的縮寫，也記作.1。G是Geach的縮寫，也記作.2。Lem是Lemmon的縮寫，也記作.3。H是Hintikka的縮寫，Dum是Dummett的縮寫。W是(anti-)welbrdered的縮寫。文獻(xiàn)中也記作G或GL,其中L用來紀(jì)念M.H.L6b,他提出卜,面提到的系統(tǒng)KW。RN是RuleofNecessitation的縮寫，稱為必然化規(guī)則”RM是RuleofMonotonicity的縮寫，稱為單調(diào)規(guī)則”RE是RuleofEquivalence的縮寫，稱為（可證）等價規(guī)則或全等規(guī)則（RuleofCongruence）..RR是RuleofRegular的縮寫，稱為正則規(guī)則。RK是RuleofKripke的縮寫，稱為正規(guī)規(guī)則.RER是RuleofEquivalenceReplacement的縮寫，稱為（可證）等價置換規(guī)則。1.1.8定義和約定令「是公理集（本質(zhì)上就是一集公式），R是推理規(guī)則集。?（1）稱s=<r；r>是（一般意義上的）模態(tài)系統(tǒng)os是如下構(gòu)成的系統(tǒng)：①S的公理是PC的公理和八②S的推理規(guī)則是MP,US和R。（2）這時稱「是S（相對PC）的特征公理的集合，R是S（相對PC）的特征（推理）規(guī)則的集合。T說明：（一）為了方便，當(dāng)「或R為空集時，我們用S=<??>或S=</>來表示S=<0；R>或S=<T；0>?注意：當(dāng)「和R皆為空集時，S=<0；0>=PC,（二）任給模態(tài)系統(tǒng)S=<r；R>0令八是新公理集且R,是新推理規(guī)則集。為了方便，我們也用S+Q+R表示RuRi>o令A(yù)是新公理，我們也用SA簡單表示S+A。我們還用S-A,S—T和S—R分別表示從S中去掉公理A和公理集廠和規(guī)則集R得到的系統(tǒng)。下面的定義給出的模態(tài)系統(tǒng)是本書主要的研究對象。LL9定義E=df<RE>,M=dfEM,R=dfMC,K=df<K；RN>,D=dfKD,T=dfKT,B=dfTB,S4=dfT4,S5=dfT5,K4.3=dfK4Lcm,S4.1=dfS4McK,S4.2=dfS4G,S4.3="S4Lem。-\下面我們分別引入形式證明、內(nèi)定理和推演概念：定義令S是任意模態(tài)系統(tǒng)。(1)稱公式序列小，…，4是S中的形式證明=對每一i使得下列條件至少有一成立：4是S的公理的代入特例；?存在J,左＜，使得4是從4和4據(jù)MP得到的；存在和力，…，使得4?是從,，…，4nl據(jù)S中的特征規(guī)則(模態(tài)規(guī)則)得到的。(2)稱］在S中有形式證明=存在S中的形式證明小，…，4使得4=，。(3)稱4是S的內(nèi)定理，記作-s4Q4在S中有形式證明。我們用Th(S)表示S的所有內(nèi)定理的集合。(4)若4任Th(S),則我們也記作公/,并稱/是S的非內(nèi)定理,(5)稱力和8相對S等價=is4一瓦T說明：(一)上述條件①一③也可以等價表示為：①4是S的公理；存在j,Yi使得4是從4和4據(jù)MP得到的；存在機＜3和力，…，使得4?是從4力，…，4nl據(jù)s中的特征規(guī)則(模態(tài)規(guī)則)得到的；存在使得4是從4據(jù)us得到的。(二)易見公理自身也是內(nèi)定理。i.i.ii定義(1)稱公式序列小，…，4是S中從。的推演O對每一IWiW",下列條件至少有一成立：①4是s的公理的代入特例；②A"》換句話說，存在S的公理A和代入映射。使得4=A(t。存在), 使得4是從4和4據(jù)MP得到的；存在加<0和力，…，/“Si使得4?是從當(dāng),…，/友據(jù)S中的特征規(guī)則得到的。(2)稱4在S中有從?的推演或稱/在S中從0推出，記作0HsA,u>存在S中從0的推演Ai，4使得A?=A,這時也稱小，…，4是S中從。到/的推演.為了方便，以后用。構(gòu)成S的推理規(guī)則稱為S的初始規(guī)則例如，MP就是任何模態(tài)系統(tǒng)的初始規(guī)則。構(gòu)成S的推理規(guī)則稱為S的初始規(guī)則例如，MP就是任何模態(tài)系統(tǒng)的初始規(guī)則。我們也用Cns(0)表示{/eML：0HsJ},且稱Cns@)是。相對S的可證后承集。(3)若1任Cns@)(即/沒有S中從。的推演)，則我們也記作(4)若。={小，…，A,,},則我們用小，…，4%4表示。入兒用小，…，4,表示。(5)稱R=m，…，An/A是S的(強)推理規(guī)則，記作ReRule(S),<=>對所有代入映射a,A\a,A?ff^sA(r<,稱R是S的導(dǎo)出規(guī)則oReRule(S)使得R不是構(gòu)成S的推理規(guī)則?o(6)稱R=4，…，A,,/A是S的弱推理規(guī)則，記作ReWRule(S),<=>若％小，…，且則(7)稱小，…，An/A是S的虛規(guī)則0存在使得S沒有任何形如4的內(nèi)定理。否則稱小，…，4/4是s的實規(guī)則。T說明：（一）以后我們在不致混淆之處省略上面兩個定義中的下標(biāo)S。（二）顯然Cns（0）=Th（S）。（三）稱R是S的弱規(guī)則是因為R只能用于Th（S）的元素，一般不能用于Cns（。）中的元素。例如，在上述定義中，代入規(guī)則只能用于公理（以后我們證明代入規(guī)則只能用于S的內(nèi)定理），否則，例如，我們有p-r?或p-_L,而這些推理都不是我們想要的。（四）（5）的意思是推理規(guī)則應(yīng)該在模式的意義上理解的。嚴(yán)格來說，pi，…，p,卜sq不是S的推理規(guī)則，除非對所有代入映射。，有如1）,…，CT（p?）HS 這正是（5）要表達(dá)的意思。（五）以后我們用RPC表示Rule（PC）（中的元素）。（六）若Re（W）Rule（S）,則稱S有R；否則稱S沒有R。（七）我們關(guān)注的規(guī)則除MP外都是單前提規(guī)則。對單前提規(guī)則，我們有A/B是S的虛規(guī)則oS沒有任何形如A的內(nèi)定理。虛規(guī)則總是（空洞的）弱規(guī)則。為了方便，我們把模態(tài)系統(tǒng)分成幾類：定義令S是模態(tài)系統(tǒng)。（1）稱S是全等系統(tǒng)oS有規(guī)則REo（2）稱S是單調(diào)系統(tǒng)oS有規(guī)則RM。（3）稱S是正則系統(tǒng)oS有規(guī)則RRo（4）稱S是正規(guī)系統(tǒng)<=>S有規(guī)則RK。(5)稱E,M和R為初等系統(tǒng)，稱K,D,T,B,S4和S5為基本系統(tǒng)。T定義令S和團(tuán)是兩個模態(tài)系統(tǒng)。(1)稱S是Si的子系統(tǒng)或S］是S的擴(kuò)充系統(tǒng)，記作ScSp0Th(S)uTh(S。。(2)稱S是&的真子系統(tǒng)或&是S的真擴(kuò)充系統(tǒng)，記作SuS|,oTh(S)uTh(Sj)。(3)稱S和Si是等價系統(tǒng)，記作S=S,,=TMS)=Th(S,)oT說明：要證明ScS),我們只須證S的公理和規(guī)則是Si的內(nèi)定理和(導(dǎo)出)規(guī)則。定義令S是模態(tài)系統(tǒng)。(1)稱S協(xié)調(diào)<=>不存在A使得A和-iJ都是S的內(nèi)定理。(2)稱S和諧o存在力使得/不是S的內(nèi)定理。T我們先來證1.1.9定義的系統(tǒng)是協(xié)調(diào)和和諧的，為此我們先給出一個定義：定義任給A,遞歸定義A的PC-變形/一口如下：p,「'=p“，對每一〃V(o；(「8)w=田口；(5AO-n=S_nAC-n；(口8)-口=8一口。H：(-)“y就是刪去工中口的每一出現(xiàn)得到的公式，其中若有?當(dāng)視為「口「。(二)一口實際上是一個從模態(tài)語言ML到經(jīng)典句子語言的翻譯映射。定理令S=<F：R>是1.1.9定義的系統(tǒng)。S協(xié)調(diào)。S和諧。證明：(1)逐個檢查廠中公理，易見①若4是「中公理的代入特例，則-PC/T□。①逐個檢查R中的規(guī)則，易見②若出，…,B“/CeR,貝IJ8「口，…，B/D/C-aGRPCo下證：③)—s/n卜pc4n°設(shè)is4。則存在S中/的形式證明小，…，A”施歸納于下證：④ipc/j口。若4是PC的公理的代入特例，則易得④。若4是「中公理的代入特例，則據(jù)①易得④。若4是從它前面的公式據(jù)MP得到的，則據(jù)歸納假設(shè)易得④。若4是從它前面的公式據(jù)R中的規(guī)則得到的，則據(jù)歸納假設(shè)和②易得④。這樣，我們證明了③。旃面引入的公理只有w在刪去其中的口后不是重言式。假設(shè)S不協(xié)調(diào)，則存在Z使得Is/且-ST1。據(jù)③，有卜pc"這種方法我們在謂詞邏輯中也常用.當(dāng)然在那里我們刪去的是量詞。> 1pc-這種方法我們在謂詞邏輯中也常用.當(dāng)然在那里我們刪去的是量詞。矛盾于PC的協(xié)調(diào)性。(2)據(jù)(1)。T說明：(一)通常人們用兩種方法證明S協(xié)調(diào)。第一種就是上述方法^——刪模態(tài)法?：據(jù)上述③，通過刪去Th(S)中公式的模態(tài)算子把S的協(xié)調(diào)性歸約為PC的協(xié)調(diào)性。另一種方法我們在以后給出。(二)后面我們還要引入另外一些系統(tǒng)，它們大部分都可以用此方法證明其協(xié)調(diào)性和和諧性。練習(xí)7證明：(唯一分解定理)對每一4eML,下列條件恰有一滿足：(1)JeAt,(2)存在雎一的公式8eML和唯一的符號OeIf口，?｝使得4=08,(3)存在雎一的公式序?qū)?lt;g,OeMLXML和唯一的符號Og｛a,v,t,一｝使得4=BOC。［提示：參見Enderton的［1972］。］歸納原則)設(shè)At的每一句符有性質(zhì)(p；(2)若4有<p,則F和口/有性質(zhì)§；(3)若/和8都有<p,則有性質(zhì)(p。證明：ML中每一公式有性質(zhì)Q。［提示：參見Enderton的［1972］。］任給公式4。證明力的代入特例的代入特例也是A的代入特例。T令S是任意模態(tài)系統(tǒng)。證明S有弱規(guī)則US：對任意代入映射%“=>hsA(7oT說明：此練習(xí)說明代入規(guī)則US可用于S的內(nèi)定理。思考題令舟是S的擴(kuò)充系統(tǒng)。下列蘊涵關(guān)系是否成立？RgRule(S)=>ReRule(S|)?T令&是S的擴(kuò)充系統(tǒng)使得S,和S有相同的初始推理規(guī)則，且令證明：0%/=W卜si4。~\令SuSi。(1)若S1協(xié)調(diào)，則S協(xié)調(diào)。(2)若&和諧，則S和諧。T§2初等系統(tǒng)從本節(jié)起到本章末，我們分別考察一批重要的模態(tài)系統(tǒng)的證明論性質(zhì)。從§2到§5我們分別考察初等系統(tǒng)、基本系統(tǒng)、退化系統(tǒng)和其他重要系統(tǒng)，著重證明這些系統(tǒng)的內(nèi)定理和導(dǎo)出規(guī)則以及這些系統(tǒng)之間的相互關(guān)系。我們也證明其中的一些系統(tǒng)的元定理，例如，等價置換定理、對偶公式定理、對偶符串定理、演繹定理、歸約定理、Post-完備性定理和模態(tài)合取范式存在定理。這些定理往往是經(jīng)典邏輯相應(yīng)定理的本質(zhì)推廣.一、全等系統(tǒng)本節(jié)我們來考察全等系統(tǒng)的一些證明論性質(zhì)。以后我們可以看到，本書涉及的所有非空洞的都是全等系統(tǒng)，所以下面證明的結(jié)果對所有非空洞模態(tài)系統(tǒng)都成立。我們先來證明這些系統(tǒng)的一些重要的內(nèi)定理和導(dǎo)出規(guī)則，它們在今后要不斷用到。為了以后提述方便，在下面的定理中,我們用s(l),…，S(〃)來指稱模態(tài)系統(tǒng)S的內(nèi)定理和導(dǎo)出規(guī)則。1.2.1定義任給"<0。(1)歸納定義口”/如下：口，=/1,???,口"+)=口口7。(2)歸納定義如下：?，=4,???,On+'A=OOnA.說明：□7和分別表示4前面有〃個口和1.2.2定理（1）下列是E的內(nèi)定理和導(dǎo)出規(guī)則:E(l)AcB/OAcOB(=REo)oE(2)RER,從而我們有4c8,C/C(A〃B)qE(3)□>—??―,―1□ >?—\poE(4)?p<—>—?□―\p,—-poE(5)對所有n<（oQE(6)>p.對所有n<coo(2)E=<RER>o證院①1：(1)證E(l)：假設(shè)②—i/l ,①，RPC③□-u4c口-18,②，RE④―(□—4《>—?□―\B,③，RPC⑤O/cOB。④，DfO［說明：（一）上面是一個推演的通常表述：這個推演可看作是由3個豎列組成：第1個豎列是序號①，②，…，它們指稱推演的步驟；第2個豎列是推演的本身；第3個豎列是推演的根據(jù)（推演的出發(fā)點（假設(shè)）、公理、推理規(guī)則（包括導(dǎo)出規(guī)則）、前面已證的內(nèi)定理、形如Df?那樣的縮寫定義）。例如，上述第1行最右的“假設(shè)”表示推演的出發(fā)點，第2行最后的“①，RPC”表示對①提到的4cB運用RPC中的規(guī)則，……。?以后我們也把此規(guī)則稱為RER,雖然，嚴(yán)格地說，它相對E弱于RERo為了簡單，以后我們在第3個豎列不致混淆之處如下省略序號：若一個公式直接從上一行公式推得，則在該行的根據(jù)中不寫序號。例如，上述第3豎列的①，②，③，④均可省略。注意：對一個推演來說，只有第2個豎列才是本質(zhì)的。為了簡潔，以后我們省略第二列中的標(biāo)點符號。類似地，我們?nèi)缟咸幚韮?nèi)定理的證明。(二)本書假定讀者比較熟悉?階邏輯，特別是經(jīng)典句子演算的形式證明和推演，.?.本書以后我們經(jīng)常只給出一個形式證明或推演的關(guān)鍵部分，有時，寫出的一步由幾步縮寫而成，想必讀者能自行補上跳躍的部分和根據(jù)。］證E(2)：在E中設(shè)n。要證^-C<->C(A//B)o考慮置換定義的5種情況：情況1C就是特定的Z：則C(4〃8)=B,...據(jù)設(shè)定和置換定義，有C(4〃8)。情況2C=3且特定的X在。中：據(jù)歸納假設(shè)，我們有FD—D(A〃B),據(jù)RPC,有卜「Dc^D(A〃B),據(jù)置換定義，有情況3C=Da￡且特定的/在。中：據(jù)歸納假設(shè)，我們有-060(4〃8),據(jù)RPC,有卜。aE—(Z)(/〃8))aE,...據(jù)置換定義，有FD八ESE)(A〃B)。情況4C=Oa￡且特定的“在E中：據(jù)歸納假設(shè)，我們有FE0E(A〃B),據(jù)RPC,有 Oa(E(/〃8)),二據(jù)置換定義，有卜。人Ec(￡U￡)(/〃5)。情況5C=DD且特定的“在。中：據(jù)歸納假設(shè)，我們有?DcD(A〃B)。據(jù)RE,有1口。6口(。(/1〃8)),二據(jù)置換定義，有1口￡>—(□￡>)(/〃8)。證E(3)：TOC\o"1-5"\h\z①.□/? PC?從實用的角度，我們這里設(shè)《可含v?從實用的角度，我們這里設(shè)《可含v和?.口>—?—?口—?—、p RER③口/H->-iO~、p DfO證E(4)：―?□—ip<—>―?口—、p PC②>-1口-、p DfO證E(5)：若〃=0,則顯然。若"=1,則據(jù)E(3)。設(shè)〃=%時要證結(jié)果成立，下證"=左+1時要證結(jié)果成立：①口7"-1<>"-中 歸納假設(shè)②□*+》—口->?， RE③ □"+16->~>口-1<>二0 RPC(或RER)④DfO證E(6)：①—!?"—?——\p E(5),USfOJpCrCIJp RPC③?”—?——,口"—<p RPC④?>>>口" RER⑵據(jù)E(2),只須證Eq<RER>,B|J<RER>WRE：①AcB假設(shè)口2口5RER說明：據(jù)(2),我們看到系統(tǒng)E實際上就是把PC的等價置換規(guī)則運用到形如口工的公式，.?.全等系統(tǒng)(即E的擴(kuò)充系統(tǒng))都有(相對所有公式的)等價置換定理。1.2.3對偶公式定義設(shè)/中不含T和c。,稱T是4的對偶公式0下列條件滿足：(P")d=->P",對每一”<3;(18)d=此4(5AC)d=5dvCd;(5v0d=5dACd；(□S)d=O5d；(O5)d=n5do說明：據(jù)上面的定義，我們稱A與V互為對偶，稱口與?互為對偶上述定義的(4)和(6)不是本質(zhì)的，增加它們只是為了簡潔。例如，若不用(4),則(SvOd=(-1(^BA-,Q)d=-1(-i5dv—iCd).. 據(jù)⑵和(3)而在PC中，從而在E中，有內(nèi)定理T-18dV-1cdK^dAC*1。例令J=O-.DOnp,則Ad是□->0口0”。T說明：T可以直觀地理解為：先加「在A前，然后右移越過口(或?)時把口變成?(或把?變成口)，越過人(或V)時把A變成V(或把V變成A),直到不能再內(nèi)移為止(「移到句符前)。對偶公式定理令S是全等系統(tǒng)。則卜sZ-證明：施歸納于Z的結(jié)構(gòu)(這里設(shè)4含V和?).情況1A=pn? P0一~1->P"，??.據(jù)對偶公式的定義，有卜sP"C—<P?°情況2 則①B-B。 歸納假設(shè)②此eifid RPC③—iBcTrB)。 對偶公式定乂情況3A=BC貝I]①B-B”,CeC」歸納假設(shè)BaCc-15dA-■C41 RPCBACe/dvC*1) RPC④8aCc「(8Aod 對偶公式定義情況44=BvC。證明類似情況3。情況5A=DB1,則①歸納假設(shè)②□8c□-18dRE③口8--1-1口-1腔RPC④口8<->—1?b"DfO⑤口86-1（口8）6對偶公式定義情況6A=OB.證明類似情況5。T說明：（一）對偶公式定理說明任何公式與它的對偶的否定等價。（-）若我們把v和?看作是縮寫定義，則我們無需在上一定理的證明中考慮情況4和情況6,只須施歸納于A的實主子公式，若Z自身不是句符。定義稱一個符號串/是模態(tài)符串=/是由｛%「，口，?｝中某些符號構(gòu)成的有窮串，其中（|）表示空串。~\說明：（一）。與0不同，后者是空集的記號。（二）除了。以外的模態(tài)符串嚴(yán)格說就是一元邏輯符串。注意：?不是本質(zhì)的。（三）據(jù)上述定義，下列都是模態(tài)符串：傘，口，傘，口，O,口?「， ?□「口?。推論下列是E的內(nèi)定理或?qū)С鲆?guī)則：E⑺ ~1/440E(8)Fc/。E(9)A/A(B//-￡d),A/AJB〃Bd)。E(10)/一(屋)%E(ll)//4。E(12)F//。E(13)AtB/B&tALE(14)E(15)A/A',其中4是若干次據(jù)F列原則從4得到的公式：若是4的子公式使得如含「，則把夕中的「右(或左)移，在越過口(或?)時把口(或?)變成?(或口)，在遇到「時刪去成對的-m。證明：舉例證明E(10)：①ri11 對偶公式定理②/c(F)d對偶公式定義③Zc(T)d E(8),RER舉例證明E(15)：據(jù)E(3)和E(4),US和PC的內(nèi)定理，在E中，有(☆)1--1口8㈠?-1B, 卜一B—B,若干次運用RER,易從1得到X、注意：(☆)中前兩個等價式從左主子公式到右主子公式是內(nèi)移「，從右主子公式到左主子公式是外移T說明：(一)以后我們把E(15)簡記為LMC。(二)LMC的4個重要的特例是：①②③④///(-(口8〃?-18),①②③④LMC可以看作是RER的一種特例。據(jù)E(15)的證明，我們甚至還有定義令夕是一個模態(tài)符串。(1)稱/是正模態(tài)符串o夕中「出現(xiàn)偶數(shù)次(包括0次)；(2)稱/是負(fù)模態(tài)符串中「出現(xiàn)奇數(shù)次：(3)稱/是疊加模態(tài)符串Q夕中口或?出現(xiàn)〃22次；(4)稱夕是標(biāo)準(zhǔn)模態(tài)符串o,中不含「或唯一的「只出現(xiàn)在夕中最前面。(5)稱如是純模態(tài)符串0如是不含「的模態(tài)符串。T對偶符串定義令如是一個模態(tài)符串。稱，是/的對偶符串o01是把夕中口和?的每一出現(xiàn)分別同時替換為?和口得到的符串。T說明：上述定義的形式定義為：1.29定義任給模態(tài)符串夕，遞歸定義，如下：(1)(2)(->—尸=-)，,(□“=?，，(O/)d=C/d?T1.2.10定理令夕和步是模態(tài)符串，令S是全等系統(tǒng)。則在s中:1夕1-^-npCp。(3)卜加o—p,(4)(逆對偶定理)令(A)手pT@p,(Ad)科pT寸p。則-A<=>1Ad。(5)S+A=S+Ado(6)(等價對偶定理)證明：證(1)：①句?夕p)d②/p<->-l，pd③如一-10dr?證⑵：①處—「父2(2)―I/—!，<->―I―\p③-10-《pCp證(3)：據(jù)⑴和(2)。(4)n:①$pT善p②->朔7-1%(3)―>#->2一一,/-1P④，p"p卜-1/—>p<=>-9％。%夕pc0PoisGpCp。對偶公式定理對■偶公式定義，對偶符串定義對偶公式定義(1)US,RPCRERARPCUS(2)1我們稱Ad是A的逆對偶公式.，，._，，u：①②③④據(jù)TOC\o"1-5"\h\z賢p一3p Ad①②③④據(jù)-1ddp—》 Rpc—I夕1 US?P-0P (1))易得(5)和(6)。T說明：據(jù)(5),在全等系統(tǒng)中，用?pTlJOp作為公理和用?口〃-?口「作為公理是等價的。定義令S是任意模態(tài)系統(tǒng)。(1)令夕和步是兩個模態(tài)符串。稱小和/相對S等價=%如一期。(2)用Modal(S)表小S中兩兩不等價的模態(tài)符串的個數(shù)。~\說明：在后面的1218,我們證明E有可數(shù)無窮多個兩兩不等價的模態(tài)符串。推論(1)]?-,□和□□相對E等價。(2)任意正模態(tài)符串相對E等價一純模態(tài)符串。(3)任意模態(tài)符串相對E等價一標(biāo)準(zhǔn)模態(tài)符串。T二、單調(diào)系統(tǒng)定理(1)下列是M的內(nèi)定理或?qū)С鲆?guī)則：M(l)RM,M(2)AtB/OAtOB(=RM。)，M(3) 八夕)—》Op八Og,M(4)OpYOqTOipvq)(=Co),M(5)□/?v□ □(pv^r)(=Fc),M(6)(OpT□q)T□(pTq)。)EcMo證明：(1)證M(l)：4TB假設(shè)RPC口/6口(4人8)RE口(Za5)tD4人口8 M,US口力一口8③，④，RPC證M(2)：4TB假設(shè)—\B—>—\ARPC□—15—>□—RM—?口—\A->—?口—\BRPCOA^OBDfO據(jù)M(2),PC和RPC,易得M(3)和M(4)o證M⑸：①口「一口⑦丫夕)，口夕一口⑦丫夕)PC,RM②(Jpv口qr口(pvq) RPC證M(6)：TOC\o"1-5"\h\z① (Op—＞口4)—＞—(?「\/口4 PC②(Op—＞口夕)—＞口-^/口］ LMC③(?夕一口2口(/聞 M(5)④ (Op—?口夕)一》口仍一＞夕) RER(2)據(jù)1.1.13,只須證Th(E)qTh(M),而這顯然。~\1.2.14對偶符串定理令S是單調(diào)系統(tǒng)，令，和步是兩個正模態(tài)符串，且令(A)Gp—Sp,(Ad)冊廠斷p,(RA) (正串單調(diào)規(guī)則)①(RAd)-A—RAgRule(S),4sAdoRAdeRule(S)o證明：⑴“n”：①4TB 假設(shè)②aiB RM,RM。，假言易位規(guī)則②TOC\o"1-5"\h\z(3)f4gA A, US④ ③，②，RPC“u”：① pip PC② RA(Z)=> ：①4TB 假設(shè)② r4rB RM, RM。，假言易位規(guī)則③步峭》8 Ad, US④「46b ②，③，RPC① pip PC?易見它是對RM和RM。的概括。?嚴(yán)格證還是要施歸納于/的長度，???/中有偶數(shù)個r。所以可以對偶數(shù)個r做歸納。②贊…6PRAdT說明：本定理關(guān)于正模態(tài)符串的假設(shè)條件是本質(zhì)的。因為從pTq推不出-pTf?推論令S是單調(diào)系統(tǒng)。則S+A=S+Ad=S+RA=S+RAd。證明：據(jù)1.2.10(5)和上一定理。~\說明：據(jù)上述推論，在單調(diào)系統(tǒng)中，我們可以用公理，也可以等價地用相應(yīng)的規(guī)則。例如，M=E+M=E+RM。三、正則系統(tǒng)定理(1)下列是R的內(nèi)定理或?qū)С鲆?guī)則：r(1)o>nn(=R),R(2)Ogv/cOpv?夕(=Ro),R(3)?(pvq)―q(=Mo),R(4)RR,R(5)K,R(6)小人…aJ〃一>4/口4仆…人口4T口4R(7)AtBtC/QAtQBtQC(=RRo),R(8)口,人?［一>?(/?△1),R(9)Q(p—>4)<->(口夕—>O^)oMcRoR=<RR>=<RRo>Dfn=<Mo；RM>>dq=<Co?Mo；REo>dq=<K:RM>,其中下標(biāo)“Df口”表示當(dāng)前系統(tǒng)的初始模態(tài)符是?,縮寫定義是(DfO)0/1=(if―)?—\Ao證明：(1)據(jù)C和M,顯然有R(l)。證R(2)：(D□(-\p/\-11)<—>口-i.aD—】q(2)□―>□―ipA□-、q(§)—?LU―i(pv(y)<->—)□―p\z―)□―11④OSvq)-OpvOg證R(4)：A八BtC口(4/\5)一口。③口/人口8一口(4八8)④DJaCB—>CC證R(5)：①(pTq)八pTq口仍一>4)人口/?一□[口⑦7l)—>□〃一>□夕證R(6)：①小人…aJ〃一>/假設(shè)RMC,US③，②,PCRRRPC②□小人口(42八…八4)一>□/③口小人…人□/〃一>□/證R(7)：①4tBvC(2)―iB八-iC-?-\A(§)O—?5aEZI-\C—>□—\A④OAtOByOC證R(8)：(J)EJ(p—》~?夕)一^口夕一^口-、q② □「(pAq)—>□〃一>□-1[R,USRERRPCDfORPC假設(shè)RRR,RERXw-2假設(shè)RPCRRRPC,DfOK,USRER-1?(p八q)―>□p―>-1?q(pM)R(9)：O(r2vq)c?-ipvOq?(—>―iLZIpvO^?(P一夕)c(□pi?1)LMCRPCRo,LMCRER舉例循環(huán)證<RR>=<RR)>dq=<Mo；RMo>d「°假設(shè)RPCRRoRPCDf口先證假設(shè)RPCRRoRPCDf口①A八BtC②-iC—>—l4v-?5③?「CtOYvOR—>?—i/i八一)?—18—>--iCRM>>Dfo：假設(shè)RMoMo,RPC(§)□/IaEiib―RM>>Dfo：假設(shè)RMoMo,RPC4tBvCOZtO/v。OAtOBvOC□—i/?a□—10—?□—i(pvq)PC,②—>□—?(pv^)—>—?□-ipv-i□—iq RPC③?(pvq)->OpvOg DfO再證RMo：①4TB 假設(shè)②—(5a-\B—>―\A RPC③□—△□一?□F RR④「口力—」口」8 RPC⑤ OAtOB DfO其余未證的均留給讀者作為練習(xí)。T最后證vMo；RMo>DfaC<RR>：先證Mo:RR說明：(一)R(6)中的限制條件是本質(zhì)的，不能改成〃20,也就是說，R(6)WRK。(―)<RR>和<RR°>dg可以稱為(兩兩)對偶系統(tǒng)”后面我們可以看到這樣的時偶系統(tǒng)有很多。1.2.17定理(Chellas,[1980](p.243))令S=E+0使得0g{M,C,N}o則S有下列弱規(guī)則(參見1.1.11(6))：OA/A,OA/A,口4—口8/4-?8,OAtOB/AtB,口4—口8/468,OA-OB/A-B。證明：先定義從ML到ML中的一步刪模態(tài)映射6如下：即")=P"對每一“<3,⑷，5(Ja5)=5(J)a5(5),5(口4)=兒易證：8(AOB)=8(A)O8(B),其中Oe{v,t,c}[注意：(一)6(4)和1.1.15定義的《一口不同。例如，易見6(口?！?gt;□□/?)是0-?口/?,而(□/7—□□「)一''是(—.)8(Oy4)=3(-1口-l4)=—?—iAo]先證在S中有下列弱規(guī)則：①r=>a8(j)o設(shè)卜4則存在S中4的形式證明小，…，An=Ao施歸納我們要證：②卜6(4)，對所有1<運〃。情況14是S的公理的代入特例：只須考慮模態(tài)公理。若4=C］(8aC)tDBaDC是公理M的代入特例，則N4)=BaCt8aC。...它是PC的內(nèi)定理。若4=D8aEICtD(Ba。是公理C的代入特例，則3(4)=3aCt8/\C。，它是PC的內(nèi)定理。若4=口丁是公理N,則易見B(4)=T是PC的內(nèi)定理。［本情況我們實際證明了一個更強的結(jié)果：ipcM4)。］情況24是據(jù)MP從前面某個4和4T4得到：據(jù)歸納假設(shè)，我們有受⑷，卜5(474)。而后者是13(4)T3(4)，???據(jù)MP,有13(4)。情況3A,是據(jù)RE從刖j面某個Aj=B^->C得到：小，…，4中每一項都是內(nèi)定理，③HAj,,'：5(/4,)=5(□ □Q=B^C=AP.I據(jù)③，F(xiàn)(4)。［注意：本情況無需歸納假設(shè)。］這樣我們證明了②,從而證明3(小)，…，—=6(4)是3(/)在S中的形式證明，，①成立。據(jù)①易證(1)—(6)oT說明：(一)我們在上一證明中主要采用一種有別于1.1.15的方法的刪模態(tài)法。后面我們還會介紹其他同類的方法。(二)在后面的6.1.27,我們要求讀者證明系統(tǒng)E,M和R沒有形如的內(nèi)定理，.,?口4/4也是這3個系統(tǒng)的虛規(guī)則。下面我們考察上述系統(tǒng)的不等價模態(tài)符串的個數(shù)。1.2.18定理令S=E+G使得。u{M,C,N}。則S有可數(shù)無窮多個兩兩不等價的模態(tài)符串。證明：定義從ML到ML中的另一種刪模態(tài)映射t如下：T(P")=P”對每一n<a>,x(―\A)=-*iT(/4),t(Aa8)=t(J)at(5),t(D/1)=To如上一定理的證明易證(那里的情況3在此更簡單)，在S中，有①HJ=>HT(J)o任給IWmVto,則工(pdZTp)=pcT。下證：②FpcETp。假設(shè)要證結(jié)果不成立，則...據(jù)①，我們有ip—T,ip,...對任意/,據(jù)US,有；.S不協(xié)調(diào)，矛盾。據(jù)②和1.2.17(5),我們有③-對所有n<(Oo據(jù)③，易見要證結(jié)果。也即我們有：Modal(S)=K0oT說明：據(jù)上述定理，初等系統(tǒng)有可數(shù)無窮多個兩兩不等價的模態(tài)符串。練習(xí)1.2證明E=<REo>DfOoT證明：M=<RM>=<RMo>nf-ioTx)zxuz)1234z(xzl\z(xz(x證明下列是M的內(nèi)定理或?qū)С鲆?guī)則：x)zxuz)1234z(xzl\z(xz(x□。、…丫口外一口伽丫…師)；AtB/$At?B, 其中/是正模態(tài)符串。(II)口4—5/口/一口8是M4的導(dǎo)出規(guī)則。T1.2.22(I)證明下列是R的內(nèi)定理或?qū)С鲆?guī)則：□ □(［一>〃)一>□(p—>r),□(pTq)八O(pz)T?(g八廠)，O(pTqz)T(5T<>q)八(UpTOr),□(p-?^)-^Op-?O^,□(pTq)人□pT?(［一>尸)一>?(pAr),OT?-?(Dp-?Op),□(p—q)T(□p<->□q),D(pv^)—>OpvD^,□(piV-vpn+|)-?Op1v-vOpnvCprt+1,口⑦】人…A/?〃)cDp］A…人口為， 其中□p|A-ACprtAOpzl+1-?O(p|A-Apn+I),口口夕八O(q八人…人?,〃)T?(qa?(qiap)a…a?(q〃Ap)),At&v…v8“/OMT<>m8N…vO"B“，其中m<(o且AtBiv…vBa/OAiOBw…vOB“,其中1<"<3。(II)證明1.2.16(3)中未證部分。(III)證明R+Q(pTp)=R+D。(IV)(R4的演繹定理)0o{□J}?-K45=>0I-R4口/—?瓦T下面和后面我們在有一定難度的練習(xí)的序號上標(biāo)以*:*證明口?口?「一口?/?是R4的內(nèi)定理。T說明：據(jù)上述練習(xí)，易見□?口?和□?相對R4等價。§3基本系統(tǒng)本節(jié)我們來研究基本系統(tǒng)K,D,T,B,S4,S5,它們是6個最常見的正規(guī)系統(tǒng)，也是本書重點要研究的系統(tǒng)。定理(1)下列是K的內(nèi)定理和導(dǎo)出規(guī)則：\!/V),\—/\!/\71\!/V),\—/\!/\7123456FZIVZIV/IXzl\/|\<<<<<<FKK-K-KKRM,RE,(從而)RER,□(pvg)—>Upv?g,□/?a□q—>□(p^q)(=C),n(pA^)<—>oocj(=r)oKoK=<N,R；RE>=<C,K(l)；RM>=<N；RR>=<RK>oK=EMCN=MCN=RN。證明：(1)證K(l)：據(jù)RN顯然。證K(2)：①A-^B 假設(shè)②□(28) RN③4T口5K, US④□力一口8 ②，③，MP證K(3)：據(jù)K(2),有RE。再如1.2.2的E(2)的證明，易得RERo

K(4)：□(fTp)TK,US□(-—>p)—>—?□―14V□pRPC□(pvq)TIZIpv?1K(5)：RER,DfOp—q—p八qPC□pT□(qTpDRM□(qTp/\q)T□q-□(p/\q)K,US□/?aDqT□(pm)②，(3),RPC證K(6)：□(p八q)T□/7, □(p八夕)一>□qPC,RM□ Dp/\dqRPC,3；□(p八4)<~?口夕人口g②，K(5)⑵顯然。(3)我們來循環(huán)證明。先證Kq<N,R；RE>：證RN：①A 假設(shè)②Tc4 RPC③□Tc口力 RE④□J (3),N,RPC據(jù)1.2.13的M(l)的證明，從M(R的一半)和RE得RM。下證K：①□((pTg)Ap)Tdg PC,RM② 口伊—>^)a□p—>□[ R③□(p-g)—>口°—>口9 RPC下證<N,R；RE>c<C,K(l)；RM>：據(jù)RM有RE。而據(jù)K(l)和RM易得No據(jù)RM易得M(見K(6)的證明)，再據(jù)C易得R。下證<C,K(l)；RM>c<N；RR>：證RM：①4TB 假設(shè)② AftB RPC口人口/一口8RR④ 口4一口8 RPC據(jù)N和RM易得K(l)?而據(jù)RR易得C?下證<N；RR>c<RK>：易見RR是RK(當(dāng)"=2時)的特例。下證N：TtTPCTtDTRK("=0時)口丁RPC證<RK>UK：施歸納于〃。當(dāng)”=01tRK就是TtZ/TtDH/.①Tf4T設(shè)②ARPC③□JRN④丁一口4RPC當(dāng)"=1時，RK就是RM(=K(2))。歸納假設(shè)”=上時要證結(jié)果成立。則①4A+1—>8 假設(shè)②A?a*** ->B RPC③口工口…>8)歸納假設(shè)口/仆…K,RPC⑤口小a…aD/*+i->D8 RPC(4)據(jù)(3)顯然。細(xì)節(jié)請讀者補充。T說明：據(jù)(3),有RK的系統(tǒng)就有K和RN,所以正規(guī)系統(tǒng)總是K的擴(kuò)充系統(tǒng)。1.3.2定理下列是K和D的弱推理規(guī)則:DA/A,OA/A,?口/-?口8//-?8,?41OB/4-B。證明：本證明類似1.2.17的證明。.?.下面只補充不同之處：情況14是公理的代入特例：只須考慮模態(tài)公理。若是K的代入特例，則N4)=(B->C)t8tC。易見它是K的內(nèi)定理。若4=口8-?08是D的代入特例，則6(4)=87「->8。易見它是D的內(nèi)定理。情況34是據(jù)RN從前面某個4得到：；卜溝，且8(4)=3(口Aj)=Aj,?*.卜8(4)。 ?說明：對其他基本系統(tǒng)，上述定理不成立。主要原因是上述情況1不能通過：口?0一??是公理T的代入特例，但以后我們可以用反模型方法證明60OpTOp)=Ope「p不必然是含T的系統(tǒng)的內(nèi)定理。口07口口0是公理4,但以后我們可以用反模型方法證明6(口0—口口°)=「一口。不必然是含4的系統(tǒng)的內(nèi)定理。Op^DOp是公理5,但以后我們可以用反模型方法35參見后面練習(xí)3.4.10(1)①。證明&(?「一口?0)=Op不必然是含5的系統(tǒng)的內(nèi)定理。從這里和1.2.17我們可以看到公理C,M,N,K和D(的代入特例)有一種對稱性。這種對稱性是1.1.7提到的其他公理(除了公理W)所不具備的。下面我們來考慮K的演繹定理。1.3.3定義令小，…，4是K中從。到X的推演。對每一143機W",稱4在此推演中依賴4n0下列條件之一滿足：4=4；(2)存在j,4Vi使得4從4和4據(jù)MP得到，且力和4至少有一在此推演中依賴Ami(3)存在_/<?使得4從4據(jù)RN得到，且4在此推演中依賴4。T說明：4依賴4“的直觀意義是：4就是4或4是以Am為一個前提(可能還根據(jù)其他前提)經(jīng)過若干步推演得到的。引理設(shè)在0u{4}1k8的某個推演中8不依賴4。則。FkB。證明：令8”…，8〃是K中從6j{4}到8的推演使得8在此推演中不依賴力。施歸納于IWiW”，只須證：(#)若5在此推演中不依賴人則。-8,。設(shè)5在此推演中不依賴4。分情況證明如下：情況18,是公理的代入特例或?則據(jù)推演的定①?.㈤在此推演中不依賴4.??無須考慮/=/的情況。義，。卜情況2存在/，左<〃使得8,是從5,和&據(jù)MP得到：?；5在此推演中不依賴4,.?.馬和以在此推演中都不依賴兒據(jù)歸納假設(shè)，。卜身和。.?.據(jù)MP,易證0情況3存在〃使得8,是從與據(jù)RN得到：:B,在此推演中不依賴人.?.當(dāng)在此推演中也不依賴4。據(jù)歸納假設(shè)，我們有0H即；.據(jù)RN,易證0H5,oT引理設(shè)d\j｛A｝卜kB,且存在K中從0u｛4｝到B的推演使得RN在其中有機<。次用于依賴/的公式。則01K□，人…八口"'/—>8。證明：設(shè)B\,…,B“是K中從入｛4｝到B的推演使得RN在其中有加<。次用于依賴4的公式。施歸納于下證：在K中，(☆)01口叮a…—>3"其中〃表示在推演叢，…，8,中運用RN于依賴4的公式的次數(shù)。因此當(dāng)i=n時h=m。情況18,是K的公理的代入特例：則易見由H據(jù)RPC(蘊涵引入規(guī)則)，易證。14T80?.1=口，，二0卜口，-?瓦。；我們沒有用RN,.?.(☆減立。情況2B,e@u｛4｝：若Bw?,則①H即其余如情況1所證。若8,=4,則0 其余也如情況1所證。情況3存在j,k<i使得8,從耳和Bk=BjTBj據(jù)MP得到，且在推演5，…，耳中運用RN于依賴4的公式有無次，在推演8”…，當(dāng)中運用RN于依賴4的公式有人2次：據(jù)歸納假設(shè)，有0卜口，A…—>巨， 且卜□a???a□l，2A o,:h，420，,易證卜口°/1人…aE|'/T口，A…Ad"/,P-□<)a……據(jù)三段論(RPC),易證P1口，a…?耳一》為，且?-口，人…據(jù)蘊涵分配規(guī)則(RPC),易見(☆)成立。情況4存在/<i使得8,從B)據(jù)RN得到?子情況1號不依賴出則據(jù)依賴的定義，Bi，…,Bj是K中從到名的推演使得用在此推演中不依賴A.據(jù)前一引理，0HBj,...據(jù)RN,0I-5?：.(P卜47比，...易見(☆)成立。子情況2號依賴4,且在推演S，…，身中運用RN于依賴力的公式有幾次：據(jù)歸納假設(shè)，01□"“A…aD"47用,據(jù)RK.。1口'/a…人口"—>口用，'：hi<h,:.hi+19,二01口°/^…aEI'N—…Ad''9,再據(jù)三段論，我們有(☆)(1T據(jù)上面的引理，我們有:K的演繹定理(1)設(shè)以j{N}1k8,且存在K中從久j{N}到B的推演使得RN沒有用于依賴/的公式。則01k/t艮(2)設(shè)41k8,且存在K中從N到8的推演使得RN沒有用于依賴力的公式。則FkAt瓦T下面考察系統(tǒng)Do定理KcD?(2)下為是D的內(nèi)定理或?qū)С鲆?guī)則：d(i)oga，D(2)A/OA(=RN。)，D(3)OpvO-ip。D=K+O(p->p)。D=K+"O/。證明：(1)顯然。(2)證D⑴:①□(/?—>p)->O(p—>p) D,US②□仍Tp) (1).K(l)③ O(p—p) ①，②，MP證D(2)：①/ 假設(shè)② 口4 RN③口/->?/ D, US④ OA ②，③，MP證D(3)：據(jù)131(2),RcK,①②①②(3①②③d①②?(pv「p)PC,D(2)?pvO-ipR(2)據(jù)D(l),只須從K+O(pTp)推出D：VRcKcD,O(p->p) 公理?(pTp)c(Dp—>Op)R(9)Dp-^Op ①，②，MP據(jù)(3)和D(2),只須從K+4/OZ推出?(pip)：pTp PCo(/?—>/?) a/oaT1.3.8定義稱1是常公式(constantformula)<=>A是用T和「，人或口構(gòu)造出來的公式：/是用T作為原子公式構(gòu)造起來的公式。T下面定理中的矛盾式是經(jīng)典二值語義意義上的常假式。1.3.9定理令“是常公式。(1)若/々是重言式，則N是D的內(nèi)定理。(2)若4口不是重言式，則Y是D的內(nèi)定理。證明：令卜=卜口。施歸納于4的結(jié)構(gòu)。情況1A=T：則不口=1"是重言式，二一4情況2A=「B：再分情況考慮：子情況1A口是重言式，則-vT。=「「8口不是重言式，.??8一口不是重言式，，據(jù)歸納假設(shè)，7, ”子情況27一口不是重言式：先證：(☆)用T和「或a構(gòu)造起來的公式D是市言式或矛盾式[(☆)實際是經(jīng)典句子邏輯中的一個結(jié)果。]施歸納于。的結(jié)構(gòu)。若。是T,則。是重言式。若D=[E。則據(jù)關(guān)于(☆)的歸納假設(shè)，E是重言式或矛盾式，則是矛盾式或重言式。若0=Ea凡則據(jù)關(guān)于(☆)的歸納假設(shè)，E和尸是重言式或矛盾式。設(shè)E和尸是重言式：則。也是重言式。設(shè)E或產(chǎn)不是重言式：則據(jù)(☆)的歸納假設(shè)，E或尸是矛盾式，二。也是矛盾式。...(☆)成立?，F(xiàn)在我們回到正題。?.7一口不是重言式，二據(jù)(☆%/T口是矛盾式，...8一口是重言式，，據(jù)歸納假設(shè)，卜8,；. ；.卜-vl。情況3A=BaC：再分情況考慮：子情況14口是重言式：因為工口=8口八C口，.IB口和C一口都是重言式。,據(jù)歸納假設(shè)，卜5且HC,/.14子情況24一口不是重言式：則易見一口或(T口不是重言式。.?.據(jù)歸納假設(shè)，有 或t~「C,二因此我們有1877),；.1-d。情況4A=DB：再分情況考慮：子情況14一口是重言式：口=廣口，...8一口是重言式，據(jù)歸納假設(shè)，有卜8,.,.據(jù)RN,有卜口8,二卜兒子情況2 不是重言式：則8Y不是重言式，據(jù)歸納假設(shè)，有卜[8,...據(jù)RN,有卜口「8。據(jù)公理D,我們有i-O-.fi,據(jù)LMC,有卜-1口8,i-vl。T說明：這個定理揭示系統(tǒng)D的內(nèi)定理集相對常公式的極大性：對每一常公式4/或-4是D的內(nèi)定理。下面考察系統(tǒng)T。1.3.10定理(1)下列是T的內(nèi)定理或?qū)С鲆?guī)則：T(l)p—Op(=T。)，T(2)A/OA(=RN。)，T(3)D,T(4)Dp)。T(5)口-\(p―>□0)—>口―>paDcToT=K+T,,其中(Ti)(dp—pM—Og)。證明：證T(l)：① /+)口「 T,RPC②-n-ip^-iD-np US③ pTOp RER,DfOT⑴是T的逆對偶公式，，T(1)也可以從T和逆對偶定理1.2.10(4)直接得到。證T⑵:據(jù)T(l)。證T(3)：據(jù)T和T⑴。證T(4)：①□―?□p T(l),US②?—□夕).(口0-?0口?) R(9),US③ O(pTLIp) ①，②，RPC證T(5)：① O(pTUp) T(4)②—>□「) DfO③ 口—i(p―>LZlp)―>□―、p RPC⑵⑶①②③④據(jù)T(3)⑵⑶①②③④從T證Ti顯然。下面只須證從K+T1證T：(□p—>p)v(―p—>?―T],US(□p7p)v(-><>-ip—>p) RERTcRp(□p—>p)v(Dn—>p) LMCTcRp下面考察系統(tǒng)B.1.3.11定理TcB.(2)下列是B的內(nèi)定理或?qū)С鲆?guī)則：B(l)OAtB/4TDB(=RB),B(2)OUp—p(=B。)，B(3)ODp^QOp(=G),B(4)OC/jaOC^—>□<>(/?a^)oB=T+RBo證明：(1)顯然。(2)證B(l)：①OAtB 假設(shè)②RM③ A-^UOA B,US④A^\JB ③，②證B(2)：據(jù)B和逆對偶定理1.2.10(4)。證B(3)：據(jù)B(2)和B顯然。證B(4)：pAg7B,USOUpTp B(2)③④⑤G①②③④⑤G①②OCpAO□ ②，③，RPC?□pA<>ElgTCIO(pAg)④，①據(jù)B(l),只須從T+RB證B：Op^OpPCp—>口?/? RBT下面我們來考慮S4,這個系統(tǒng)有許多有趣的性質(zhì)。據(jù)1.1.20,任意模態(tài)系統(tǒng)S都有弱規(guī)則US,.".若Hs$p—Sp，Hs則對所有4有我們可以有下面的約定：約定在不致混淆之處，我們用卜s?T力和1S?S、分別表示Hs?p10p和Hs T定理TcS4,(2)下列是S4的內(nèi)定理：S4(l)口一□□，S4(2)S4(3)?□?一?,S4(4)□?一□?□?,S4(5)□?一□?□?,S4(6)?□一?口?口,S4(7)□一口?口,S4(8)□(口p->g)T□pT□q0(3)(S4的演繹定理)eu{/}卜S48=。卜S4口/->8。證明：⑴顯然。(2)證S4(l)：①□一口□ 4②□□一口 T, US③ □一□□ ①，②，RPC證S4⑵:據(jù)S4⑴和1210(6)。證S4(3)：①②證S4(3)：①②?口?一??③?口?―證S4(4)：①口?->?口?②□□?—□?口?③□?一口?口?證S4(5)：①□?□?一口?②□?一□?□?T,USRMoS4(2),RERT。，USRMS4(l),RERS4(3),RMS4(4),RPC證84(6)：據(jù)S4(5)和1210(6)。證84(7)：①?口 To②口RM③口一□?口 4

［證明2：；S4(7)是S4(3)的逆對偶公式，，據(jù)逆對偶定理1.2.10(4)立得。］證S4(8)：①□(□p-?g)—K②□(口/>―>q)——>CJq S4(1)>RER(3)設(shè)皿{4}1S4B。則存在8”…，B"是S4中從到8的推演。只須證：在S4中，(☆)0卜□/—>8" 對每一施歸納于IWiW"。在此我們只考慮不平凡的情況，其余情況請讀者補充：存在/Vi使得8,從易據(jù)RN得到。據(jù)歸納假設(shè)，.,.據(jù)RM,01-口口/1—□易。.?.據(jù)4,01□/—?口鳥，0H口工一冊T據(jù)上面定理的(2),易得：推論F列模態(tài)符串的序?qū)ο鄬4等價：<oo,o>,<?口?口,?□><>T定義A的模態(tài)度Deg(4)定義如下：①②③④Deg(p?)=0,對每一n<co；①②③④Deg(-iB)=Deg(B)；Deg(^A0=max{Deg(B),Deg(0),Deg(Q^)=Dcg(^)+lo(2)稱/是"度公式<=>Deg(Z)="；(3)模態(tài)符串，的模態(tài)度Deg(/)定義如卜：Deg(O)=0；Deg(->/)=Deg(，)；Deg(□/)=Deg(^)+1.(4)稱/是〃度模態(tài)符串=Deg(/)=〃。T說明：易見純模態(tài)符串的模態(tài)度就是它的長度，且Deg(O/)=Deg(/)+k定義任給模態(tài)符串/和人(1)稱。相對S可歸約于#，記作/fs/，=0使得Deg(0)<Deg(/)。稱/相對S可歸約<=>存在0使得夕一s步。(2)稱/相對S可歸約于8oDeg(8)<Deg(4)且(3)稱，相對S吸收實T說明：(一)在不致混淆之處我們省略“一s”的下標(biāo)S。(二)據(jù)上述定義，Modal(S)及示相對S不可歸約的模態(tài)符串的個數(shù)。據(jù)1.3.14,我們有：S4的歸約定理相對S4,我們有下列歸約關(guān)系：□□f口，口?口?一口?,OO-O,?口?口一?口。T1.3.18定理Modal(S4)^14o證明：據(jù)1212(3),只須證S4至多有下列不可歸約的標(biāo)準(zhǔn)模態(tài)符串：(!(口?口??口nonOno-i-)□-nO->□<> -1<>□->□<>□ ->?口?我們先考慮上面一排。首先我們將它們編號如下：(1)% (2)口， (3)?,(4)口?, (5)?口，(6)口?口， (7)ODO.易見(1)是惟一的0度模態(tài)，(2)和(3)是兩個1度模態(tài)。在(2)和(3)上疊加一個模態(tài)符(可加在前面也可加在后面)，我們至多有4個不可歸約的2度模態(tài)符串：(8)口口，(9)oo,(10)no,(11)on,據(jù)歸約定理,(8)和(9)分別可歸約為⑵和(3)。在(10)和(11)上疊加一個模態(tài)符(可加在前面也可加在后面)，我們至多有6個不可歸約的3度模符串：(12)□□<>, (13) (14)口?口，(15)口??, (16)??口， (17)?口口。據(jù)歸約定理，(12)和(15)可歸約為(4),(16)和(17)可歸約為(5)。在(13)和(14)上疊加一個模態(tài)符(可加在前面也可加在后面)，我們至多有6個不可歸約的4度模態(tài)符串：(18) (19) (20)?口?口，(21)OOOO,(22)□□<>□, (23)據(jù)歸約定理，(18)可歸約為(4),(19)和(21)可歸約為⑺，(20)可歸約為(5),(22)和(23)可歸約為(6)。這樣，在S4中沒有不可歸約的4度純模態(tài)符串，從而(I)S4至多有7個不可歸約的純模態(tài)符串。在上述7個純模態(tài)符串前加上下證：(II)S4沒有形如?ASA的內(nèi)定理。假設(shè)(【I)不成立，則和都是S4的內(nèi)定理，易證「夕/和，T都是S4的內(nèi)定理，矛盾于S4的協(xié)調(diào)性(參見1.1.16(1))。據(jù)(I)和(11),易見S4至多有14個不可歸約的模態(tài)符串。T說明：(一)后面我們將證明Modal(S4)=14。Modal(S4)=14最早由Parry在1939年證明，讀者可以參見Segerberg的口971](/?.59)。(二)在上述證明最后部分，我們實際證明一個更概括的命題：(ir)任一協(xié)調(diào)系統(tǒng)都沒有形如灰4c「d/的內(nèi)定理。(三)相對S4,不可歸約的純模態(tài)符串有下列關(guān)系：其中。一步表示-S4如f/：□-□on-onIIiI00-000i i0 ??說明：第1行的第1個f據(jù)S4(3)和逆對偶定理1.2.10(4),第1行的第2個一和第2行的左邊兩個I據(jù)T,第2行的第3個I,第3行的一和第5行的一據(jù)T。，第4行的右邊的I據(jù)S4(3)。下面我們來考慮S5,這個系統(tǒng)比S4更有意思。1.3.19定理下列是S5的內(nèi)定理。S5(l)?一口?,S5(2)口一?口，S5(3)4,(從而S4qS5),S5(4)□(pr□])6口〃丫口q,S5(5)□(pvO^)<-^DpvO^,S5(6)O(p八S5(7)?(/7人口9)10。八口幻S5(8)B,(從而BcS5),S5(9)G,(從而S4.2cS5)o證明：證S5(l)：①?一口?5②口?7?T,US③?一口? ①，②，RPCffiS5(2)：據(jù)S5⑴和1.2.10(6)。證S5(3)：①口一?口②?口一□證S5(3)：①口一?口②?口一□?口③口一口?口④口一□口證S5(4)：To,US5,US①，②，RPCS5(2),RER①□(pvD^)—>D/?vOUq②口①"口夕)一口〃丫□夕③口,丫口口夕―>口9丫口夕)④Dpv□夕一口小口夕)⑤口伽\/口夕)<->口口口9證S5(5)：①口3/口?[)一口夕\/口<>4②□(pvO^)<-^DpvO^證S5(6)：(T)口(一口一?[)<->口一ipv口一?夕K(4),US①，S5(2),RERM(5),US(3),S4(l),RER②，④，RPCS5(4),USS5(l),RERS5(4),US②③④證①②證①②③證①②②③④證①②證①②③證①②―iLJ(—ipvEJ-—i(LJ->pvLJ―>q) RPC?TlpvrOq-OpvrOq) LMC?(pAOg)cOpAOg RER5(7)：?(/^?□/6?pAOdg S5(6),US?(pAdg)-OpAC]g S5(2),RER5(8)：p—>0/2 To?「—>口?/? 5pTfJOp ①，②，RPC5(9)：□一?D?□一口?S5(2),S5(l),RERH1.3.20S5的歸約定理(1)相對S5,我們有下列歸約關(guān)系：(☆)DD^D, <>□-□, □?一?,從而在S5中沒有不可歸約的2度模態(tài)符串，；.\10(1叫55)《6。(2)模態(tài)度大于1的公式相對S5可歸約于?模態(tài)度小于等于1的公式。證明：⑴據(jù)S4的歸約定理(1.3.17),S5(l)和S5(2),易見(眾)成立，...在S5中沒有不可歸約的2度模態(tài)符串，.?.在S5中不可歸約的標(biāo)準(zhǔn)模態(tài)符串至多有0, □, O?-1> ]□, —>?。，Modal(S5)W6。》參見1.3.16(2).(2)令4是模態(tài)度大于1的公式，我們用下列方法進(jìn)行歸約：用縮寫定義和RER消去T和c；用LMC等把「內(nèi)移至句符前面：③用(1)給出的歸約關(guān)系，把疊加模態(tài)符串歸約為非疊加模態(tài)符串：④若據(jù)上述步驟得到的公式小還不是1度公式，則再據(jù)下列步驟進(jìn)行歸約：設(shè)A\含子公式口8使得Deg(8)>0。情況18=CaO：據(jù)R和RER內(nèi)移口于8中。情況2B=CyD：子情況1C和。至少有一以口或?開頭：則據(jù)S5(4>-S5(5)和RER內(nèi)移□于8中。子情況2C和。都沒有以口或?開頭：???Deg(8)>0,，Deg(C)>0或Deg(￡>)>0。據(jù)本子情況的設(shè)定，我們不妨設(shè)C=CiaC2o據(jù)RER和R,□((C!aC2)vD)^□(C,vZ))a□(C2vD)o再據(jù)RER內(nèi)移□于8中。若在經(jīng)過上述內(nèi)移后的合取肢或析取肢的模態(tài)度還大于1，則再據(jù)③或④進(jìn)行歸約，最后總能使B前面的口被B中的模態(tài)吸收。?設(shè)小含子公式使得Deg(8)>0。情況18=Cv0：據(jù)R。和RER內(nèi)移?于8中。情況2B=C八D：子情況1C和。至少有一以口或?開頭：則據(jù)S5(6)-S5⑺和RER內(nèi)移?于B中。?參見1.3.16(3).子情況2C和。都沒有以口或?開頭：?.,Deg(8)>0,Deg(C)>0或Deg(0>O。據(jù)本子情況的設(shè)定，我們不妨設(shè)C=C,vC2?則據(jù)RER和Ro,1O((CivC2)a￡>)<->O(CjaD)vO(C2aD)?再據(jù)RER如上內(nèi)移?于8中。若在經(jīng)過上述內(nèi)移后的合取肢或析取肢的模態(tài)度還大于1,則再如③或④進(jìn)行歸約，最后總能使B前面的?被B中的模態(tài)吸收。重復(fù)上述步驟，最終我們能證明(2)。注意：我們在歸約過程的開始、中間或結(jié)束遇到的公式有的可以直接歸約為模態(tài)度為0的公式，例如，重言式或矛盾式的代入特例。T說明：(一)據(jù)上述(1),對系統(tǒng)S5來說，疊加模態(tài)符串不會增加新東西。更仔細(xì)地說：若。是疊加純模態(tài)符串，則Oi…O”相對S5可歸約于?！被蛘哒fO“吸收…0“一|。(二)以后我們要證明K,D.T和B沒有上述歸約定理。,.,口4—/和是S5的內(nèi)定理，推論相對S5不可歸約的純模態(tài)符串是一個線序：說明：以后我們證明Modal(S5)=6。下面我們證明S5的模態(tài)合取范式存在定理。定義(1)稱l是1度模態(tài)簡單析取oA形如4V…v4,使得對每一1WiW",Deg(4)=0，或Deg(4)=l且4形如口8或?以這時也稱4是4的析取肢。(2)稱/是1度模態(tài)合取范式<=>A形如4A…使得對每一lWiW〃，4是1度模態(tài)簡單析取。這時也稱4是/的合取肢。T說明：易見任何1度模態(tài)合取范式4的Deg(Z)e{0,1}。1.3.23例(1)下列公式是1度模態(tài)合取范式：p,DpA^vr),(□pvOgvr)A(OpvO(qw))。(2)下列公式不是1度模態(tài)合取范式：□□p,(□(pvO^)vr)Ar,DpA(Orv(^aO/?))?T定理(1)任給公式人存在公式8=8IA…a8”使得對每一14i《"，M是由形如5,.|>???>Bh