模态逻辑是一个多方面的学科，它起初在哲学中得名，在很长一段时间中作为“必然和可能的逻辑”而被人所知。但是，把模态逻辑视为关于“可能”和“必然”的逻辑至少在20世纪60年代末就已经过时。“模态语言是研究关系结构的一种简单但富于表达力的语言”、“模态语言为关系结构提供一种内部的、局部的视角”、“模态语言不是孤立的形式系统”，这就是关于模态逻辑的新观点（这种观点有时称为“阿姆斯特丹观点”）。新观点不再把模态逻辑视为任意种类的形而上学系统，而是作为研究行为、知识以及我们周围任何其他具有良好结构的具体事物的逻辑形式系统。

　　　　一　关系结构无处不在

关系结构是由一个称为论域的集合和定义于论域之上的关系组成的序对。

基本模态逻辑的一个克里普克模型只是一个各种不同的（可达）关系定义于其上以及对原子信息进行真值指派的可能世界的集合，是一个有向的多重图；因此克里普克模型是一阶模型论意义上的非常简单的关系结构，一类被用来解释一阶和二阶经典语言的结构。此时，在克里普克模型中，把可能世界视为某种状态(state)比较恰当，而可达关系则包含着可以从一种状态过渡到另外一种状态的可能运动的意思。

