彭玉 林哲

1 引言

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

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

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

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

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

2 混合邏輯的代數(shù)語義及矢列演算系統(tǒng)

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

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

3 有窮模型性

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

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

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

4 結論

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

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