多模態(tài)公理化系統(tǒng)的可分離性研究

趙 賢

(河北大學 哲學系，河北保定 071002)

多模態(tài)邏輯是指包含兩種或兩種以上模態(tài)算子的邏輯系統(tǒng)，且算子間不能規(guī)約。在多模態(tài)邏輯的公理化系統(tǒng)中，不同的模態(tài)算子有不同的演繹方式，即與不同模態(tài)算子相關的(單)模態(tài)系統(tǒng)(子系統(tǒng))是不同的。例如有的多模態(tài)系統(tǒng)同時包含T類型的模態(tài)算子□1，S4類型的模態(tài)算子□2，以及KD類型的算子集(□13，…，□n3)等。

從一般意義上考察多模態(tài)系統(tǒng)的公理化，則面臨下述問題:在何種程度上一個多模態(tài)系統(tǒng)可以被看作是多個(單)模態(tài)系統(tǒng)的疊加?或已知多模態(tài)系統(tǒng)L的公理化及其語言中的任意算子O，能否得到與O相關的子公理化系統(tǒng)?

上述問題即多模態(tài)系統(tǒng)的可分離性關注的主要內容，本文將在多模態(tài)公理化系統(tǒng)及其子系統(tǒng)基礎上對這一問題展開研究。

一、多模態(tài)邏輯系統(tǒng)的公理化

多模態(tài)邏輯系統(tǒng)內包含兩種或兩種以上的模態(tài)算子，不同模態(tài)算子的聯(lián)合問題既是多模態(tài)邏輯研究的核心，也是多模態(tài)邏輯系統(tǒng)公理化的核心。根據(jù)多模態(tài)系統(tǒng)內模態(tài)算子、公理及規(guī)則的組合方式，多模態(tài)系統(tǒng)可分為包含交互作用的系統(tǒng)和不包含交互作用的系統(tǒng)。本文將分別考察這兩類公理化系統(tǒng)的可分離性問題。

一個多模態(tài)邏輯系統(tǒng)L是一個模態(tài)公式集，它包含重言式且在經(jīng)典邏輯的推理規(guī)則下封閉。L是可公理化的意思是指，存在公理集和相關規(guī)則能夠生成L的所有定理。公理化這一概念可形式化表述為:

(1)一個公理化系統(tǒng)是一個二元組Ax=〈Γ，R〉，其中Γ是公式集(也被稱為公理集)，R是推理規(guī)則的集合;

(2)如果R是空集，則Ax和Γ是等同的;

(3)公理化系統(tǒng)的集合 Axi=〈Γi，Ri〉(1≤i≤n)是公理化系統(tǒng) Ax=〈Γ，R〉的并，其中Γi是集合Γ的并，Ri是集合R的并。

假設此處考察的系統(tǒng)在替代規(guī)則下是封閉的，此處使用的是公理模式而不是公理。同時假設所有的公理化系統(tǒng)(包括公理化系統(tǒng)的子系統(tǒng))包含命題演算的重言式，分離規(guī)則和替代規(guī)則。

定義1.1:已知 L是多模態(tài)語言，Ax=〈Γ，R〉是其公理化系統(tǒng)。

(1)如果O是模態(tài)算子，用Γ(O)表示屬于子語言L(O)的公式集Γ，同樣的，用R(O)表示與L(O)中公式有關的規(guī)則集R;最后Ax(O)被記作〈Γ(O)，R(O)〉，表示從Ax中提取的O的公理化系統(tǒng)或與O相關的子系統(tǒng)的公理化。注意，此處使用的替代規(guī)則僅僅是針對于L(O)的公式。

(2)若Ax是包含Γ且在推理規(guī)則R下封閉的極小的多模態(tài)公理化系統(tǒng)，則這一系統(tǒng)被記作MML(Ax)(MML為Multimodal Logic的簡寫)。如果R是空集，則用MML(Γ)表示由公式集Γ進行公理化的多模態(tài)邏輯系統(tǒng)。

(3)類似地，如果Γ和R出現(xiàn)在單模態(tài)語言中，則用ML(Ax)表示包含Γ且在推理規(guī)則R下封閉的極小的單模態(tài)公理化系統(tǒng)。如果R是空集，則用ML(Γ)表示由公式集Γ進行公理化的單模態(tài)邏輯系統(tǒng)。