关系结构无处不在，在许多领域都是非常有用的工具：所有标准的数学结构都是关系结构，计算机科学家可以把加标转换系统看成是一种关系结构，人工智能研究者可以把各种不同的时间图看成是关系结构，描述逻辑学家把个体网络视为关系结构，哲学家则用关系结构来描述“可能世界”及其之间的联系。作为关系结构的克里普克模型是基本的模拟工具，模态逻辑广泛应用的一个原因在于，无论对于什么样的关系结构，只要研究者感兴趣，都可以运用模态逻辑来表达和进行推理。另一方面，关系结构是经典模型论的基本概念，因此，我们不必一定要用模态逻辑来对它进行研究，所有在关系结构上进行解释的逻辑，如一阶（或者二阶）逻辑、无穷逻辑或者不动点逻辑等等，都可以用作研究工具。而且，现在很少有模态逻辑学家把模态逻辑看作是通过“可能世界语义”来研究“内涵现象”的非经典逻辑，相反，自从20世纪70年代以来，模态逻辑被当作是各种经典逻辑的子系统来研究。那么，为什么还需要模态逻辑？原因大致有三个：第一是模态语言的简单性。在标准翻译下我们看到，模态词概念隐藏了约束变元，得到一个紧凑的、容易阅读的形式表示。像“可能”和“必然”这样的经典模态算子在根本上是一种宏观的(macros)算子，比如一元的“可能”算子就把“在某个可达的世界上寻找我们感兴趣的信息”这样一个经典的量化形式压缩成一个更为简单的算子记法——带“可能”算子的模态公式；时态运用中的Until算子把复杂的量化方式压缩成一个简单的二元算子格式；而命题动态逻辑的〈π[*]〉算子“通过有穷多的π转换以寻找我们感兴趣的信息”把对关系的自返传递闭包上的量化压缩成一个一元算子。总而言之，模态逻辑的游戏就是寻找灵活的算子，当进行不同的组合时，可以产生表现良好的和有用的经典逻辑部分。此外，就有效式的证明系统来讲，不管是公理系统还是后承演算、自然推演等其他证明形式，模态推演是一种记法清晰的简单推理。比如说，普遍有效式的极小模态逻辑公理系统为：(1)命题逻辑公理；(2)可能算子用必然算子定义：；(3)模态分配公理：(4)必然化规则：若定理则是定理。如果把必然算子看成是全称量词把可能算子看成是存在量词，这一系统就好像是一阶逻辑的一个标准公理系统，但是它排除了那些对自由和约束带技术性边款的公理：。第二在于可计算性方面。众所周知，一阶逻辑是不可判定的，而正规模态逻辑却是可判定的。第三则是模态语言研究关系结构的“透视”观点——模态语言为研究关系结构提供了一种内部的、局部的观点。我们在模型内部特殊的状态（即“当前状态”）中对模态公式进行赋值，模态公式就像是一个微型的机器人，在、也仅在当前状态以及当前状态可达的状态之间移动以考察模型。这是最关键的模态直观，模态语义学中可能世界之间基本的等价概念——双仿(bisimulation)——就来源于此。模态语言的表达能力通过两个模型之间恰当的双仿概念来衡量。两个模型M和N之间的一个双仿是这两个模型的两个状态m∈M和n∈N之间的一个二元关系。如果m和n是双仿的，指其满足以下三个条件：(1)m和n满足相同的命题变元，即“原子一致”；(2)若m可达m′，则有一个状态n′使得n可达n′且m′和n′是双仿的；(3)若n可达n′，则有一个状态m′使得m可达m′且m′和n′是双仿的。这一“原子一致”和后面两个“弯弯曲曲(zig-zag)”条件使得双仿成为一个自然的“过程等价”概念——计算机科学家也独立发现了这一概念。双仿是两个模型的论域之间一种很自然的性质，通常的生成子模型、有界态射和不相交并等都是特殊的双仿。模态公式是双仿不变的：如果两个模型之间有一个双仿且分别属于这两个模型的状态m和n是双仿的，那么m和n满足相同的模态公式。这一命题的逆仅对于带任意无穷合取和无穷析取的模态语言或者特殊模型的模态语言成立。例如，如果状态m和n在有穷模型M和N中满足相同的模态公式，那么在M和N之间有一个双仿使得m和n是双仿的。当然，还有更强的可定义性结果。例如，对于任意的带点模型(M,s)，总是存在一个无穷的模态公式，这个公式只在那些与(M,s)“双仿的”模型中为真。但是，并非所有的一阶公式都是双仿不变的。在对应语言中，只包含一个自由变元的一阶公式其双仿不变性的充分必要条件是该公式等价于一个模态公式的标准翻译，换句话说，模态逻辑就是刻画一阶逻辑的双仿不变片断的一种简单记法。双仿概念是从模型的层面来研究模态逻辑。逻辑要反映一些不依外在的变化的本质，而模型不堪此任，原因就在于它还依赖具体的真值指派和赋值。将这些具体的附加物去掉就是我们所想要的——标架(frame)！枸德布赖特—托马森(Goldblatt-Thomason)定理从标架层面指出一阶语言与模态语言之间的关系：一个一阶可定义的标架类是模态可定义的当且仅当这一标架类对取有界态射像、生成子标架和不相交并封闭并且反射超滤扩充。所谓标架类K反射超滤扩充，指的是如果标架F的超滤扩充在K中，那么标架F本身也在K中。所有这些还表明，模态语言并不是一类孤立的形式系统。此外，模态逻辑的这一内部的、局部的观点不仅对于模态逻辑的许多重要的数学性质意义重大，而且使得模态表示在时间逻辑、特征逻辑和词项逻辑等许多应用当中成为理想的工具。

