作者系中國社會科學院研究員，專著《可能世界的名字》入選《國家哲學社會科學成果文庫》

核證邏輯開始于20世紀90年代的“證明邏輯”，后者是為直覺主義邏輯提供算術語義的一個部分。根據哥德爾的一個推理結果，直覺主義邏輯嵌入到S4，由于哥德爾不完全性定理，S4的必然性算子不能作為算術中的形式可證性；但根據哥德爾1938年的一個推理想法，S4的必然性可以看作“顯式”可證性謂詞。這一思想在20世紀90年代被阿逖莫夫獨立發現，成為建立證明邏輯系統的動機，模態算子被一族顯式“證明項”所替換。阿逖莫夫證明的“算術完全性定理”表明，S4可嵌入到證明邏輯，而證明邏輯可嵌入到形式算術。所有這些一起為直覺主義邏輯提供了一個算術語義學。“核證邏輯”是把證明方法論內部化的模態邏輯新分支。

可能世界語義學

模態邏輯是關于必然性和可能性的邏輯，或者說，是關于“一定是”和“可能是”的邏輯。必然性和可能性也可做其他解釋：真勢模態邏輯把必然解釋為必然真；道義邏輯則把必然解釋為道義必然性或規范必然性。必然也可以指“知道為真”或“相信為真”，這是認知邏輯的解釋；如果指“總是為真”或“從此總是為真”，則是時態邏輯的解釋。還可以把“必然p”解釋為“p是可證的”。作為必然性和可能性的邏輯，模態邏輯不僅考慮事物實際存在方式的真和假，而且考慮“如果事物處在與實際存在方式不同的存在方式中，那么什么將是真的或假的”。如果一個人考慮到了事物在真實世界中的存在方式，那他或許也會考慮事物在可替代的、非真實即可能的世界中是如何地不同于真實世界中的存在方式。邏輯關注真和假，模態邏輯則關注真實世界和其他可能世界中的真和假。在這個意義上，一個命題在一個世界中是必然的僅當它在可能替代該世界的所有世界中為真，它是可能的則僅當它在可能替換該世界的某個可能世界中為真。

以此為基礎來考慮模態邏輯有效性的可能世界語義學始于20世紀50年代晚期和60年代早期。可能世界是可能世界語義學的核心概念，模態邏輯歷史中最主要的突破性進展是可能世界語義學的提出，由于簡單、自然以及起源于哲學等特點，可能世界語義學一直是模態邏輯模型論研究的基本工具。

可能世界的名字

可能世界語義學與舊有的句法傳統之間的對應并不完美，局部視角與標準模態語言的全局視角兩者之間的不對稱正是問題的來源。也就是說，在可能世界語義學中具有根本地位的（模型中的）可能世界并沒有在模態句法中表現出來。這種不對稱情形導致了許多并非我們需要的結果，比如，缺乏對許多語義特征的充分表示，缺乏合適的模態證明論。前者比較容易解釋，因為標準模態語言沒有一套機制來命名一個模型中的特殊“可能世界”、斷定或否定可能世界的相等、表達從一個可能世界到另一個可能世界的可達性等。這些都屬于模態模型論的核心問題，但在標準句法中表示不出來。可能世界語義學中框架的許多重要性質都以一種非常間接的方式被表達出來，而其他許多重要性質則干脆在標準模態語言中無法被表達。

模態邏輯的標準證明論的應用范圍是非常有限的。普通證明方法應用到標準模態邏輯時的問題主要與下述事實有關：很難處理模態算子轄域內的信息。對于許許多多的模態邏輯來講，存在著大量的非公理化的證明系統，但是在大量情況下，這些邏輯提供的都是對它們的形式化中所出現的問題的人為解決。一些所謂自然的系統只是某些特殊的邏輯的形式系統，難以進行一般化推廣。因此，在標準模態邏輯中，與可能世界模型所成功提供的語義工作相比，句法方面并沒有一種統一的架構可言。

