混合模態邏輯的有窮模型性研究

彭玉 林哲

1 引言

所謂一個邏輯具有有窮模型性是指如果一公式在該邏輯系統中不可證，那么它在該邏輯系統的一有窮模型中不成立。有窮模型性是邏輯研究中重要的基礎性質之一，此概念不僅本身具有重要意義，并且有廣泛應用。一個有窮可公理化且具有有窮模型性的邏輯是可判定的。長久以來，一邏輯是否具有有窮模型性是證明其是否可判定的重要方式。關于模態邏輯的有窮模型性有著廣泛的研究。模態邏輯的有窮模型性的一般證明方法是濾子方法（見[6]）。蓋比（D.M.Gabby，[4]）給出了濾子方法在模態邏輯上的一般化方案，證明了如K、T、B、S4、S4.1、S4.2、S5等熟知的經典模態邏輯具有有窮模型性。扎哈拉斯基夫(M.Zakharyaschev)在[15,16]中修改這種方法并用典范公式證明了K4以上的所有經典模態邏輯具有有窮模型性。時態邏輯的有窮模型性問題也備受研究者們的關注，有部分時態邏輯被證明具有有窮模型性，也有部分被證明并不滿足有窮模型性，具體可參照賽格博格(K.Segerberg)的研究（[12]）。沃爾特（F.Wolter，[14]）考慮了時態邏輯有窮模型性的一般化結論，他將扎哈拉斯基夫在模態邏輯上的結論延伸到經典時態邏輯中，證明了K4以上滿足一定典范框架條件的所有經典時態邏輯具有有窮模型性。

模態邏輯和時態邏輯有著廣泛的應用場景，如認知、人工智能、邏輯程序、知識表達等，因此單模態不足以駕馭如此多的應用。許多邏輯學家早已敏銳地察覺到混合模態邏輯研究的重要性。范恩（K.Fine）和舒爾茨（G.Schurz）在[3]中提出了傳遞性定理（transfer theorem）來研究單模態邏輯的重要性質與混合多模態邏輯相應性質的關系。傳遞性定理是說如果一些重要的性質如完全性和有窮模型性等在某些單模態邏輯中成立，那么在基于這些單模態邏輯的混合模態邏輯中也成立?？死仗兀∕.Kracht）和沃爾特（F.Wolter）在[5]中通過代數的方法證明了在一些經典模態邏輯中傳遞性定理成立。遺憾的是沒有已證的時態邏輯上的傳遞性定理的一般性結果。

除了上述的混合模態邏輯與混合時態邏輯外，時態邏輯與模態邏輯的混合也具有強烈的研究動機。一般單維時態邏輯被認為是復雜信息系統的表達和推理形式工具，而添加模態混合可以增強其表達力，使其可表達平行的論域、過程或代理，并且也讓表示無限大小的系統成為可能。例如時態和模態邏輯的混合可以用來刻畫知識或信仰如何隨時間發生變化。從哲學的角度來看，時態和模態相結合的邏輯系統也是一個有趣的問題，因為這些邏輯在原始的哲學問題上有著廣泛的應用領域，例如因果關系理論、行為理論等。這方面的研究始于托馬斯（R.Thomason，[13]）。不同的時態和模態邏輯的混合邏輯被許多學者所關注，例如在[10]中萊夫（J.Reif）和希斯塔拉（A.Sista）提出了一種時態和空間模態混合的邏輯，而雷洛茲（M.Reynolds）在[11]中考慮了時態邏輯K4.3.t和模態邏輯S5的混合邏輯，并證明了這種混合邏輯雖然具有可判定性但卻不具有窮模型性。本文考慮了雷洛茲的混合邏輯的基礎邏輯即時態邏輯K4.t和模態邏輯S5的混合邏輯。與時態邏輯K4.3.t和模態邏輯S5的混合邏輯不同，本文證明了K4.t和模態邏輯S5的混合邏輯具有有窮模型性。鑒于時態邏輯也是模態邏輯的一種，同時本文對混合時態模態邏輯的研究方法同樣也適用于時態邏輯與時態邏輯，或者模態邏輯與模態邏輯之間的混合。因此在本文中統一將這三種混合邏輯稱為混合模態邏輯。