模态语言有标架的和代数的两大类解释。历史上先有代数的解释，后有成熟的标架解释。但是由于标架解释非常直观，而且不需要有太多的代数背景即可被人们理解和接受，因此一经出现就广为流行，而且正是由于它的出现，模态逻辑在20世纪60年代以后得到了极大的发展。一个模态逻辑是指一个模态公式集，它包含所有的命题重言式，并且对于分离规则和代入规则封闭。而且我们一般特别关注的是一类通常所说的正规模态逻辑，这是还包含极小模态逻辑K并对必然化规则也封闭的一类模态逻辑。一般来讲，可以从两个方面来获得一个模态逻辑：一个是句法层面的；一个是语义层面的。值得一提的是，一类模型下有效的公式未必是一个模态逻辑，一类标架下有效的公式却一定是一个模态逻辑。所以，此处也说明模态逻辑在本质上是反映标架的。模态研究可以从句法角度先从一些有意思的公式开始得到一个模态逻辑系统，然后研究这个系统所刻画的标架是什么，或者说是否有一类标架，其上有效的公式恰好就是该模态逻辑。另一方面，也可以从语义角度出发得到一个模态逻辑，然后试图寻找一个与之匹配的简单的句法系统（公理系统、表列系统等）。这些就是模态逻辑完全性理论所研究的内容。模态逻辑完全性理论中最常用的方法是典范模型方法。为了证明一个正规模态逻辑相对于具有某些性质的一类标架是完全的，只需要证明其公理对于该类性质是典范的即可。通过这种方法可以解决一批模态逻辑的完全性问题，如常见的T,S4等等。这种证明方法的关键之处是要使得典范标架具有某一性质。其实这是一种过高的要求。由于某些性质不可能为典范标架所具有，此时可以采取展开(unravelling)等多种策略使得典范标架的局部具有这些性质，从而获得完全性结果。但是，有些模态逻辑系统事实上是没有标架与之对应的，如K[,t]ThoM。20世纪70年代初标架不完全性结果的发现以及70年代末理论计算机科学中模态语言的普遍采用，这两者极大地改变了模态逻辑的进程。理论计算机科学的影响从根本上改变了模态语言可以用于什么以及如何应用的前途。不完全性结果则是无法根除的，这迫使逻辑学家们从根本上重新评价模态语言到底是什么：作为研究标架的工具，模态语言在根本上是一种伪装的一元二阶逻辑，其本质是高度复杂的。为了充分地理解模态语言，需要精确地在逻辑世界中为它们定位。在随后的许多年中，模态语言从泛代数和经典模型论的角度得到了广泛的研究。枸德布赖特引入泛代数来研究模态逻辑，发展出模态对偶理论（赋有拓扑结构的关系结构与赋有带算子布尔代数的关系结构两者之间的系统研究）。他和托马森证明了泛代数的概念与结论可以用来产生一些有趣的模态结论，最著名的例子是把柏格霍夫(Birkhoff)的簇定理运用到带算子布尔代数而得到的模态可定义标架类的、模型论刻画的枸德布赖特—托马森定理。布洛克(W.J.Blok)的工作进一步使用了代数方法。泛代数成为完全性理论研究中一个关键性的工具，代数语义学的复兴是这一时期最为持久的遗产之一。

对于经典命题逻辑其实就有代数解释，即布尔代数。而模态逻辑的代数语义就是这种布尔代数的一种推广，即带算子布尔代数。关于代数语义，模态逻辑有漂亮的代数完全性定理：任意一个正规模态逻辑公理系统相对于公理在其上有效的带算子布尔代数类既可靠又完全。此外，在代数语义中还有一个重要的约翰逊—塔尔斯基(Jónsson-Tarski)定理：任意一个带算子布尔代数可嵌入到一个复合代数中，这个复合代数其实就是该布尔代数的典范的嵌入代数，即它的超滤标架的复合代数。借助它及代数语义下的典范模型——林顿巴姆—塔尔斯基(Lindenbaum-Tarski)代数，立即可以得到正规模态逻辑公理系统相对复合代数的完全性结果。在从一个标架构造一代数、从一个代数构造一标架的这些转换中，有许多重要的关系值得一提。例如：如果F是G的生成子标架，那么F的复合标架是G的复合标架的满射的像；如果G是F的满射的像，那么G的复合代数是F的复合代数的子代数；等等。利用这些对偶理论，我们也可以用纯代数的方法证明前述的枸德布赖特—托马森定理。

无论是标架语义，还是代数语义，这两种语义都是以一个集合为基础集(carrier)，在其上再定义一些关系或者是运算，因此可以把这两种语义都视为一种关系结构。模态逻辑是以构造合理的蕴涵为开端、发展到以研究模态词为目的的一种非经典逻辑，再到今天被视为研究关系结构的一般理论，人们对其认识正在一步一步地深化，模态逻辑本身也在不断地壮大发展。

