模態邏輯

　　數理邏輯的一個重要分支，研究“必然”、“可能”、“不可能”和“偶然”等所謂“模態”概念的邏輯學說。這裏“模態”一詞是英語詞“modal”的音譯，而“modal”又來自“modes of truth”(真的方式)中的“modes”一詞。

　　模態概念的研究可一直溯源到亞裡斯多德時期。在中世紀時又有人進行這種研究，直到19世紀末至20世紀初才有位叫H.麥科爾的邏輯學傢邁出瞭近代模態邏輯研究的第一步。他在他的著作中第一次指出瞭所謂謂“蘊涵佯謬”。但是，麥科爾沒有提出任何公理。因此，他的系統和當代的研究是迥然不同的。現代模態邏輯的公認奠基人是C.I.劉易斯。從1912年，即B.A.W.羅素和A.N.懷特海的巨著《數學原理》出版後的兩年起，劉易斯發表瞭一系列論文和著作，對上述巨著中的“實質蘊涵”提出異議，其理由和麥科爾一樣，即對“蘊涵佯謬”深為不滿。他於是在上述巨著的基礎上引進新的公理系統，並通過引進模態命題算子在其中加入瞭模態概念。以所謂“嚴格蘊涵”取代實質蘊涵以圖消除“蘊涵佯謬”。但是劉易斯沒有預料到，在他提出的幾個系統中同樣有著類似於實質蘊涵佯謬的“嚴格蘊涵佯謬”，問題仍然沒有解決。不過劉易斯所提出的五個模態系統S1～S5，特別是S4和S5卻是最著名和研究得最多的模態系統。他與C.H.蘭福德合著的於1932年出版的名著《符號邏輯》仍然是現代模態邏輯學的經典著作。

　　模態邏輯和古典二值邏輯一樣，也分為命題邏輯與謂詞邏輯兩個層次：即模態命題邏輯和模態謂詞邏輯兩層次。20世紀50年代以前邏輯學傢們基本上隻對模態命題邏輯有興趣，因為各式各樣的命題模態邏輯系統有著極為豐富的邏輯問題。研究量詞模態系統（即模態謂詞邏輯）的人極少，成果也不足道。50年代末以來，特別是1959年S.A.克裡普克提出關系語義概念並證明S5^*(即帶量詞的S5)對於適當的關系模型概念為完備的之後，從事後一方面研究的人才多起來，所獲成果也甚為顯著和豐富。

　　一般認為模態邏輯有三個主要研究方向或方法，即：公理學的、語義學的和代數學的方向或方法。50年代末以前盛行的是公理學研究，即提出各種各樣的模態命題系統，研究它們與熟知系統的關系；研究它們有多少個模態辭（或更一般地說，有多少個含固定有限個變元的模態函數）；采用特定的(αdhOс)真值表以區分各系統；論證出發點不同的系統的演繹等價性（即包含同樣的定理）等等。關於出發點主要分兩大類：一類是把模態命題邏輯建立在古典二值系統PC之上，在PC的命題聯結詞基礎上再加入模態算子如“∟”（指“必然”，通常多用“□”表示）或“M”(指“可能”，通常多用“◇”表示)作為一元命題算子，相應地增加一些新的形成規則。在公理系統方面先列出一組完備的PC公理及推理規則，再加入若幹條含∟或M的公式為附加公理，加入一些新的模態推理規則如“

”(即所謂 N規則)之類。在G.H.von賴特1951年的專著《模態邏輯》一書附錄2中就是采用這種方式建立三個系統 M， M′和 M″的，已知 M即為R.費斯於1937年提出的系統 T，而 M′和 M″則分別是劉易斯的系統 S4和 S5。另一類可以用劉易斯和蘭福德的《符號邏輯》一書中給出 S1～ S5 的方式為代表；在那裡，全部公理沒有一條屬於 P C，但卻可以證明 P C中的全部定理（即重言式）均是 S1～ S5 中各系統的定理。屬於這一類型的還有L.西蒙斯1953年提出的 S3、 S4 的新公理系統，他同時還證明瞭新公理系統中各條公理都是獨立的，對 S5他也提出瞭新系統，可惜不能證明其中公理的獨立性。為瞭把 S1～ S5(特別是 S1～ S3) 的公理系統化歸入前一類型，E.J.萊蒙1957年提出瞭4個系統 K1～ K4，四者的公理系統均屬前一類型，並證明瞭它們分別演繹等價於 S1～ S4。

　　關於語義學和代數學方向或方法更確切地說應是指關系語義學和代數語義學方向或方法如果說前者是1959年前後以克裡普克為主建立的，則後者早在40年代即已由J.C.C.麥金西和A.塔爾斯基提出。麥金西和塔爾斯基的代數方法當時主要針對S2和S4；但是萊蒙在1966年指出，上述代數方法可以推廣到大量的模態命題系統上。首先建立每個被討論系統S的正則真值表與某種類型代數間的聯系，更確切地說，稱S為正則的，如果對S而言，實質等價“≡”是模態合式公式之間的相對於命題聯結詞和模態算子而言的合同關系。這時疊合等價公式而得的代數l_s稱為S的林登鮑姆代數。l_s的任何具有兩個以上元素的同態像均稱為S代數。特別地，若S分別為T，S4和S5，則相應的S代數分別為“外延代數”，“閉包代數”和“一目佈爾代數”。容易證明l_s以其中單位元為惟一指定元是S的特征真值表，亦即，

當且僅當 α在 l _s上永真，由此可以證明系統 S具有有窮模型性質，因此 S的判定問題是可解的。最後，可以限於討論有窮 S代數，並證明可以把這些代數表示為基於某一給定集合的一切子集的集合上的代數的定理。此種表示導出瞭代數語義方法和關系語義方法間的聯系，從而立即可得關系語義完備性的結果。萊蒙還斷言，這些討論可以推廣到模態謂詞邏輯上，並準備寫專文論述；可惜他的願望未曾實現便溘然長逝瞭。模態謂詞邏輯的代數語義學及代數完備性對 S4和 S5 而言有人做過工作。對於 S4的情形結果不夠滿意；而對 S5的情形結果甚好，而且現已發現其與克裡普克1959年得到的對於 S 5 ^*而言的關系語義完備性定理可以互推。後者似乎部分地(即就 S5而言)實現瞭萊蒙的遺願。（見 模態模型論）

　　模態邏輯在哲學、計算機科學(特別是程序理論)和數理邏輯學的另一分支證明論中均有重要的應用，而且它目前仍是數理邏輯各分支學科中最活躍的領域之一。

　　

參考書目

　C.I.Lewis and C.H.Lanford，Symbolic Logic，2nd ed.，Dover，New York，1959.

　G.H.von Wright，An Essay in Modal Logic，North Holland，Amsterdam，1951.

　G.E.Hughes and M.J.Cresswell，An Introduction to Modal Logic，Methuen，London，1968.

　G.Boolos，The Unprovability of Consistency，AnEssay in Modal Logic，Cambridge Univ.Press，Cambridge，1979.