假設本文研究的多模態(tài)邏輯是正規(guī)系統(tǒng)，則分別用NMML(Ax)和NMML(Γ)表示由Ax或公式集Γ進行公理化的正規(guī)多模態(tài)邏輯系統(tǒng)。在單模態(tài)情況下，分別用NML(Ax)和NML(Γ)表示正規(guī)單模態(tài)邏輯系統(tǒng)。

上述定義是單模態(tài)邏輯相關定義［1］的一個簡單擴展。如果只考慮正規(guī)系統(tǒng)，則有如下經(jīng)典模態(tài)邏輯系統(tǒng):

· K=NML(?)

· D=NML({◇T})=NML({□p→◇p})

· T=NML({□p→p})

· B=NML({□p→p，p→□◇p})

定義1.2:已知L是多模態(tài)邏輯系統(tǒng)。如果存在一個公理化系統(tǒng) Ax=〈Γ，R〉，滿足 L=MML(Ax)，則稱L是可公理化的，Ax是L的公理化系統(tǒng)。

如果Γ是有窮的，則稱L是可有窮公理化的。對于任意可公理化的系統(tǒng)L而言，可以將其看作L公理的所有定理集(即Γ=L)。L是可有窮公理化的情況是研究多模態(tài)邏輯公理化系統(tǒng)的主要內容。在多數(shù)情況下，采用Γ進行公理化。

如果L是可公理化的，那么L系統(tǒng)的定理α的證明可定義為公式的序列(α1，…，αn)，該序列滿足:(1)αn=α;(2)αi或者是L的公理或者是使用 L 的推理規(guī)則可從(α1，…，αi－1)推出。

二、多模態(tài)公理化系統(tǒng)的子系統(tǒng)

定義2.1:任意邏輯系統(tǒng)可看作是一個公式集。已知L是多模態(tài)邏輯系統(tǒng)，O是任意模態(tài)算子，L是多模態(tài)語言，L(O)是與算子O相關的子語言。用L(O)表示與O相關的子系統(tǒng)，L(O)是出現(xiàn)在 L(O)中的 L的定理集，即:L(O)={α∈L(O)/├Lα }=L(O)∩L。

定理2.2:集合L(O)是相對于子語言L(O)定義的模態(tài)邏輯系統(tǒng)［2］。

證明:很容易證明L(O)包含所有的重言式(因為L(O)就在L之中)在分離規(guī)則下是封閉的(因為L(O)和L在分離規(guī)則下是封閉的)，在替代規(guī)則下也是封閉的。①在這個規(guī)則中，L(O)在L(O)的公式中是封閉的:如果α∈L(O)，且 β∈L(O)，則 α［p/β］∈L(O)，其中 α［p/β］是用 β替換α中所有p的出現(xiàn)。與之對應的，L(O)在一般的替代規(guī)則下是不封閉的:因為如果用β替換不出現(xiàn)在L(O)中的p的出現(xiàn)，則公式α［p/β］就不在L(O)中，也就不在L(O)中。

另外，如果O是唯一的模態(tài)算子，那么L(O)和L是一致的。

定義2.3:若Γ是多模態(tài)公式集且O是已知的算子，則Γ(O)是Γ中某類公式的集合，其中O是唯一的模態(tài)算子:Γ(O)=?！蒐(O)={α∈Γ/α∈L(O)}。

如果Oσ是O的對偶模態(tài)，若Γ(O)包含公式Γ，其中算子是Oσ或On，則O和Oσ確定了相同的模態(tài)邏輯子系統(tǒng)，即L(O)=L(Oσ)。其中O不一定是原子模態(tài)算子，也可能是復合模態(tài)。②在原子模態(tài)算子基礎之上，通過模態(tài)形成算子生成的模態(tài)算子。

因此，能夠定義與任意模態(tài)算子O相關的子系統(tǒng)L(O)。那么整個系統(tǒng)L是不是L(O)系統(tǒng)的疊加呢?系統(tǒng)L的性質與子系統(tǒng)L(O)的性質的關系是什么?此時需要用到演繹邏輯中保守擴展的概念:

定義2.4:如果L和L'是分別由語言L和L'構建的邏輯系統(tǒng)，且L?L'，如果對于任意公式α而言，├Lα?├L'α，則稱L'是 L的保守擴展。

根據(jù)子系統(tǒng)L(O)的定義(參見2.1)，多模態(tài)系統(tǒng)L是每個子系統(tǒng)L(O)的保守擴展。由此可以確定這些子系統(tǒng)的性質，但這并沒有直接回答系統(tǒng)L是不是L(O)系統(tǒng)的疊加，而“疊加”這一概念涉及到系統(tǒng)L和子系統(tǒng)L(O)的公理化問題。因此，產生下述問題:如果L是可(有窮)公理化的且O是任意模態(tài)算子，那么子系統(tǒng)L(O)是可(有窮)公理化的嗎?

換言之，已知L系統(tǒng)的有窮公理化Ax，能夠由Ax推導出L(O)的有窮公理化嗎?或者，如果Ax是L的公理化系統(tǒng)，那么是否存在子系統(tǒng)L(O)的公理化系統(tǒng)，即提取的公理化Ax(參見1.1(1))?由此又產生了新的問題:如果Ax是L的有窮公理化系統(tǒng)，那么在何種情況下提取的公理化系統(tǒng)Ax(O)是子系統(tǒng)L(O)的有窮公理化?即:如果Ax是L的有窮公理化系統(tǒng)，L=MML(Ax)且L(O)=MML(Ax)(O);如果Ax(O)是L(O)的有窮公理化系統(tǒng)，且L(O)=ML(Ax(O))。上述問題改述為:在何種情況下 MML(Ax)(O)=ML(Ax)(O))?

此時則需引入公理化可分離性的概念:

定義2.5:公理化系統(tǒng)Ax(或公式集 Γ)是可分離的，則對于任意原子算子O而言，滿足MML(Ax)(O)=ML(Ax(O))(或 MML(Γ)(O)=ML(Γ(O)))［3］。

引理2.6:對于任意公理化Ax和任意算子O而言，ML(Ax(O))?MML(Ax)(O)。

證明:如果α∈ML(Ax(O))，那么在 ML(Ax(O))中存在α的一個證明，即在L(O)中存在公式序列 α1，…，αn，其滿足:每個 αi或者是 Ax(O)的公理或者是使用Ax(O)的推理規(guī)則從之前的公式得到的;并且這一證明在MML(Ax)中是有效的，因為Ax(O)的公理或者推理規(guī)則在Ax中也是有效的。因此，α也是MML(Ax)的定理，又因為α∈L(O)，則最終 α∈MML(Ax(O))。

另外，多模態(tài)邏輯系統(tǒng)L的公理化Ax的可分離性也可以表述為:對于任意原子算子O而言，L是ML(Ax(O))的保守擴展(參見2.4)。

上述定理的相反方向，即MML(Ax)(O)?ML(Ax(O))，可表述為:如果 α 是 L=MML(Ax)的定理，且O是唯一的模態(tài)算子，那么α也是(單)模態(tài)系統(tǒng) ML(Ax(O))的定理，即 α是可以由Ax(O)推出的。然而，這一性質并不是所有的公理化都滿足的。

如果Ax是可分離的公理化，那么“(單)模態(tài)系統(tǒng)的疊加”這一概念就變得清晰:Ax是由若干Ax(O)組成，并且每個Ax(O)可以由與原子算子O相關的(單)模態(tài)邏輯系統(tǒng)進行公理化。如果假設{O1，…，On}是有窮的原子模態(tài)算子集，那么上述關系可以表示為:

一般來講，在直覺中有這樣一個畫面:多模態(tài)邏輯的公理化系統(tǒng)似乎都是可分離的。這是因為一直以來我們將多模態(tài)系統(tǒng)L等價于多個子系統(tǒng)L(O)的疊加。實際上，決定多模態(tài)公理化系統(tǒng)是否可分離，除了多模態(tài)系統(tǒng)L與子系統(tǒng)L(O)各自的性質之外，另一個重要的因素是該多模態(tài)系統(tǒng)是否包含交互作用，這是決定多模態(tài)公理化系統(tǒng)是否可分離的關鍵。