　　　　二　模态逻辑的扩充和应用

模态逻辑的新观念来源于20世纪60年代以来模态逻辑两种不同的发展。其一在于模态逻辑中起先意想不到的广泛应用。这一应用肇始于时序逻辑和认知逻辑，然后发展出空间逻辑、（行为的）动态逻辑，现在又有语法推导、广义量词、博弈和人工智能中概念描述的模态逻辑。此类“逻辑”都是特殊类型可达关系的不同模态理论，这些应用为模态逻辑的发展提供了新的动力，而本体论则似乎不再是灵感的源泉。第二个影响来源于模态逻辑内部。从一个方面讲，模态逻辑是一种典型的、经典逻辑加新算子的扩张；从另一个（更为深刻的）方面来讲，模态逻辑又都是经典语言的片断，在可表达性和推理的关系结构的自然谱系中，这一观点是一块里程碑。

新的模态逻辑观点带来了两个正面效果。首先，它丰富了我们对模态逻辑的理论理解，新的技术工具如标准翻译和双仿被发展出来。第二，也是更重要的，它鼓舞了模态逻辑学家们去充当“逻辑工程师”，为适应某些特殊的应用而把逻辑工艺化，这导致了许多“扩充模态逻辑”的诞生。模态逻辑内部、局部的“透视”观点源于模态逻辑的数学性质，同时在许多应用当中也使模态表示成为理想的工具，经典的例子是时序逻辑。在模态词为F和P的双模态语言中，〈F〉表示“在将来某一状态中”，而〈P〉解释为“在过去某一状态中”；为反映这一时序意义，一般的做法是把这一语言放到标架（T,＜）上进行解释，（T,＜）可以合理地看成是“时间流”。例如，如果把时间看成是一个分叉的结构，（T,＜）就可以是一种树形结构；如果需要线性的时间观，则（T,＜）又可以是带通常序的整数（Z,＜）。此时，可达关系RF是〈，而RP是其逆，即保证〈F〉沿着时间流朝前看，〈P〉朝后看。时序逻辑公式“〈P〉汤姆失去知觉”为真当且仅当我们可以从当前状态朝后看见一个状态，在其中汤姆失去知觉；与此类似，时序逻辑公式“〈F〉汤姆失去知觉”要求我们寻找一个将来的状态，在其中汤姆失去知觉。因此这两个公式的作用分别和自然语言中的句子“汤姆已经失去知觉”、“汤姆将要失去知觉”相同：它们没有指出汤姆失去知觉的绝对时间，而是相对于说话时间来确定。也就是说，自然语言所刻画的人类生活在时间中可以用模态语言清楚地模拟出来。推而广之，我们也可以把时序状态看成是时间段，并且添加诸如〈SUB〉和〈SUP〉等分别表示“在当前状态的某一子时段中”、“在包含当前状态的某一时段中”这样一些新的模态词。然后，新的时序逻辑公式〈SUB〉〈F〉〈SUP〉p是说：“通过寻找包含当前状态某个子时段的将来的某一时段，可能找到一个p在其中为真的状态”。这一模态逻辑可以从“内部”来研究一个线性时间流上两个封闭时段之间所有可能的关系。另外，近年来在对“安保片断(guarded fragment)”的研究中，研究者已经证明可以把局部性直观引入到经典逻辑中来，发掘出来许多一阶（或其他）经典逻辑以前未被认识到的可判定片断。