一個自然而然的問題就是如何使得句法和語義相互一致起來。一種可能性就是在語言中為模型中的可能世界引入明顯的句法表示。這樣一種擴張可以為表達力提供足夠的靈活性，不過也引發一個伴生的問題：以何種方式實現這一工作。至少可以有兩種方向：外部方向和內部方向。外部方向是為邏輯語言引入新的元理論工具，模態邏輯中最流行的解決辦法是為公式添加前綴。內部方向則是添加對象語言以及新的算子，對象語言的豐富通過對原子進行分類表達到。這就是混合邏輯所做的工作——在句法中為可能世界引進“名字”。

混合邏輯是模態邏輯的一個嶄新分支，不過起源可以追溯到20世紀50年代，只是重要性直到20世紀90年代才被認識到。混合邏輯的兩個根本思想是：滿足關系的內部化（此時的滿足關系是相對而言的）、把命題劃分為普通命題和名字。

添加了這些內容之后，我們可以獲得怎樣的結果？尤其是，這樣一來確實就比標準模態語言優越嗎？這個問題在原子分類方面尤其有意思：眾所周知，對一階語言的變元進行劃分并不會獲得更多的表達能力，只是比標準單種類語言表述得稍微緊致、簡單一點。但是，在模態語言中對（命題）變元進行分類將會真正改變表達能力從而獲得更多的改進。因此，混合的模態語言主要是修復關系結構的元素與語言能力之間不對稱性的一種工具。簡而言之，混合語言的引入將有下述用處：獲得更具表達力的語言；完全性理論中更好的表現；更自然、更簡單的證明理論；可判定性、復雜性、內插性以及其他重要性質中的良好行為。

關于獲得更具表達力的語言，直接的字面意思就是說在擴張后的語言所表述的邏輯中將會有更多的有效式，但更為重要的是，混合語言可以定義許多在標準模態語言中不能表達的框架性質。表達能力的提高有利于更為直接、更為完備的框架可定義性理論的建立。混合邏輯中獲得的一般完全性理論也將比標準模態邏輯中相應的結果更為簡單。模態邏輯的標準證明方法的應用比較復雜是因為很難處理模態算子轄域內的句子。在混合邏輯中，一些自然的工具如名字和滿足算子可以處理這一問題。混合邏輯中的每一個模態化句子都可以分裂成幾個部分，其中一些部分載有一個模型的結構信息，而一個部分直接為我們給出原先處于模態算子轄域內的句子。把復雜信息分解成較為簡單部分的這一自然方式，容易使經典邏輯的非公理化方法移植到模態邏輯。因此，混合邏輯更為豐富的語言為模態證明論提供了更為一般且統一的句法背景。

值得一提的是，在很多情況下，我們不必為語言表達能力的提高而付出代價。邏輯的一個非常重要的特征是它們的可判定性及判定程序的復雜性。那些可判定的模態邏輯經過混合化之后仍然是可判定的，而且通常的情況是復雜性也并沒有被觸動。

可能世界語義學是模態邏輯最流行的語義學，也是最具哲學意義的語義學，在模態邏輯的對象語言中引入“可能世界的名字”作為一類原子命題，非但沒有破壞模態邏輯的基礎，反而提高了它的表達能力，具有深刻的理論意義和哲學意義。

構造核證邏輯系統

混合邏輯是內部化了的可能世界語義學的模態邏輯，而核證邏輯內部化了證明方法論。一個自然而然的問題是：是否具有核證邏輯形式的混合邏輯。也就是說，把“可能世界的名字”引入核證邏輯，在一個邏輯中既內部化語義學又內部化證明，把這兩種思想組合到一個系統當中。這個方向開始于世界著名邏輯學家費汀在2010年的工作。我們的研究在其基礎上構造了混合邏輯形式的核證邏輯系統，把語義學內部化和證明內部化統一在一個形式系統內，建立起混合核證邏輯的極小系統，提出適當的語義解釋并給出完全性定理和實現定理的證明，從而解決了費汀提出來的未解決問題——混合核證邏輯的極小系統問題。

混合核證邏輯極小系統的建立對于混合核證邏輯這一族邏輯的研究具有重要意義，極小系統的發現意味著這一族邏輯中“最普遍真理”的發現。從哲學上來說，由一個名字命名的可能世界是一類“事實”，在維特根斯坦看來，“邏輯空間中的諸事實即是世界”，構成一個世界的諸事實必須要能被驗證確實是構成了一個世界，這是建立并研究“混合的核證邏輯”的部分哲學意義。