多模態公理化系統的可分離性研究

趙 賢

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

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

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

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

一、多模態邏輯系統的公理化

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

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

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

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

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

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

定義1.1:已知 L是多模態語言，Ax=〈Γ，R〉是其公理化系統。

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

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

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

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

上述定義是單模態邏輯相關定義［1］的一個簡單擴展。如果只考慮正規系統，則有如下經典模態邏輯系統:

· K=NML(?)

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

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

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

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

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

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

二、多模態公理化系統的子系統

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

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

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

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

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

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

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

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

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

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

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

定義2.5:公理化系統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)的推理規則從之前的公式得到的;并且這一證明在MML(Ax)中是有效的，因為Ax(O)的公理或者推理規則在Ax中也是有效的。因此，α也是MML(Ax)的定理，又因為α∈L(O)，則最終 α∈MML(Ax(O))。

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

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

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

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

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

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

定義3.1:已知L是多模態邏輯系統

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

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

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

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

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

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

證明:已知O是原子算子，則根據引理2.6需要表明L(O)?ML(Ax(O)。首先，單模態O的推理規則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的推理規則R得到，那么R是單模態的(因為Ax不包含交互作用)。并且R必然在Ax(O)中，因為之前假設αi在L(O)中。此外，R的前件也在L(O)中，因此 αi－1∈L(O)。

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

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

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

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

一般認為多模態系統是通過下述方式構建的［5］:

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

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

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

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

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

·□1是正規算子，且是自返的(T系統)，

·□2是正規算子(K系統)，

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

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

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

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

四、結束語

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

［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，France，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.