“数学必然”——可证性——的模态分析把模态逻辑引入到数学基础中来，模态逻辑的拓扑语义和代数语义的发现又把它与一般拓扑和泛代数联系起来，而一阶逻辑可以被视为命题模态逻辑的事实则开启了经典数理逻辑中的“模态观点”。但是，当模态逻辑为研究计算机程序的状态转换系统、知识表示的语义网络、语言学—语言中的属性值结构等各种不同的关系结构提供了具有充分表达力和能行性的语言时，最令人惊奇的变化发生了。这一变化为模态逻辑在计算机科学、人工智能、语言学和数学本身打开了新的、丰富的和快速成长的应用领域。模态逻辑的当代应用并不是对以往既有概念和技术的例行运用，而是把一些意想不到的东西添加到基本的模态逻辑框架中。例如，命题态度（如知识）显示出与本体论模态词一样的逻辑行为：认知算子“主体i知道（用符号表示成K[,i]）”就像是一个全称模态词，断定“在i所有认知不可区分的情境中为真”。其他认知命题态度如相信(belief)也是如此。由此看来，可达性对主体来说常常是等价关系。这类语言表达的基本认知命题经常在自然语言中使用：“主体i知道是否属实”，相应地，刻画认知算子的公理也以一种新面貌出现：。但是，现实生活中的认知行为往往发生在不同的主体之间：。这就需要“多主体的认知逻辑”。多主体认知逻辑的一个核心概念是“公共知识”，在技术上，公共知识按照如下方式起作用：“：经由对于G中的参与者来说不确定关系的任意有穷链可达的每个世界中，成立”。模态逻辑还被广泛地应用于人工智能、语言学和数学等领域，或在这些领域中被重新发现，如描述(description)逻辑、语境(context)逻辑、范畴语法(categorical grammar)和特征(feature)逻辑等就是这些应用或者重新发现的成果。由此也可以看出模态结构（或者说关系结构）自然而然地出现在广阔的学科领域。为了提供能行的形式化来研究时间、空间、信念、行为和义务等概念，人们在过去的几十年中构造了大量的、带各种各样模态算子的时序、空间、认知、动态、道义等系统。但是，现代应用常常需要相当复杂的形式模型和相应的语言以反映应用领域的不同特征。例如，为了分析多主体分布式计算机系统的行为，就需要既包含刻画主体知识的认知算子又包含刻画这些知识在时间中发展的时序算子。换句话说，我们必须把认知逻辑和时序逻辑恰当地组合起来。借用几何术语，可以把得到的混合称为一个“多维模态逻辑(many-dimensional modal logic)”。带着不同的动机，计算机科学、人工智能、代数逻辑和模态逻辑领域的研究者们独立或者联合发展出来这样一些多维的混合物，然而，它们的算法性质却和它们那些众所周知的、行为良好的一维组成部分大不相同。特别是判定算法复杂性的增加更是惊人，甚至得出不可判定性；两个相当简单的、可有穷公理化的系统在混合之后甚至不是递归可枚举的；等等。模态语言还在它们原先的模型上得到丰富，一种流行的“逻辑扩充”是添加“全称模态词”在所有世界上为真（不管具有可达关系与否）。新的模态词增加了表达能力，我们可以用此来叙述某些“全局事实”，如模型的一个区域被全部包含在另一个区域之内。标准技术在全局语言中可以推广，语言｛□,U｝就具有“全局双仿”的性质，而且其极小逻辑也是可判定的，不过有效式的复杂性增加至EXPTIME。在模态逻辑早期，并没有对基本模态语言进行扩充，原因在于这样做会改变游戏规则，颠覆基本模态逻辑中许多可望不可及的事情。另一个很好的例子就是对“可能世界’’进行命名。模态语言中可能世界名字的引人为模态逻辑的实际使用和模态元理论都带来了极大的便利。例如，新的语言提高了对标架的表达能力，禁自反性()在基本模态语言中没有公式与之对应，现在可以用扩充的模态语言简单地表示成“”（其中可能世界的名字i命名了标架中惟一的一个世界）。这一扩充的模态语言一方面提高了表达能力；另一方面又没有增加计算复杂性。

所有这些扩充之后的语言依然是“模态语言”，原因在于它们允许进行双仿分析，同时又保持了可判定性。

 

（原载《哲学动态》2005年12期）