三、基于交互作用的公理化分離標準

上文將多模態(tài)邏輯系統(tǒng)分為包含交互作用公理的多模態(tài)系統(tǒng)和不包含交互作用公理的多模態(tài)系統(tǒng)。是否包含交互作用公理作為判定多模態(tài)公理化系統(tǒng)是否可分離的一個重要標準，本文將對其進行形式化定義。

定義3.1:已知L是多模態(tài)邏輯系統(tǒng)

(1)如果交互作用公理涉及到不同的模態(tài)算子O1，…，On，那么系統(tǒng)的公理、定理及推理規(guī)則都會有所涉及;

(2)如果該公理化系統(tǒng)包含或不包含公理或推理規(guī)則的交互作用，則被稱為包含或不包含交互作用的公理化系統(tǒng);

(3)如果邏輯系統(tǒng)L的公理化包含或不包含交互作用，則稱L是一個包含或不包含交互作用的邏輯系統(tǒng)。

例如，如果模態(tài)算子集為{□1，…，□n，◇1，…，◇n}，則公理□1α→□2□1α是交互作用公理，規(guī)則是交互作用規(guī)則［4］。如果O是系統(tǒng)內唯一的模態(tài)算子，則稱公理或規(guī)則是關于模態(tài)O的。因此，一個不包含交互作用的公理化只包含單模態(tài)的公理和推理規(guī)則。

直覺上講，一個不包含交互作用的多模態(tài)公理化系統(tǒng)是(單)模態(tài)系統(tǒng)的疊加。實際上，可以表明下面的結論:

定理3.2:已知Ax是多模態(tài)系統(tǒng)L的公理化。如果Ax不包含交互作用，那么Ax是可分離的。

