作者系中国社会科学院研究员，专着《可能世界的名字》入选《国家哲学社会科学成果文库》
核证逻辑开始于20世纪90年代的“证明逻辑”，后者是为直觉主义逻辑提供算术语义的一个部分。根据哥德尔的一个推理结果，直觉主义逻辑嵌入到厂4，由于哥德尔不完全性定理，厂4的必然性算子不能作为算术中的形式可证性；但根据哥德尔1938年的一个推理想法，厂4的必然性可以看作“显式”可证性谓词。这一思想在20世纪90年代被阿逖莫夫独立发现，成为建立证明逻辑系统的动机，模态算子被一族显式“证明项”所替换。阿逖莫夫证明的“算术完全性定理”表明，厂4可嵌入到证明逻辑，而证明逻辑可嵌入到形式算术。所有这些一起为直觉主义逻辑提供了一个算术语义学。“核证逻辑”是把证明方法论内部化的模态逻辑新分支。
可能世界语义学
模态逻辑是对于必然性和可能性的逻辑，或者说，是对于“一定是”和“可能是”的逻辑。必然性和可能性也可做其他解释：真势模态逻辑把必然解释为必然真；道义逻辑则把必然解释为道义必然性或规范必然性。必然也可以指“知道为真”或“相信为真”，这是认知逻辑的解释；如果指“总是为真”或“从此总是为真”，则是时态逻辑的解释。还可以把“必然辫”解释为“辫是可证的”。作为必然性和可能性的逻辑，模态逻辑不仅考虑事物实际存在方式的真和假，而且考虑“如果事物处在与实际存在方式不同的存在方式中，那么什么将是真的或假的”。如果一个人考虑到了事物在真实世界中的存在方式，那他或许也会考虑事物在可替代的、非真实即可能的世界中是如何地不同于真实世界中的存在方式。逻辑关注真和假，模态逻辑则关注真实世界和其他可能世界中的真和假。在这个意义上，一个命题在一个世界中是必然的仅当它在可能替代该世界的所有世界中为真，它是可能的则仅当它在可能替换该世界的某个可能世界中为真。
以此为基础来考虑模态逻辑有效性的可能世界语义学始于20世纪50年代晚期和60年代早期。可能世界是可能世界语义学的核心概念，模态逻辑历史中最主要的突破性进展是可能世界语义学的提出，由于简单、自然以及起源于哲学等特点，可能世界语义学一直是模态逻辑模型论研究的基本工具。
可能世界的名字
可能世界语义学与旧有的句法传统之间的对应并不完美，局部视角与标准模态语言的全局视角两者之间的不对称正是问题的来源。也就是说，在可能世界语义学中具有根本地位的（模型中的）可能世界并没有在模态句法中表现出来。这种不对称情形导致了许多并非我们需要的结果，比如，缺乏对许多语义特征的充分表示，缺乏合适的模态证明论。前者比较容易解释，因为标准模态语言没有一套机制来命名一个模型中的特殊“可能世界”、断定或否定可能世界的相等、表达从一个可能世界到另一个可能世界的可达性等。这些都属于模态模型论的核心问题，但在标准句法中表示不出来。可能世界语义学中框架的许多重要性质都以一种非常间接的方式被表达出来，而其他许多重要性质则干脆在标准模态语言中无法被表达。
模态逻辑的标准证明论的应用范围是非常有限的。普通证明方法应用到标准模态逻辑时的问题主要与下述事实有关：很难处理模态算子辖域内的信息。对于许许多多的模态逻辑来讲，存在着大量的非公理化的证明系统，但是在大量情况下，这些逻辑提供的都是对它们的形式化中所出现的问题的人为解决。一些所谓自然的系统只是某些特殊的逻辑的形式系统，难以进行一般化推广。因此，在标准模态逻辑中，与可能世界模型所成功提供的语义工作相比，句法方面并没有一种统一的架构可言。
一个自然而然的问题就是如何使得句法和语义相互一致起来。一种可能性就是在语言中为模型中的可能世界引入明显的句法表示。这样一种扩张可以为表达力提供足够的灵活性，不过也引发一个伴生的问题：以何种方式实现这一工作。至少可以有两种方向：外部方向和内部方向。外部方向是为逻辑语言引入新的元理论工具，模态逻辑中最流行的解决办法是为公式添加前缀。内部方向则是添加对象语言以及新的算子，对象语言的丰富通过对原子进行分类表达到。这就是混合逻辑所做的工作——在句法中为可能世界引进“名字”。
混合逻辑是模态逻辑的一个崭新分支，不过起源可以追溯到20世纪50年代，只是重要性直到20世纪90年代才被认识到。混合逻辑的两个根本思想是：满足关系的内部化（此时的满足关系是相对而言的）、把命题划分为普通命题和名字。
添加了这些内容之后，我们可以获得怎样的结果？尤其是，这样一来确实就比标准模态语言优越吗？这个问题在原子分类方面尤其有意思：众所周知，对一阶语言的变元进行划分并不会获得更多的表达能力，只是比标准单种类语言表述得稍微紧致、简单一点。但是，在模态语言中对（命题）变元进行分类将会真正改变表达能力从而获得更多的改进。因此，混合的模态语言主要是修复关系结构的元素与语言能力之间不对称性的一种工具。简而言之，混合语言的引入将有下述用处：获得更具表达力的语言；完全性理论中更好的表现；更自然、更简单的证明理论；可判定性、复杂性、内插性以及其他重要性质中的良好行为。
对于获得更具表达力的语言，直接的字面意思就是说在扩张后的语言所表述的逻辑中将会有更多的有效式，但更为重要的是，混合语言可以定义许多在标准模态语言中不能表达的框架性质。表达能力的提高有利于更为直接、更为完备的框架可定义性理论的建立。混合逻辑中获得的一般完全性理论也将比标准模态逻辑中相应的结果更为简单。模态逻辑的标准证明方法的应用比较复杂是因为很难处理模态算子辖域内的句子。在混合逻辑中，一些自然的工具如名字和满足算子可以处理这一问题。混合逻辑中的每一个模态化句子都可以分裂成几个部分，其中一些部分载有一个模型的结构信息，而一个部分直接为我们给出原先处于模态算子辖域内的句子。把复杂信息分解成较为简单部分的这一自然方式，容易使经典逻辑的非公理化方法移植到模态逻辑。因此，混合逻辑更为丰富的语言为模态证明论提供了更为一般且统一的句法背景。
值得一提的是，在很多情况下，我们不必为语言表达能力的提高而付出代价。逻辑的一个非常重要的特征是它们的可判定性及判定程序的复杂性。那些可判定的模态逻辑经过混合化之后仍然是可判定的，而且通常的情况是复杂性也并没有被触动。
可能世界语义学是模态逻辑最流行的语义学，也是最具哲学意义的语义学，在模态逻辑的对象语言中引入“可能世界的名字”作为一类原子命题，非但没有破坏模态逻辑的基础，反而提高了它的表达能力，具有深刻的理论意义和哲学意义。
构造核证逻辑系统
混合逻辑是内部化了的可能世界语义学的模态逻辑，而核证逻辑内部化了证明方法论。一个自然而然的问题是：是否具有核证逻辑形式的混合逻辑。也就是说，把“可能世界的名字”引入核证逻辑，在一个逻辑中既内部化语义学又内部化证明，把这两种思想组合到一个系统当中。这个方向开始于世界着名逻辑学家费汀在2010年的工作。我们的研究在其基础上构造了混合逻辑形式的核证逻辑系统，把语义学内部化和证明内部化统一在一个形式系统内，建立起混合核证逻辑的极小系统，提出适当的语义解释并给出完全性定理和实现定理的证明，从而解决了费汀提出来的未解决问题——混合核证逻辑的极小系统问题。
混合核证逻辑极小系统的建立对于混合核证逻辑这一族逻辑的研究具有重要意义，极小系统的发现意味着这一族逻辑中“最普遍真理”的发现。从哲学上来说，由一个名字命名的可能世界是一类“事实”，在维特根斯坦看来，“逻辑空间中的诸事实即是世界”，构成一个世界的诸事实必须要能被验证确实是构成了一个世界，这是建立并研究“混合的核证逻辑”的部分哲学意义。
