多模态公理化系统的可分离性研究

赵 贤

(河北大学 哲学系，河北保定 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.