关于模态逻辑介绍

[拼音]：motai luoji

[外文]：modal logic

数理逻辑的一个重要分支，研究“必然”、“可能”、“不可能”和“偶然”等所谓“模态”概念的逻辑学说。这里“模态”一词是英语词“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 的方式为代表；在那里，全部公理没有一条属于PC，但却可以证明PC 中的全部定理（即重言式）均是 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 而言，实质等价“呏”是模态合式公式之间的相对于命题联结词和模态算子而言的合同关系。这时叠合等价公式而得的代数ls称为S 的林登鲍姆代数。ls的任何具有两个以上元素的同态像均称为S 代数。特别地，若S 分别为 T，S4和S5，则相应的S 代数分别为“外延代数”，“闭包代数”和“一目布尔代数”。容易证明ls以其中单位元为惟一指定元是S 的特征真值表，亦即，当且仅当α在ls上永真，由此可以证明系统S 具有有穷模型性质，因此S 的判定问题是可解的。最后，可以限于讨论有穷S代数，并证明可以把这些代数表示为基于某一给定集合的一切子集的集合上的代数的定理。此种表示导出了代数语义方法和关系语义方法间的联系，从而立即可得关系语义完备性的结果。莱蒙还断言，这些讨论可以推广到模态谓词逻辑上，并准备写专文论述；可惜他的愿望未曾实现便溘然长逝了。模态谓词逻辑的代数语义学及代数完备性对 S4和S5 而言有人做过工作。对于S4的情形结果不够满意；而对S5的情形结果甚好，而且现已发现其与克里普克1959年得到的对于S5* 而言的关系语义完备性定理可以互推。后者似乎部分地(即就S5而言)实现了莱蒙的遗愿。（见模态模型论）

模态逻辑在哲学、计算机科学(特别是程序理论)和数理逻辑学的另一分支证明论中均有重要的应用，而且它目前仍是数理逻辑各分支学科中最活跃的领域之一。

参考书目

1. C.I.Lewis and C.H.Lanford，Symbolic Logic，2nd ed.，Dover， New York， 1959.
2. G.H.von Wright，An Essay in Modal Logic，North Holland， Amsterdam， 1951.
3. G.E.Hughes and M.J. Cresswell，An Introduction to Modal Logic，Methuen， London， 1968.
4. G.Boolos，The Unprovability of Consistency， AnEssay in Modal Logic，Cambridge Univ. Press， Cambridge，1979.