论可能世界的名字，本文主要内容关键词为：名字论文,世界论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
“可能世界”是模态逻辑语义学的核心概念，一般也可以称为“世界”、“点”、“状态”、“时间”以及“情境”等。模态语言本质上是研究通常一阶模型论意义上的关系结构的简单、且具有丰富表达力的形式语言，但是，传统的模态语言没有一种机制来指称关系结构中的个体并对其进行推理。以传统模态逻辑为基础，在句法中引入“可能世界的名字”作为第二类原子命题、引入相应的算子和约束词而得到的语言称为混合语言，这一语言既发扬了模态语言积极的一面，同时又克服了模态语言前述的重大缺陷。
本文首先介绍“可能世界的名字”引入的逻辑背景和主要思想，然后讨论引入“可能世界的名字”的意义。
一、模态逻辑背景
把模态逻辑视为关于“可能”和“必然”的逻辑，至少在20世纪60年代末就已经过时。模态语言是研究关系结构的一般工具。模态命题逻辑的一个克里普克模型只是一个各种不同的关系定义于其上以及对原子信息进行指派的世界的集合，是一个有向的多重图（或者加标转换系统），因此克里普克模型是一阶模型论意义上的非常简单的关系结构，一类被运用于解释一阶和二阶经典语言的结构。关系结构无处不在，在许多领域是非常有用的工具：所有标准的数学结构都是关系结构，计算机科学家可以把加标转换系统看成是一种关系结构，人工智能研究者可以把各种不同的时间图看成是关系结构，描述逻辑学家把个体网络视为关系结构，哲学家则用关系结构来描述“可能世界”及其之间的联系。作为关系结构的克里普克模型是基本的模拟工具。模态逻辑广泛应用的一个原因在于，无论对于什么样的关系结构，只要研究者感兴趣都可以运用模态逻辑来进行推理。
关系结构是经典模型论的基本概念，因此，我们不必一定要用模态逻辑来对它进行研究，所有在关系结构上进行解释的逻辑，如一阶（二阶）逻辑、无穷逻辑以及不动点逻辑等，都可以用作研究工具。而且，模态公式都可以翻译成等价的一阶公式，反之则不然，由此也可以看出模态语言在表达能力上弱于一阶语言。现在，很少有模态逻辑学家把模态逻辑看作是通过“可能世界语义”来研究“内涵现象”的非经典逻辑，相反，自从20世纪70年代以来，模态逻辑已经被看成是经典逻辑的子系统。
那么，为什么还需要模态逻辑？原因大致有三个。第一是模态语言的简单性。在标准翻译下我们看到，模态概念隐藏了约束变元，得到一个紧凑的、容易阅读的形式表示。像“可能”和“必然”这样的经典模态算子在根本上是一种宏观的（macros）算子，比如一元的“可能”算子就把“在某个可达的世界上寻找我们感兴趣的信息”这样一个经典的量化形式压缩成一个更为简单的算子记法——带“可能”算子的模态公式。第二在于可计算性方面。众所周知，一阶逻辑是不可判定的，而正规模态逻辑却是可判定的。第三则是模态语言研究关系结构的内部视角：模态语言为研究关系结构提供了一种内部的、局部的观点。我们在模型内部的特殊的可能世界（即“当前世界”）中对模态公式进行赋值，模态公式就像是一个机器人，在、也仅在当前世界以及当前世界可达的可能世界之间移动以考察模型。
这是最关键的模态直观，模态语义学中可能世界之间基本的等价概念——双仿（bisimulation）就来源于此。双仿是不同论域之间的一种很自然的性质，模态公式是双仿不变的。但是，并非所有的一阶公式都是双仿不变的，在对应语言中，只包含一个自由变元的一阶公式的双仿不变性的充分必要条件是该公式等价于一个模态公式的标准翻译，换句话说，模态逻辑就是刻画一阶逻辑的双仿不变片断的一种简单记法。从这一点来看，模态语言并不是一类孤立的形式系统。此外，模态逻辑的这一内部的、局部的观点不仅对于模态逻辑的许多重要的数学性质意义重大，而且使得模态表示在时间逻辑、特征逻辑和词项逻辑等许多应用当中成为理想的工具。
综上所述，模态语言是研究关系结构的一般工具，为研究关系结构提供了一种内部的、局部的观点，并且模态语言不是一类孤立的形式系统。这就是关于模态逻辑的新观点，这种观点有时被称为“阿姆斯特丹观点”。新的观点带来两个正面效果。首先，它丰富了我们对模态逻辑的理论理解，新的技术工具如标准翻译和双仿被发展出来。第二，也是更重要的，它鼓舞了模态逻辑学家们去充当“逻辑工程师”，为适应某些特殊的应用而把逻辑工艺化，这导致了许多“扩充的模态逻辑”的诞生：研究包含任意元关系的关系结构时引入多元模态算子，在可能世界序列中对公式进行赋值时推广到多维模态逻辑，等等。这些都是模态逻辑的优点。
但是，传统模态语言也有一个明显的缺陷：模态语言无法指称模型中的可能世界（或状态、时间、点、情境……）。例如：某事发生在这里，某物出现在那时，该世界具有性质q，点i拥有信息p，等等。这一缺陷对于许多应用来说非常严重，因为当对时间进行推理时，我们常常想对在特定时点或时段所发生的事件进行推理，而当我们进行词项推理时，我们常常需要对它们如何应用到特殊个体进行推理。在既要指称可能世界又不能破坏模态逻辑简练性的前提下，解决克里普克语义和模态句法之间这一不对称性的方法是“公式用作词项”。
二、公式用作词项
“公式用作词项”的基本思想是对模态语言的原子符号（即命题字母）进行分类，新的原子被用作可能世界的“名字”，用i，j等表示。两种类型的原子可以用通常方式进行组合而得到更复杂的公式，如：
〈π〉（i∧p）∧〈π〉（i∧q）→〈π〉（p∧q）（*）
其中p、q都是普通的命题变元，〈π〉是可能模态词。语义上每一个“名字”在任意模型中都在、且只能在一个世界上为真。通过只在某一个世界上为真而不在任何其他世界上为真这一途径，“名字”命名了这一世界。
把普通命题字母和作为可能世界名字的命题字母混合起来的这一简单思想催生了大批新的逻辑。例如，公式（*）是有效的：如果前件在一个世界m上是可满足的，那么由i所命名的那个惟一的世界一定是m的R[,π]后继，而且p和q都在i所命名的那个世界上为真。
1.名字、满足算子及其解释
令NOM是一个不同于由普通命题变元p、q等组成的集合PROP的集合。NOM中的元素称为“名字”，写成i，j等。在NOM和PROP上现在可以定义基本混合语言：
WFF：＝i｜p｜
｜∧Ψ｜∨Ψ｜→Ψ｜〈π〉｜[π]｜＠[，i]]
用来指称世界的名字是主要的混合装置，名字扮演的角色与经典逻辑的词项相同，不过，名字是公式而不是词项。名字可以作为符号“＠”的下标出现，这样的组合“＠[,i]”称为满足算子。这个语言的解释是直接的，关键的一步是赋值函数要重新定义。
一个（混合）赋值是一个从集合NOM∪PROP到2[W]的函数V，使得对于所有的i[,∈]NOM，V（i）有且只有一个元集。也就是说， 普通的命题变元可以在模型中的任意多个世界上为真，而名字在任意模型中都只能在一个世界上为真，从而形式刻画了“名字以自己在某一个世界上但不在任何其他世界上为真而命名了该世界”这一直观思想。V（i）中这个惟一的世界一般叫作i的所指（denotation）。 有了赋值概念，新的满足关系可以定义为：模型M中的可能世界w满足公式i当且仅当w是i 的所指；模型M中的可能世界w满足公式＠[,i]当且仅当M中i的所指u满足。也就是说，名字在任意模型中都在惟一的一个世界（即各自的所指）上为真，而公式＠[,i]的作用则是把赋值的世界转移到由i命名的世界，然后检验是否在该世界上为真，因此，＠[,i]是说“在i命名的世界上被满足”。根据满足定义，＠[,i]p是说名字为i的可能世界具有信息p，而＠[,i]p则否定了这一点，因此我们有了一个原子性质如何分布的模态理论。其前缀为满足算子的公式本身可以是名字：公式＠[,i]j是说，名字j在i命名的可能世界上为真，或者说，i和j命名了同一个可能世界，而＠[,i]j则否定了这一点，这样，满足算子给出了一个状态相等的模态理论。此外，公式＠[,i]〈π〉j是说，由j命名的可能世界是i命名的可能世界的R[,π]后继，因此，满足算子还给出了一个状态相续的模态理论。这样，混合语言中就具备了刻画模型所需要的所有工具。
混合语言是模态语言，满足算子具有许多重要的模态性质。首先，满足算子是一个正规模态算子，它满足对蕴涵词的分配性及概括规则：对任意的名字i，＠[,i]（→Ψ）→（＠[,i]→＠[.i]Ψ）是有效式；如果是有效式，那么＠[,i]也是有效式。其次，满足算子是自我对偶的：
是有效式。最后，也是最重要的，是满足算子在语义和句法之间架设了一座联系的桥梁，也就是说，公式在世界w上为真当且仅当＠[,i]为真（其中i是世界w名字），正是由于这一点，满足算子使得作为语义概念的满足关系本身可以在对象语言中被谈及，其被称为“满足算子”的原因就在于此。
此外，在标准翻译下，基本混合语言刻画了带常元和等词的一阶逻辑的双仿不变片断。
2.约束词
在句法中允许直接指称模型中的可能世界这一思想为进一步扩充模态语言打开了方便之门。从标准翻译的角度来看，在模态语言中添加名字实际上就是添加了可能世界的自由变元，因此，一个最明显的扩充是把名字用作可能世界的变元并且加入约束它们的量词，而不仅仅把它们视为单个世界的名字，从而加强了语言的表达能力。
约束方法有“↓”和“
”、“
”两种，比如，公式
就是这种新的合式公式。前一公式在世界m上可满足当且仅当与m具有R[,π]关系的任意世界x都可达至少一个自返的世界y。具有这种性质的公式在传统模态语言和基本混合语言中都不会出现。取值为世界的变元约束思想是当前混合语言大部分研究工作的基础。后一种扩充得到的混合语言足以表达任何一阶概念，不过这样一来，对任意世界取值的全称量词也模糊了克里普克语义学的核心——局部性的直观思想。而“↓”把变元约束到当前的世界，使得“此时此地”有了自己的名字，在本质上是一种局部的方式，例如，公式“↓x.〈π〉x”的直观意思是说，“把当前的世界称为x并且使得x不可达x本身”，从而定义了禁自返性。这一扩充而得到的语言是目前研究的主要混合语言，但是，限制到“↓”并不导致可判定性。
3.历史
“公式用作词项”的思想最早可以追溯到普莱尔（A.Prior）于1967 年出版的名著《过去、现在和将来》，在该书中，名字（普莱尔称为“世界状态命题”）可以被存在量词约束。随后，普莱尔的这一思想被他的学生布珥（R.Bull）在时态逻辑的经典论文《时态逻辑研究》中所发挥，并且引入了第三类命题变元——用“历史过程”来命名模型中的路径（paths）。20世纪80年代中期， 索非亚学派独立提出了混合语言的思想，不仅研究了包含存在量词的混合语言，而且研究了没有约束词的逻辑系统，是当前研究表达能力较弱的混合语言的基础。
三、“混合”的含义
定义“混合语言”的途径是在传统模态逻辑的基础上添加模型论域中个体成员的句法变元和相应的约束词并且进行推理。名字和满足算子扩充了模态语言，得到的是吸收了模态逻辑和一阶逻辑的系统，保持了模态语言的局部性和可判定性，获得了对世界进行命名的能力以及刻画世界之间的相互关系以进行推理的能力，而对名字的约束则为研究一阶可表达性开拓了新思路。前面已经看到，近似于原子的满足命题＠[,i]j和＠[,i]〈π〉j分别是说，名字j在i命名的可能世界上为真（或者说i和j命名了同一个可能世界）、j命名的世界是i命名的世界的R[,π]后继，这些分别属于经典等词理论、断定两个特定世界之间具有某种关系的经典能力。也就是说，混合语言把经典的等词概念和指称概念带进了模态逻辑。
但是，对混合语言中“混合”一词的理解不能仅仅停留在“公式用作词项”这一点上，混合语言同时也是一种社会学意义上的混合。面对类似于图形的结构，围绕如何更好地表示并且对其进行推理这一相同问题，许多不同的学科各自独立地得出了相似的回答，特征逻辑、描述逻辑和加标演绎等都独立地提出过混合语言的关键思想。
除此之外，最重要的一点是混合语言本身的混合性。混合语言把不同的信息种类都组合到一个形式理论之内，在本质上是多种类的模态逻辑。长期以来，人工智能、语言学和哲学等都认识到种类划分的重要性：了解到某一信息是某一特殊种类可以使我们简单地得出有用的结论。不过，在逻辑研究中种类划分长期被忽视了：逻辑学家认为形形色色的多种类推理太简单而不感兴趣，比如说，多种类一阶语言就不能提供新的表达能力。多种类模态语言恰恰相反。通过添加第二种类的原子公式（即可能世界的名字）和相应的句法构造（如满足算子），多种类的模态语言就可以更仔细地刻画模型、定义新的标架类，在此基础上建立的形式推演系统也是模态自然的。
四、理论意义和应用价值
混合语言都是模态语言。同时，混合化非但没有破坏模态逻辑的基础，反而提高了它的能力，引入“可能世界的名字”不仅具有深刻的理论意义，而且有着广泛的应用。兹述四点如下：
1.在模型论方面，混合语言首先提高了对标架的表达能力。在标架可定义性理论中，传统模态语言表达标架性质的能力非常弱。例如，它不能定义禁自返性，即，没有模态公式在具有性质wwRw的标架上有效。而公式＠[,i]〈x〉〈π〉i则定义了这一性质。同样，反对称性（＠[,i][π]（〈π〉i→i））、禁对称性（＠[,i]〈π〉j→＠[,j]〈π〉i）和三歧性（＠[,j]〈π〉i∨＠[,j]i∨＠[,i]〈π〉j）都不能在传统模态语言中而可以在混合语言中得到定义， 而传统模态语言可定义的性质混合语言也能够定义。其次，约束算子“↓”动态地命名了“此时此地”，它和满足算子一起严格贯彻了模态逻辑的第二个新观点，刻画了局部性或者说对生成子模型不变的一阶逻辑。另外，20多年以来一阶模态逻辑一直发展缓慢，主要有一般公理化问题、标架不完全性问题以及大范围内不具有克雷戈（W.Craig）内插性和贝斯（E.W.Beth）可定义性的问题。在一阶模态逻辑中加入算子“↓”和“＠”之后，两者的相互作用使得我们可以轻松地构造出内插公式：任何由不带名字但带有可能世界变元的纯公式所定义的标架类的逻辑都具有内插性（相应地具有贝斯可定义性）。这一结果对于一阶逻辑有界片断中可定义的任意标架类的逻辑都成立，而且并不对论域有任何要求。得出这一结果的一个重要原因在于，混合语言可以刻画出世界相等和相继的模态理论，使得一阶亨金（L.A.Henkin）技术和模态典范模型的运用可以结合起来。内插定理的成立使得句法完美地切合了语义。
2.一般完全性结果。混合逻辑的一个传统话题是混合化导致更简单、更一般的完全性结果。名字和满足算子使我们可以在混合语言的公理系统中，完全性证明不一定要使用模态典范模型，而是也可以使用一阶亨金模型；而在表列系统中，表列规则把公式分解成（）＠[,i]p、（）＠[,i]j和（）＠[,i]〈π〉j，使得表列中所有的开分支都是满足模型的罗宾逊（Robinson）图像。虽然传统模态逻辑具有一般完全性结果（特别是萨奎维斯特（H.Sahlqvist）定理），但是叙述和证明都非常困难。在混合逻辑中，情况简化了：任何不含命题变元的公式相对于其定义的标架都保证是完全的（对任意的纯公式和任意的名字i，与＠[,i]定义的是相同的标架类）。例如，＠[,i]〈π〉i定义了禁自返性，而且也没有包含命题变元，如果把它作为公理加到一个恰当的基本逻辑中，那么可以保证得到的结果相对于非自返标架类是完全的。
3.证明论简化。研究不同的模型需要有不同的逻辑，例如[π]p∧[π]q→[π]（p∧q）是基本的、普遍可用的逻辑的一部分，在任何模型上都有效，而〈π〉〈π〉p→〈π〉p却只属于刻画传递模型的、更强的逻辑，只能在传递模型上有效。模态逻辑学家一直致力于发展一般的逻辑证明方法，这些方法经过改编后可以运用于多种多样模型的逻辑。这一目标通过公理方法来实现，其中基本的公理系统K 可以处理任意的模型。为了处理特殊的模型类，需要给K添加公理，例如，把〈π〉〈π〉p→〈π〉p作为公理添加到K，就得到传递标架的逻辑。但是， 公理系统不便于使用，特别是计算执行（implementation）。自然演绎系统和表列系统易于使用，而消解系统和表列系统则便于计算执行。但在传统模态逻辑中，这些系统又不容易构造出来。困难在于“可能”模态词辖域内信息的选取，也就是说，给定〈π〉之后，如何处理就成为问题。在一阶逻辑中，类似的问题是不足道的：简单的“存在消除规则”（对于某一新常元a，从x可以得出[x←a]）消除了存在量词。而在传统模态逻辑中却没有这样简单的方法消除可能模态词。而名字和满足算子再一次简化了这一问题。例如，在一个表列证明中，我们有＠[,i]〈π〉。通过引入一个新名字j，就可以把这个信息分解成＠[,i]〈π〉j和＠[,j]，这样就把从〈π〉的辖域中分离出来。这一规则本质上就是一阶逻辑的“存在消除规则”：由标准翻译，＠[,i]〈π〉是y(Riy ∧ST[，y]())的缩写，后者由存在消除规则得到Rij∧ST[,j]（），而这就是＠[,i]〈π〉j∧＠[,j]。简而言之， 我们可以通过构造一个状态相续的模态理论来完成一个表列证明，而且名字的运用使得一阶技术可以运用到可判定的逻辑中来。另外，刻画任意模型的表列系统定义出来之后，就可以把它直接扩展到刻画特殊模型类的逻辑，混合化无须通过公理系统就可以达到传统的模态一般性目的。
在证明论上，混合语言比传统的l态语言更为自然。原因在于基本混合语言精确刻画了加标演绎的主要思想，加标演绎建立在记法“l：”的基础之上， 在这一记法中，元语言符号“：”把元语言标记l和对象语言中的公式结合了起来。这一记法有一个自然的模态解释：把标记看成是世界的名字，从而把l：看成是公式在由l命名的世界上被满足。 基本混合语言直接把标准的加标演绎“内在化”于对象语言中：名字实际上就是对象层面上的标记，而公式＠i：在对象语言中所断定的就是“i：”在元语言中所断定的。
4.没有计算性代价。通常，添加名字和满足算子没有提高满足性问题的复杂性。例如，基本模态语言的满足性问题是PSPACE完全的，如果我们加上名字和满足算子仍然保持在PSPACE内。也就是说，不计多项式，混合语言与传统模态语言具有相同的复杂性。命题动态逻辑的满足性问题是EXPTIME完全的，如果我们加进名字和满足算子甚至是全局模态性仍然保持在EXPTIME内。
总而言之，无论是从理论的还是逻辑工程的角度来看，混合化都提供了新的内容。“混合语言”是对位于模态逻辑和经典逻辑之间的逻辑系统的一个称呼，通过在句法中添加可能世界变元和约束它们的装置，任何模态语言都可以“混合化”。