彭玉 林哲

1 引言

所謂一個(gè)邏輯具有有窮模型性是指如果一公式在該邏輯系統(tǒng)中不可證，那么它在該邏輯系統(tǒng)的一有窮模型中不成立。有窮模型性是邏輯研究中重要的基礎(chǔ)性質(zhì)之一，此概念不僅本身具有重要意義，并且有廣泛應(yīng)用。一個(gè)有窮可公理化且具有有窮模型性的邏輯是可判定的。長(zhǎng)久以來(lái)，一邏輯是否具有有窮模型性是證明其是否可判定的重要方式。關(guān)于模態(tài)邏輯的有窮模型性有著廣泛的研究。模態(tài)邏輯的有窮模型性的一般證明方法是濾子方法（見(jiàn)[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)邏輯具有有窮模型性。時(shí)態(tài)邏輯的有窮模型性問(wèn)題也備受研究者們的關(guān)注，有部分時(shí)態(tài)邏輯被證明具有有窮模型性，也有部分被證明并不滿足有窮模型性，具體可參照賽格博格(K.Segerberg)的研究（[12]）。沃爾特（F.Wolter，[14]）考慮了時(shí)態(tài)邏輯有窮模型性的一般化結(jié)論，他將扎哈拉斯基夫在模態(tài)邏輯上的結(jié)論延伸到經(jīng)典時(shí)態(tài)邏輯中，證明了K4以上滿足一定典范框架條件的所有經(jīng)典時(shí)態(tài)邏輯具有有窮模型性。

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

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

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

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

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

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

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

3 有窮模型性

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

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

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

4 結(jié)論

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

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