證明:已知O是原子算子，則根據(jù)引理2.6需要表明L(O)?ML(Ax(O)。首先，單模態(tài)O的推理規(guī)則R∈Ax(O)，如果R的后件在子語言L(O)中，那么R的前件也在L(O)中。因此α∈L(O)，即├Lα且α∈L(O)。其次，需要表明α∈ML(Ax(O))，即α可以由Ax的提取公理化Ax(O)推導得出。因為├Lα，已知α1，…，αn是L中α的一個證明，則需要表明這一證明在ML(Ax(O))中也是有效的:

· 對于i=n可得αn=α∈L(O)

· 假設 αi∈L(O):如果 αi是 L的公理，αi是Ax(O)的公理;如果αi可以通過L的推理規(guī)則R得到，那么R是單模態(tài)的(因為Ax不包含交互作用)。并且R必然在Ax(O)中，因為之前假設αi在L(O)中。此外，R的前件也在L(O)中，因此 αi－1∈L(O)。

根據(jù)歸納，可以表明對于所有1≤i≤n而言，有(1)αi∈L(O)且(2)αi或者是 Ax(O)的公理或者可以根據(jù)Ax(O)之前的規(guī)則得到。證明α1，…，αn在ML(Ax(O))中是有效就表明α∈ML(Ax(O))。

推論3.3:已知Γ是多模態(tài)公式集，其中包含原子算子 O1，…，On，1≤i≤n。如果 Γ 不包含交互作用公式，那么Γ是可分離的，即MML(Γ)(Oi)=ML(Γ(Oi))。(證明略)

例如，公式集 Γ ={□1α→◇1α，□2α→α}是可分離的，并且 NMML(Γ)(□1)=NML({□1α→◇1α})=KD 系統(tǒng)，NMML(Γ)(□2)=NML({□2α→α})=T系統(tǒng)。這也表明，在雙模態(tài)系統(tǒng)NMML(Γ)中，任意與□1(或□2)相關的定理就是KD系統(tǒng)(或T系統(tǒng))的定理。

上述推理表明不包含模態(tài)算子之間的交互作用的公理化是可分離的。對于包含模態(tài)算子交互作用的多模態(tài)公理化系統(tǒng)而言，不同模態(tài)算子的演繹方式會因其算子間的交互作用發(fā)生變化，而導致包含交互作用的多模態(tài)公理化系統(tǒng)不可分離。本文將用一個具體的例子對此進行說明。

一般認為多模態(tài)系統(tǒng)是通過下述方式構建的［5］:

(1)對于每個原子模態(tài)算子O而言，可構建系統(tǒng)(初始公理化)去描述O，這一系統(tǒng)是可有窮公理化的(例如T，S4等);

(2)(可能)添加一些算子之間的交互作用公理;

(3)如果語言中包含模態(tài)算子之上的一些形式運算，則需給出一些公理去刻畫這些形式運算(例如動態(tài)邏輯中的并和附和)。

由此推斷:與算子O相關的子系統(tǒng)L(O)即是O的初始公理化系統(tǒng)。然而，子系統(tǒng)L(O)不一定與O的初始公理化系統(tǒng)重合!因為算子之間的交互作用會使得算子O產生新的性質(可推導的)。例如，已知L是一個正規(guī)的雙模態(tài)系統(tǒng)，其構建方式如下:

· L的語言包含原子算子集{□1□2◇1◇2}，

·□1是正規(guī)算子，且是自返的(T系統(tǒng))，

·□2是正規(guī)算子(K系統(tǒng))，

· 滿足公理□2α→□1α

經(jīng)過推導會發(fā)現(xiàn):L(□2)不是系統(tǒng)K而是系統(tǒng)T!實際上，在L中□2會變成自返的，因為在L(□2)中，根據(jù)□1α→α 和□2α→□1α 可得□2α→α。根據(jù)公理化Ax=Γ ={□1α→α，□2α→□1α}，NMML(Ax)(□2)=系統(tǒng) T，而 NML(Ax(□2))=NML(?)=系統(tǒng)K;所以 NML(Ax(□2))?NMML(Ax(□2))。因此，這一公理化系統(tǒng)是不可分離的(參見2.6)。換言之，L不是K之于□2的保守擴展。究其原因在于這一系統(tǒng)中包含模態(tài)算子的交互作用，即□2α→□1α。

根據(jù)上述例子可以看出NMML(Ax)(□2)包含多個T系統(tǒng)(因為□2是自返的)，然而在實際操作中如何證明它是T系統(tǒng)呢?換言之，如果將公理□2α→α添加到上述公理化中，得到的公理化Ax=Γ ={□1α→α，□2α→□1α，□2α→α}是可分離的嗎?

于是又面臨這樣一個問題:即定義一個標準去判定一個給定的公理化是否是可分離的。這一問題可以在多模態(tài)邏輯的決定性基礎上進行研究，本文對此不加詳述。

四、結束語

通過對多模態(tài)系統(tǒng)的公理化的定義、性質等進行細致的考察，并對多模態(tài)公理化系統(tǒng)的子系統(tǒng)的性質進行研究，表明不包含交互作用的多模態(tài)系統(tǒng)的公理化是可分離的，并對此進行了證明。這一結論是進一步精確分析多模態(tài)系統(tǒng)的一般性質、多模態(tài)系統(tǒng)與其子系統(tǒng)之間的關系以及研究多模態(tài)邏輯相關結論的“漸增參考(cumulativity)”問題的重要基礎，這將有助于構建更加完整的多模態(tài)邏輯一般理論。對于包含交互作用的多模態(tài)公理化系統(tǒng)而言，本文僅給出了一個具體的例子說明其公理化不可分離，但未對此給出普遍性的結論，這是今后需要研究的問題。

［1］Van Benthem J.Modal logic and classical logic［M］.Monographs in Philosophical Logic and Formal Linguistics Bibliopolis，Naples，1985.

［2］Chellas B F.Modal Logic:An introduction［M］.London:Cambridge University Press，1980:58 －62.

［3］Catach L.Les Logiques Multimodales［D］.Univérsité de Paris VI，F(xiàn)rance，1989:88 －89.

［4］Catach L.Normal multimodal logic［G］//Proceedings of AAAI’88-Seventh National Conference on Artificial Intelligence.CA:The AAAI Press，1988:491 －495.

［5］Carnielli W，Pizzi C，Modalities and Multimodalities［M］.Logic，Epistemology，and the Unity of Science 12，? Springer Science+Business Media B.V.2008:234.