趙 賢

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

上述定義是單模態(tài)邏輯相關(guān)定義［1］的一個(gè)簡(jiǎn)單擴(kuò)展。如果只考慮正規(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)。如果存在一個(gè)公理化系統(tǒng) Ax=〈Γ，R〉，滿足 L=MML(Ax)，則稱L是可公理化的，Ax是L的公理化系統(tǒng)。

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

如果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)可看作是一個(gè)公式集。已知L是多模態(tài)邏輯系統(tǒng)，O是任意模態(tài)算子，L是多模態(tài)語(yǔ)言，L(O)是與算子O相關(guān)的子語(yǔ)言。用L(O)表示與O相關(guān)的子系統(tǒng)，L(O)是出現(xiàn)在 L(O)中的 L的定理集，即:L(O)={α∈L(O)/├Lα }=L(O)∩L。

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

證明:很容易證明L(O)包含所有的重言式(因?yàn)長(zhǎng)(O)就在L之中)在分離規(guī)則下是封閉的(因?yàn)長(zhǎng)(O)和L在分離規(guī)則下是封閉的)，在替代規(guī)則下也是封閉的。①在這個(gè)規(guī)則中，L(O)在L(O)的公式中是封閉的:如果α∈L(O)，且 β∈L(O)，則 α［p/β］∈L(O)，其中 α［p/β］是用 β替換α中所有p的出現(xiàn)。與之對(duì)應(yīng)的，L(O)在一般的替代規(guī)則下是不封閉的:因?yàn)槿绻忙绿鎿Q不出現(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的對(duì)偶模態(tài)，若Γ(O)包含公式Γ，其中算子是Oσ或On，則O和Oσ確定了相同的模態(tài)邏輯子系統(tǒng)，即L(O)=L(Oσ)。其中O不一定是原子模態(tài)算子，也可能是復(fù)合模態(tài)。②在原子模態(tài)算子基礎(chǔ)之上，通過(guò)模態(tài)形成算子生成的模態(tài)算子。

因此，能夠定義與任意模態(tài)算子O相關(guān)的子系統(tǒng)L(O)。那么整個(gè)系統(tǒng)L是不是L(O)系統(tǒng)的疊加呢?系統(tǒng)L的性質(zhì)與子系統(tǒng)L(O)的性質(zhì)的關(guān)系是什么?此時(shí)需要用到演繹邏輯中保守?cái)U(kuò)展的概念:

定義2.4:如果L和L'是分別由語(yǔ)言L和L'構(gòu)建的邏輯系統(tǒng)，且L?L'，如果對(duì)于任意公式α而言，├Lα?├L'α，則稱L'是 L的保守?cái)U(kuò)展。

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

換言之，已知L系統(tǒng)的有窮公理化Ax，能夠由Ax推導(dǎo)出L(O)的有窮公理化嗎?或者，如果Ax是L的公理化系統(tǒng)，那么是否存在子系統(tǒng)L(O)的公理化系統(tǒng)，即提取的公理化Ax(參見(jiàn)1.1(1))?由此又產(chǎn)生了新的問(wèn)題:如果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))。上述問(wèn)題改述為:在何種情況下 MML(Ax)(O)=ML(Ax)(O))?

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

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

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

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

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

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

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

一般來(lái)講，在直覺(jué)中有這樣一個(gè)畫面:多模態(tài)邏輯的公理化系統(tǒng)似乎都是可分離的。這是因?yàn)橐恢币詠?lái)我們將多模態(tài)系統(tǒng)L等價(jià)于多個(gè)子系統(tǒng)L(O)的疊加。實(shí)際上，決定多模態(tài)公理化系統(tǒng)是否可分離，除了多模態(tài)系統(tǒng)L與子系統(tǒng)L(O)各自的性質(zhì)之外，另一個(gè)重要的因素是該多模態(tài)系統(tǒng)是否包含交互作用，這是決定多模態(tài)公理化系統(tǒng)是否可分離的關(guān)鍵。

三、基于交互作用的公理化分離標(biāo)準(zhǔn)

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

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

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

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

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

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

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

定理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的后件在子語(yǔ)言L(O)中，那么R的前件也在L(O)中。因此α∈L(O)，即├Lα且α∈L(O)。其次，需要表明α∈ML(Ax(O))，即α可以由Ax的提取公理化Ax(O)推導(dǎo)得出。因?yàn)椹繪α，已知α1，…，αn是L中α的一個(gè)證明，則需要表明這一證明在ML(Ax(O))中也是有效的:

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

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

根據(jù)歸納，可以表明對(duì)于所有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)相關(guān)的定理就是KD系統(tǒng)(或T系統(tǒng))的定理。

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

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

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

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

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

由此推斷:與算子O相關(guān)的子系統(tǒng)L(O)即是O的初始公理化系統(tǒng)。然而，子系統(tǒng)L(O)不一定與O的初始公理化系統(tǒng)重合!因?yàn)樗阕又g的交互作用會(huì)使得算子O產(chǎn)生新的性質(zhì)(可推導(dǎo)的)。例如，已知L是一個(gè)正規(guī)的雙模態(tài)系統(tǒng)，其構(gòu)建方式如下:

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

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

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

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

經(jīng)過(guò)推導(dǎo)會(huì)發(fā)現(xiàn):L(□2)不是系統(tǒng)K而是系統(tǒng)T!實(shí)際上，在L中□2會(huì)變成自返的，因?yàn)樵贚(□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)是不可分離的(參見(jiàn)2.6)。換言之，L不是K之于□2的保守?cái)U(kuò)展。究其原因在于這一系統(tǒng)中包含模態(tài)算子的交互作用，即□2α→□1α。

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

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

四、結(jié)束語(yǔ)

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

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