本文給出了一種適用于混合模態邏輯有窮模型性的一般性證明方法，并用該方法證明了時態邏輯K4.t和模態邏輯S5的混合邏輯具有有窮模型性。該邏輯是傳遞性基礎時態邏輯K4.t和認知邏輯S5的混合邏輯，是重要的基礎混合時態模態邏輯，同時也是雷洛茲考慮的混合邏輯的基礎邏輯。該邏輯的有窮模型性是未知的，本文給出了肯定的回答。同時本文所采用的有窮模型性證明方法還可以被直接應用到混合模態邏輯M×M,M×N 和N×N 中。其中M 為基礎時態邏輯K.t（[14]）的D,T,B,4 擴張，而N 為模態邏輯的D,T,B,4 擴張。本文證明有窮模型性的方法是一種代數證明論方法。該方法關鍵在于構造基于目標邏輯且滿足內插引理的矢列。此條內插引理源于克拉格（Crag）的內插引理，由魯達（D.Rooda）首次引入到蘭貝克演算。這條性質被用來證明一些子結構邏輯的表達力等價于上下文無關文法語言。如彭圖斯（M.Pentus，[9]）證明了蘭貝克演算的表達力等價于上下文無關文法語法。該引理也被范拉列斯基（M.Farulewski，[2]）和布斯科沃夫斯基（W.Buszkowski，[1]）應用于證明非結合的蘭貝克演算及其多種格上延伸的強有窮模型性和嵌入性。林哲（Z.Lin，[7,8]）修改此條性質并應用于證明不同的非經典模態邏輯的有窮模型性或強有窮模型性。本文證明方法源自[7,8]中的方法，并在此基礎上做了拓展，簡化并應用到經典時態與模態邏輯中。

本文結構安排如下：第2 節中引入K4.t×S5混合邏輯，同時給出了其對應的代數及矢列演算系統。第3 節中證明K4.t×S5混合邏輯具有有窮模型性，并討論了該結論如何擴展到其他一般混合時態和模態邏輯中，第4 節總結了本文的工作并展望了進一步的研究前景。

2 混合邏輯的代數語義及矢列演算系統

定理1.矢列演算系統G對于K4.t×S5代數類是有效完全的。

對于有效性的證明，只需要逐條檢驗定義4中的(1) (10)在G中都成立即可。而完全性的證明可以由經典的塔斯基林登鮑姆構造證明，也可由下節有窮模型性的證明得到。

3 有窮模型性

本節證明矢列演算系統G具有代數有窮模型性。令S為一矢列演算，K(S)為其對應的完全有效的代數類。如S=G，則K(G)是K4.t×S5代數類。一個矢列演算系統S有代數有窮模型性指的是：如果對于S中的任意矢列Γ?β，/?SΓ?β，那么必然存在一個有窮代數A ∈K(S)，使得/|=AΓ?β。對任意公式α,令sub(α)表示其所有子公式組成的集合。令T為一個公式集合，定義s(T)。

定義6.令s(T)為滿足下面所有條件的最小公式集：

則可得到混合邏輯KD4.t×S5，由于在上面有窮模型性的證明中D的證明類似于T的證明，因此易得到KD4.t×S5的有窮模型性。另在時態上考慮B的擴張，則有?=?，那么可以得到相應模態混合擴張的有窮模型性。如在K4.t×S5增加K4.t的B 性質及相關證明，那么可以得到K4×S5的有窮模型性證明。同樣考慮兩時態邏輯混合只需要重復時態部分的證明即可得到相應的混合邏輯的有窮模型性證明，如K4.t×K4.t。綜上所述通過該方法我們可以得到當K1和K2是經典時態邏輯K.t或經典模態邏輯K上的D,T,B,4 組合擴張時，K1和K2的混合邏輯同樣具有有窮模型性。

4 結論

本文證明了時態邏輯K4.t和模態邏輯S5的混合邏輯具有窮模型性，并且該結果可延伸為一般性的結果：當K1和K2是經典時態邏輯K.t或經典模態邏輯K上的D,T,B,4 組合擴張時，K1和K2的混合邏輯同樣具有有窮模型性。

本文建立一種證明混合時態邏輯和混合模態邏輯的有窮模型性的一般證明方法。該方法也可以被用來證明常見的正規模態或時態邏輯的有窮模型性。本文的證明方法基于代數證明論，其關鍵是證明混合的兩個單維時態或模態邏輯存在滿足內插引理性質的矢列演算系統。在未來的研究中我們將嘗試給出存在內插引理性質的矢列演算系統的時態或模態邏輯的代數條件，以期將本證明拓展為更一般的結果。