《可能世界的名字》概要
刘新文[1]
一、研究的目的、意义及方法
模态逻辑是关于必然性和可能性的逻辑，或者说，是关于“一定是”和“可能是”的逻辑。当然，必然性和可能性有不同的解释。真势模态逻辑把必然解释为必然真；道义逻辑则把必然解释为道义必然性或规范必然性。必然也可以指知道或相信为真，这是认知逻辑的解释；如果指总是为真或从此总是为真，则是时态逻辑的解释。另外也可以把“必然p”解释为“p是可证的”。作为必然性和可能性的逻辑，模态逻辑不仅考虑事物实际存在方式的真和假，而且考虑如果事物处在与实际存在方式不同的存在方式中，那么什么将是真的或假的。如果一个人考虑到了事物在真实世界中的存在方式，那他或许也会考虑事物在可替代的、非真实即可能的世界中是如何不同于真实世界中的存在方式。逻辑关注真和假，模态逻辑则关注真实世界和其他可能世界中的真和假。在这种意义上，一个命题在一个世界中是必然的仅当它在可能替代该世界的所有世界中为真，是可能的则仅当它在可能替换该世界的某个可能世界中为真。这就给出了适于模态逻辑的有效性的形式定义的基础。
这样考虑有效性始于20世纪50年代晚期和60年代早期，其中尤以克里普克的贡献为最大，故我们经常称框架为“克里普克框架”，称模态逻辑的可能世界语义或关系语义为“克里普克语义”。不过，相似的观点也出现在其他人的著作中，如康格尔、巴亚尔、蒙塔古和辛迪卡。较早的相关工作可以在瓦伊斯伯格、卡尔纳普的论著以及其他一些文献中找到。扬森和塔尔斯基为这个有效性概念提出了一个代数描述，不过在论文中没有与模态逻辑联系起来。20世纪六七十年代，模态逻辑完全性结果的研究以及一些局限的发现导致了对模态语言的表达能力的更为系统的研究，其中，模态语言因应用为人工智能中关系结构的描述语言而得到了深刻研究，范本特姆则奠定了对应理论的基础。但是，为什么模态语言可以用于研究关系结构，它们又可以表达多少？可能的原因就在于模态语言的公式对应于一些关系条件。
混合逻辑是标准模态逻辑的一个扩张，方式是对其语言进行改变。构成整个混合语言家族的基础的改变是引入一类特殊的符号——“名字”（nominal），由此可以明显指称克里普克模型中的状态。这一研究方向的名称反映出一个事实：名字既命名了模型中的状态，同时又是模态语言的句子。这一领域肇端于普莱尔在20世纪50年代末关于模态逻辑与时态逻辑的工作，但深入、系统的研究直到20世纪90年代才开始。当代混合逻辑是现代模态逻辑最活跃的分支之一，为经典结论提供了大量的改进。本成果的目的主要在于两个方面。第一，全面地介绍和研究混合逻辑的极小系统。第二，混合逻辑将自己的语义内在化，而新近出现的核证逻辑则将各自的证明方法内在化，很自然地，把两种理念组合成一个系统就是一个很吸引人的工作，本成果介绍并研究这一新的研究方向，最终目的在于为混合的核证逻辑建立起极小系统，从而解决美国著名逻辑学家梅尔文·费汀在2010年提出的这个问题——混合核证逻辑的极小系统问题，将这一新的研究方向做进一步推进。在方法上，我们主要采用的是模态模型论的研究方法。
二、成果的主要内容和重要观点
1.主要内容
“可能世界”是模态逻辑可能世界语义学的核心概念，模态语言本质上是研究经典模型论意义上关系结构的形式语言，但传统模态语言不能指称关系结构中的个体并对其进行推理。在传统模态逻辑的句法中引入“可能世界的名字”作为第二类原子命题（并引入相应的算子和约束词），得到的语言称为“混合语言”。混合语言既发扬了模态语言积极的一面，又克服了模态语言前述的重大缺陷，把经典一阶逻辑和模态逻辑的方法和技术混合起来，在可定义性理论中提高了对框架的表达能力，完全性理论方面导致更具普遍性的结果，证明论上比传统的模态语言更为自然。2007年出版的《模态逻辑手册》把混合逻辑专门列为一章，主要概述了模型论方面的重要结果。
混合逻辑（hybrid logic）是内部化了可能世界语义学的模态逻辑，而最近出现的一族相当不同的“核证逻辑”（justification logic）则内部化了证明方法论。核证逻辑开始于“证明逻辑”（logic of proofs，LP），证明逻辑是为直觉主义逻辑提供算术语义这一规划的一部分。根据哥德尔的一个结果，直觉主义逻辑嵌入到S4，由于哥德尔不完全性定理，S4的必然性算子不能作为算术中的形式可证性；但根据哥德尔1938年的一个想法，S4的必然性可以看作是“显式”可证性谓词。这一思想被俄罗斯逻辑学家阿逖莫夫于20世纪90年代初独立发现，成为建立证明逻辑系统的动机，模态算子被一族显式“证明项”（proof terms）所替换。阿逖莫夫证明的“算术完全性定理”表明，S4嵌入到LP、LP本身嵌入到形式算术。所有这些一起为直觉主义逻辑提供了一个算术语义学。从此开始，证明被理解成一种核证。这些技术不仅仅应用到S4，现在，一大批对应于K、T、S4、S5及其多模态、多主体形式甚至关于量化核证的逻辑得以建立起来，特别是应用到认知逻辑时具有更为丰富的成果。这一方向中进一步的工作还在继续。
一个自然而然的问题是：是否具有核证逻辑形式的混合逻辑？也就是说，我们想要把“可能世界的名字”引入核证逻辑，在一个逻辑中既内部化语义学又内部化证明，把这两种思想组合到一个系统当中是当前哲学逻辑的一个重要的新分支。另外，“可能世界语义学”是模态逻辑最流行的语义学，也是最具哲学意义的语义学，在模态逻辑的对象语言中引入“可能世界的名字”作为一类原子命题，非但没有破坏模态逻辑的基础，反而提高了它的表达能力，不仅具有深刻的理论意义，而且有着广泛的应用；而核证逻辑是可证性逻辑的最新进展，把两者组合在一个系统之内，研究所得系统的元理论性质，这是一种逻辑基础理论的研究。
本成果首先简要介绍混合逻辑的基本思想，主要内容是研究混合逻辑在两个方面所提供的优势。第一方面是混合语言表达力问题，在简要介绍普通模态逻辑之后，对最重要的混合语言、混合逻辑以及它们的谱系进行综述；在每种情形中，都定义其最弱的逻辑及其完全的公理系统。在这一部分的内容之后，介绍了一阶混合逻辑，主要关注混合逻辑的可判定性、复杂性以及关于内插性的一些结果。第二方面是关于混合逻辑证明论的。尽量介绍迄今为止混合逻辑所有的演绎系统并描绘出它们最有意思的特征。对混合逻辑证明系统的全景式研究有一个更为广阔的背景，那就是标记在证明系统中的应用。另外还有一个原因就是，模态逻辑证明方法的研究仍然是一个备受冷落的领域，而混合逻辑将为这一领域提供突破。最后，在介绍核证逻辑的基础上，进一步解决梅尔文·费汀提出的未解决问题——混合核证逻辑的极小系统问题，并对其哲学意义做出初步阐释。
2.重要观点
模态逻辑中最主要的突破性进展是可能世界语义学的提出，可能世界语义学即通常所说的克里普克语义学，于20世纪五六十年代由辛迪卡、康格尔、克里普克等提出。由于其简单、自然以及起源于哲学等特点，可能世界语义学一直是模态逻辑模型论研究的基本工具。但是，近半个世纪的研究表明，可能世界语义学与旧有的句法传统之间的对应并不完美。可能世界语义学的局部视角与标准模态语言的全局视角，这两者之间的不对称正是问题的来源，也就是说，在可能世界语义学中具有根本地位的（模型中的）可能世界并没有在模态句法中表现出来。这种不对称情形导致了许多并非我们所需要的结果，比如：第一，缺乏对许多语义特征的充分表示；第二，合适的模态证明论问题。这里的第一点比较容易解释。标准模态语言没有一套机制来命名一个模型中的特殊“可能世界”（或者说“状态”），断定或否定可能世界的相等，表示出从一个可能世界到另一个可能世界的可达性，等等。这些事情都属于模态模型论的核心问题，但在标准句法中表示不出来。情况是很严峻的，尤其是与经典一阶逻辑比较起来的时候更为明显：在一阶逻辑中，模型中的元素在语言中有直接的表示。实际上，可能世界语义学中框架的许多重要性质都以一种非常间接的方式表达出来，而其他许多重要性质则干脆在标准模态语言中无法表达。
另外，模态逻辑的标准证明论在应用范围中是非常有限的。普通证明方法应用到标准模态逻辑时的问题主要与下述事实有关：很难处理模态算子辖域内的信息。对于许许多多的模态逻辑来讲，存在着大量的非公理化的证明系统，但是在大量情况下，这些逻辑提供的都是对它们的形式化中所出现的问题的人为解决。一些所谓自然的系统只是某些特殊的逻辑的形式系统，难以进行一般化推广。因此，在标准模态逻辑中，与可能世界模型所成功提供的语义工作相比，句法方面并没有一种统一的架构可言。
这样看来，一个自然而然的问题就是如何使得句法和语义相互一致起来。一种可能性就是在语言中为模型中的可能世界引入明显的句法表示。这样一种扩张可以为表达力提供足够的灵活性，不过也引发一个伴生的问题：以何种方式实现这一工作？至少可以有两种方向：第一，外部的方向，如多夫·格拜的加标演绎系统；第二，内部方向，即混合逻辑。外部方向是为逻辑语言引入新的元理论工具，模态逻辑中最流行的解决办法是为公式添加前缀，这一方面以美国的梅尔文·费汀贡献最为显著，可以参看他于1983年出版的《模态逻辑与直觉主义逻辑中的证明方法》一书，此书广为称引，影响甚大，而对这一方向最为成熟的提倡者是多夫·格拜的加标演绎系统——逻辑的一种一般形式化理论，具体可以参看他于1996年出版的《LDS——加标演绎系统》一书。
内部方向则是添加对象语言以及新的算子作为模态词，对象语言的丰富通过对原子进行分类来达到。这就是混合逻辑所做的工作——在句法中为可能世界引进“名字”。
混合逻辑是模态逻辑的一个崭新分支，不过其起源可以追溯到20世纪50年代，只是其重要性直到20世纪90年代才得以被认识。混合逻辑源于普莱尔的工作。普莱尔是公认的标准时态逻辑的创始人，但他的一些后期工作未被充分注意。普莱尔根据麦克塔格特对时间的分析而区分出两种不同的演算：A-序列（用过去、现在和将来表达的时间）对应的是使用时态常项F和P的标准时态逻辑（T-演算）；对应B-序列（早于/迟于）的是使用时刻表上的二元I-关系的I-演算（随后又称U-演算）。虽然I-演算比T-演算表达能力更强，但普莱尔认为时态（sense）在形而上学方面更为基本。I-演算提供的是一种便利但间接的叙述方式。所以，普莱尔的问题就是：如何证明T-演算比I-演算更基本？他最后的解决办法是利用语言扩张而在T-演算内部来发展I-演算，这使他发明出带有时刻变元和Symbolb@@的强混合逻辑。受奎因关于模态词的著名思想影响，普莱尔在《时间和时态的论文集》中引入了时态逻辑结果的四等级概念。在第二等级中，普莱尔引入了形如T（a,j）的公式，用来表示“j在时间a上为真”，此外，他认为时刻变元a、b、c等还必须表示命题。因此，当代混合逻辑的两个根本思想已经出现：第一，满足关系的内部化（此时的满足关系是相对而言的）；第二，把命题划分为普通命题和名字（“名字”是现今通行的叫法）。
使用带有语义满足关系编码的句法算子这一思想曾经很流行，至少有三种很著名的做法来使用这样的算子：约翰·麦卡锡和P.海耶斯的情境演算、尼古拉斯·雷斯彻儿和A.厄克特的时态逻辑以及J.艾伦在人工智能适于时态表示的语言中对“Hold”算子的使用。J.培扎诺夫斯基在为形式本体论引入一般模态算子理论时也独立地获得了相似的思想。类似的概念也是加标演绎所固有的，不过这是在元理论水平上的发展，即作为状态表述的外部研究。这一方向归功于梅尔文·费汀，其一般发展是多夫·格拜的加标演绎系统的理论。
对混合逻辑更为基本的第二个思想，长期以来被人们所遗忘（说名字更基本是因为存在很多只带名字的混合语言）。20世纪70年代初，普莱尔的学生罗伯特·布珥早期的工作引入一种“历史变元”来表示分叉时态逻辑中的路径，但这一工作长期没有得到注意，而且人们在很长时间内对名字并不感兴趣。使用名字的这一想法重返人们的视野是和索菲亚学派的工作分不开的，伽格夫、汀科夫、帕斯和葛兰科等人在20世纪90年代的工作中复兴了名字的使用，而且发展了混合约束词的工作。这一学派特别致力于组合的命题动态逻辑的研究。
真正的混合逻辑运动始于20世纪90年代初P.白磊本对带名字的时态逻辑的研究工作以及杰瑞米·塞利格曼对情境理论的证明方法的研究工作。此后，大批研究者开始投入到这一研究中来，2007年出版的《模态逻辑手册》专门有一章概述混合逻辑的已有成果（主要是模型论方面）。
添加了这些内容之后，我们可以获得什么样的结果？尤其是，这样一来确实就比标准模态语言优越吗？这个问题在原子分类方面尤其有意思：众所周知，对一阶语言的变元进行划分并不会获得更多的表达能力，只是比标准单种类语言表述得稍微紧致、简单一点；但是，在模态语言中对（命题）变元进行分类将会真正改变表达能力从而获得更多的改进。因此，混合的模态语言主要是修复关系结构的元素与语言能力之间不对称性的一种工具。简而言之，混合语言的引入将有下述用处：第一，获得更具表达力的语言；第二，在完全性理论中有更好的表现；第三，获得更自然、更简单的证明理论；第四，可判定性、复杂性、内插性以及其他重要性质中具有良好行为。关于第一点，直接的字面意思就是说我们在扩张后的语言所表述的逻辑中将会有更多的有效式，但更为重要的是，混合语言可以定义许多在标准模态语言中不能表达的框架性质。表达能力的提高有利于更为直接、更为完备的框架可定义性理论的建立。混合逻辑中获得的一般完全性理论也将比标准模态逻辑中相应的结果（如著名的萨奎斯特完全性定理）更为简单。混合逻辑的证明系统在什么意义上更为自然、更为简单，我们将会在后续内容中阐述，此处稍加提及。前面提到，模态逻辑的标准证明方法的应用比较复杂乃是因为很难处理模态算子辖域内的句子。在混合逻辑中，一些自然的工具如名字和满足算子可以处理这一问题。混合逻辑中的每一个模态化句子都可以分裂成几个部分，其中一些部分载有一个模型的结构信息，而另外一些部分直接为我们给出原先处于模态算子辖域内的句子。把复杂信息分解成较为简单部分的这一自然方式，容易使经典逻辑的非公理化方法移植到模态逻辑中。因此，混合逻辑更为丰富的语言为模态证明论提供了更为一般且统一的句法背景。
值得一提的是，在很多情况下，我们不必为语言表达能力的提高而付出代价。逻辑的一个非常重要的特征是它们的可判定性及判定程序的复杂性。那些可判定的模态逻辑经过混合化之后仍然是可判定的，而且通常的情况是其复杂性也并没有被触及（例如，基本混合逻辑的满足性问题与标准模态逻辑K同样都是PSPACE-完全的）。此外，混合逻辑在许多方面都比标准模态逻辑优越——比方说在内插性方面就很明显。
最后，从哲学上来说，西方哲学界自柏拉图以来一直都认为“知识是得到核证的真信念”。1963年，美国哲学家葛梯尔为这一定义提出两个反例，说明即使是得到核证的真信念也未必是知识，引发了哲学界对于知识定义的一系列争论，并导致葛梯尔问题的出现：怎样补充或修改知识三要素才能完整定义知识概念。自冯莱特、欣迪卡以来，对知识和信念概念的形式化研究主要是以模态逻辑的方式进行，也就是认知逻辑。认知逻辑没有考察在认知研究中占据基本地位的核证概念，使得知识的模态逻辑具有极大缺陷，在“逻辑万能”问题上尤其突出，也使认知逻辑与主流认识论之间存在鸿沟。当然，形式逻辑方法并不能直接解决哲学问题，而是提供工具来分析假设，并且确保我们可以得出正确的结论。我们认为，葛梯尔推理在形式上是正确的，它属于处理部分核证的核证逻辑领域，但是与事实性核证和知识的核证逻辑系统不协调。核证逻辑吸收来自主流认识论和数学证明理论的基本原理，为认知核证的推理及其与知识、信念之间的联系提供了一般的逻辑框架，从三个方面扩展了知识的逻辑：核证的数学概念的增添使得这一逻辑更具表达力，“F被知道”解释成“F具有足够的核证”而为知识的逻辑提供了新的、基于证据的基础，核证逻辑为真理追踪提供了崭新的、基于证据的机制来获得坚实的核证。对于核证的进一步研究，比如说JTB知识定义的“第四个条件”或许具有促进作用。其他核证逻辑原理或许会推进进一步的讨论。另外，由一个名字命名的可能世界是一类“事实”，在维特根斯坦看来，“逻辑空间中的诸事实即是世界”，构成一个世界的诸事实必须要验证确实是构成了一个世界——这应该是我们所要建立并研究的“混合的核证逻辑”的部分哲学意义。
三、成果的学术创新、应用价值以及社会影响和效益
本成果是对哲学逻辑的新分支——混合逻辑的一个专题研究。到目前为止，国际逻辑学界已经出版了三本研究混合逻辑的专著——《扩充的模态语言的模型论》（2005年）、《混合逻辑及其证明论》（2009年）以及《混合逻辑的演绎系统和可判定性问题》（2014年），这三本著作分别研究了混合逻辑的模型论、证明论以及可判定性与计算复杂性。本成果则主要侧重于混合逻辑的极小系统方面。
本成果主要有两个方面的内容：第一，在传统模态逻辑的基础上，系统介绍、研究了混合逻辑的主要思想、元理论成果和证明方法。在可证性逻辑的基础上，介绍、研究了核证逻辑的主要思想，并运用一阶核证逻辑对著名的哲学问题“葛梯尔问题”进行了初步分析。第二，解决了美国著名逻辑学家费汀提出的一个问题。本成果的研究重点和最主要的创新之处在于，构造混合逻辑形式的核证逻辑系统，把语义学内部化和证明内部化统一在一个形式系统内，建立起混合核证逻辑的极小系统，提出适当的语义解释并给出完全性定理和实现定理的证明，解决了费汀在2010年的论文《核证逻辑和混合逻辑》中提出来的未解决问题——混合核证逻辑的极小系统问题。
本成果属于模态逻辑前沿问题研究，成果的发表和出版对于促进国内模态逻辑研究具有重要意义；另外，混合核证逻辑极小系统的建立对于混合核证逻辑这一族逻辑的研究也具有重要意义——极小系统的发现意味着这一族逻辑中“最普遍真理”的发现。本成果建立了模态逻辑T的一个对应的混合/核证逻辑，其他的模态逻辑也可以进行相似的研究，尽管研究能走多远还未可知。至于K4和S4的对应似乎也是同样可行的，S5可能也不会有大问题。本成果中所用的混合机制都是基本混合逻辑的——并没有假设所有世界都被命名的情况。在命名模型（named model）的情况中，混合逻辑有更强的性质和能力。处理命名模型的机制，从理论性的证明而言，要增加一些规则到基本混合逻辑中。这些规则的对应也要添加到我们的混合/核证逻辑中。困难之处就是提出合适而直观可行的机制允许我们证明内在化定理，如同我们在元定理的证明中所做的那样。本成果认为，一旦内在化定理被证明，其他内容可以容易得到。我们希望有人能填补这项研究。尽管本成果已经展现了一个明确地组合了其模型论和证明论方面的逻辑，但到现在为止，这两方面还不存在任何性质上的联系。表达力机制也提了出来但没有做太多。可以把核证逻辑看作知识的逻辑，其中外在（明确）的理由可以被讨论。也可以把这个逻辑的机制与“谈论”世界的能力结合起来，这样可能涉及一些有意义的内容。HJT的语言也需要研究。它允许我们说什么？这也是我们鼓励大家来一起探讨的一个重要问题。
注释
[1]刘新文，中国社会科学院研究员，硕士生导师。