正规多模态逻辑的混合系统

霍 旭

(安徽大学 数学科学学院， 安徽 合肥 230601)

多模态逻辑是单模态逻辑的扩充，它包含有两个或两个以上乃至可数无穷多个初始模态词，如时态逻辑和认知逻辑系统都是多模态逻辑。要把多模态逻辑作为一类对象来研究就要引进能涵盖更多多模态系统的一般理论。Walter Carnielli和Claudio Pizzi在专著ModalitiesandMultimodalities中提出了更为一般化的多模态逻辑系统，证明了这些系统的完全性[1]。把模态逻辑混合化的工作始于新西兰籍逻辑学家亚瑟·普莱尔(Arthur N.Prior)[2]。Torben Braüner在其专著HybridLogicanditsProof-Theory中对经典模态逻辑的混合化的工作进行了系统的研究[3]。把多模态逻辑完全性和混合逻辑完全性证明合并起来可以证明多模态混合系统的完全性，但是还没有相关文献给出详细的证明，本文将给出。

一、多模态语言

一个多模态命题语言(multimodal propositional language)定义为用原子模态参数(atomic modal parameters)的(固定的)集合Φ0扩充的正规模态命题语言。这种语言除了包含在Var(变元的集合)中的命题变元，符号⊥和→之外，基本字母表还包括原子模态参数a,b,c,…。模态参数是用来标示模态算子的，其中有两个特殊的参数：空参数，记为0；同一参数，记为1。

Φ0上的模态参数类Φ定义为根据Φ0在如下运算∪和⊙下封闭的集合：

1．如果a∈Φ0，那么a∈Φ。

2．如果a,b∈Φ0，那么a∪b∈Φ并且a⊙b∈Φ。

由模态参数标示的模态算子的类Ξ定义为：如果a∈Φ，那么[a]∈Ξ。

把Ξ的元素看作用组合代理人(agent)标记的模态算子，这些代理人相互的态度由这些多模态算子控制，这样可以给多模态语言一个直观的解释。例如，我们可以把多模态算子[a∪b]解释为由代理人a和b分享的“知道”“必然”或“义务”。类似地，[a⊙b]可以表示代理人a相对于(依赖于)b的“知道”“必然”或“义务”。当然这些解释不是唯一的。

多模态算子可以看作程序(process)的标签。于是，多模态系统是看作对串行程序(serial processes)(在a⊙b的情形)和并行程序(parallel processes)(在a∪b的情形)的逻辑的形式化，[1]被看作恒等程序(identity process)，[0]被看作程序中的终止条款(halting clause)。

多模态合式公式按照通常的方式定义，如果涉及到多模态算子，再加上如下条款：

如果φ∈WFF(WFF表示合式公式集合)并且[a]∈Ξ，那么[a]φ∈WFF。

对任何模态算子[a]，我们定义〈a〉如下：

〈a〉φ=df﹁[a]﹁φ

用于定义多模态语义的关键思想是，关系Ra和每个模态参数a相关，使得模态公式[a]φ和〈a〉φ在模型M的世界w∈W中的可满足性由如下两个条件决定：

(1)M,w[a]φ 当且仅当对所有w′∈W，wRaw′蕴涵M,w′φ。

(2)M,w〈a〉φ当且仅当存在w′∈W，wRaw′并且M,w′φ。

二、多模态逻辑的公理

基本的多模态系统是最小模态逻辑系统的多模态扩充。由这个系统加上一系列的公理模式可以得到更复杂的多模态系统，如基底系统(basilar systems)、肯定系统(affirmative systems)、Catach-Sahlqvist系统(Catach-Sahlqvist systems)等等[1]213。本文主要给出标准的(Standard)正规的(Normal)多模态逻辑，它就是最小模态系统的多模态版本。

定义2.1 所有基于模态参数的集族(collection)Φ的多模态系统SΦ，是包含所有PC(经典命题逻辑)重言式的(多)模态公式的集族，并且在经典命题规则(MP)和(US)(代入规则)下封闭。

首先假定我们所说的多模态系统都包含定义2.2中的公理，即正规的和标准的多模态系统。在不引起混淆的情况下可以把它仅仅记作S而不是SΦ。

定义2.2 令SΦ是一个多模态系统，那么SΦ被称为：

(a)正规的，如果它对每个原子模态参数a∈Φ0，公式φ和ψ，满足正规性公理(Normality Axiom)(K[a])：

[a](φ→ψ)→([a]φ→[a]ψ)

和必然化规则(Necessitation Rule)(Nec[a])：

(b)标准的，如果它对每个a,b∈Φ和公式φ，满足多模态算子的公理(Axioms for Multimodal Operators)：

(MM3) [a⊙b]φ≡ [a][b]φ 串行程序公理(Axiom of serial processes)

(MM4) [1]φ≡φ 中立程序公理(Axiom of neutral process)

对原子模态参数引进的正规性公理和必然化规则，可以扩展到所有模态算子，这就是下面的命题。

命题2.3 对每个多模态系统S和c∈Φ，下面条款成立：

(1) [c](φ→ψ)→([c]φ→[c]ψ)

证明：

(1) 根据对多模态算子的复杂性实施归纳。如果c是原子的，根据定义结果成立。如果c是a∪b，则

1.[a∪b](φ→ψ) [假设]

4.[a](φ→ψ) [3,PC]

5.[b](φ→ψ) [3,PC]

6.[a]φ→[a]ψ [4,归纳假设]

7.[b]φ→ [b]ψ [5,归纳假设]

13.[a∪b]φ→[a∪b]ψ [(MM1),12,PC]

如果c是a⊙b,证明类似。

命题2.4 多模态算子的公理(即定义2.2中的公理(MM1)-(MM4))等价于如下条款：

(3) 〈a⊙b〉φ≡ 〈a〉〈b〉φ

(4) 〈1〉φ≡φ

证明：直接根据多模态算子的公理和定义〈a〉φ=df﹁[a]﹁φ实施归纳。

标准正规多模态系统、基底系统、肯定系统、Catach-Sahlqvist系统的完全性采用极大一致集(MCS)方法已经给出了证明[1]222-235。

三、@算子的引进

本文给出的混合多模态逻辑是通过在正规多模态逻辑中增加被称为名词性词(nominal)的第二类命题符号和满足算子而得到的[4]。用w，v，u，t等表示状态和名词性词的变元，名词性词用来命名状态，这里用同样的符号表示而不加区分。符号@w称为满足算子。如果φ是合式公式，@wφ也是合式公式。

现在考虑增加部分的语义。令M=(W,R,V)是一个模型，g是M上的一个指派，Den(w)是状态符号w的指称(即如果w是状态变元，Den(w)是g(w)；如果w是名词性词，Den(w)是V(w))。于是：

M,g,v@wφ当且仅当M,g,Den(w)φ,即满足算子@w让我们跳到w的指称，并在那里对φ的变元赋值。

我们通过在S中增加关于@的公理和规则，将会得到混合化的公理系统，记为H[@](S)。

下面给出@的公理和规则。首先引进@w-必然化规则：

除了这个规则之外，下面还将引进被称为Name和Paste的规则。

下面引进@的公理，共有3组。第一组：

K @w(φ→ψ)↔(@wφ→@wψ)

Self-Dual @wφ↔﹁@w﹁φ

其中，K是模态分配模式，因为我们有@w-必然化规则，所以@w是正规模态算子。Self-Dual告诉我们@w是一个其转换关系是一个函数的模态。Introduction告诉我们如何引进@算子辖域下的信息。我们根据Introduction和Self-Dual可得到消解(Elimination)模式：

第二组公理是标记的模态理论(modal theory of labeling)(或者称为状态等式的模态理论(modal of state equality))：

Label @ww

Nom @wv→(@vφ→@wφ)

Swap @wv→@vw

Scope @v@wφ↔@wφ

第三组告诉我们@和〈c〉是怎样相互影响的，其中c∈Φ0：

Back 〈c〉@wφ→@wφ

Back和Bridge公理只是给出了c∈Φ0的情形，事实上在c∈Φ时它们也成立，因此有需要证明的命题3.1。

命题3.1 当c∈Φ时Back和Bridge公理成立。

证明：

(1)证明Back公理。根据多模态算子的复杂性实施归纳。当c是原子时，所证成立。

当c是a∪b时，则

1．〈a〉@wφ→@wφ [归纳假设]

2．〈b〉@wφ→@wφ [归纳假设]

4．@wφ→@wφ [3，命题2.4(1)]

当c是a⊙b时，则

1．〈a〉@wφ→@wφ [归纳假设]

2．〈b〉@wφ→@wφ [归纳假设]

3．﹁@wφ→[b]﹁@wφ [2，PC]

4．[a]﹁@wφ→[a][b]﹁@wφ [3，命题2.3，MP]

5．〈a〉〈b〉@wφ→〈a〉@wφ [4，PC]

6．〈a〉〈b〉@wφ→@wφ [5，1，MP]

7．〈a⊙b〉@wφ→@wφ [6，命题2.4(3)]

(2) 证明Bridge公理。同样用归纳法。当c是原子时，所证成立。

当c是a∪b时，则

当c是a⊙b时，则

2．〈b〉w→(@wφ→〈b〉φ) [1，PC]

3．[a](〈b〉w→(@wφ→〈b〉φ)) [2，概括]

4．[a](φ→ψ)→(〈a〉φ→〈a〉ψ) [命题2.3]

5．〈a〉〈b〉w→〈a〉(@wφ→〈b〉φ)) [3，4，代入]

11．@wφ→[a]@wφ [Back，Self-Dual]

由上面所证可知命题成立。

下面再引进两个规则：

在两个规则中，v必须是不同于w的不在φ或θ中出现的状态符号(当然v和w可以用同一个名词性词代换)，c∈Φ0。

Paste规则在c∈Φ0时也成立，我们需要证明下面的命题。

命题3.2 当c∈Φ时Paste规则也成立。

证明：根据多模态算子的复杂性实施归纳。当c是原子时，所证成立。当c=0，1时，所证显然成立。

当c是a∪b时，则

7．@w〈a〉φ→θ [5，归纳假设]

8．@w〈b〉φ→θ [6，归纳假设]

11．@w(〈a∪b〉>φ)→θ [10，命题2.4(1)]

当c是a⊙b时，则

6．@u〈b〉φ→(@w〈a〉u→θ) [5，归纳假设]

8．@w〈a〉〈b〉φ→θ [7，归纳假设]

9．@w〈a⊙b〉φ→θ [8，命题2.4(3)]

由上面所证可知命题成立。

事实上，因为模态词至多有可数无穷多个，Back和Bridge公理和Paste规则中的条件c∈Φ0直接替换为c∈Φ也是成立的。命题3.1和3.2说明，正规多模态混合系统的模态词可以用原子参数标示的模态词表达出来，这有利于简化系统。至此我们得到公理系统H[@](S)。该系统可靠性易证，证明过程在此省略。

四、完全性证明

单模态词的混合逻辑系统的完全性已由P.Blackburn,M.de Rijke和Y.Venema给出了证明[5]434-443，下面参照他们的工作对标准正规多模态系统的完全性给出证明。

定义4.1(典型模型) 对于可数多模态语言L，典型模型Mc是(Wc,Rc,Vc)。其中Wc是所有L-MCS(公式的极大一致集)；Rc是Wc上的二元关系，定义为：ΓRcΔ当且仅当对所有L-公式φ，[a]φ∈Γ蕴涵φ∈Δ。Vc是赋值，定义为：Vc(α)={Γ∈Wc|α∈Γ}，其中α是一个命题符号或名词性词。

为便于证明下面的引理，称一个MCS是被标记的(labeled)当且仅当它包含一个状态符号；如果一个状态符号属于一个MCS，我们称它是那个MCS的标记(label)。

引理4.2 令Γ是一个被标记的MCS，并且对所有状态符号w，令Δw是{φ|@wφ∈Γ}。于是，

1．对每个状态符号w，Δw是包含w的被标记的MCS。

2．对所有状态符号w和v，@wφ∈Δv当且仅当@wφ∈Γ。

3．存在一个状态符号w使得Γ=Δw。

4．对所有状态符号w，Δw={φ|@wφ∈Δw}。

5．对所有状态符号w和v，如果w∈Δv，那么Δv=Δw。

证明：

还需要证Δw是极大的。假定不是，那么存在一个公式χ使得χ和﹁χ都不在Δw中。但是这样有@wχ和@w﹁χ都不属于Γ，根据Γ的极大一致性，﹁@wχ和﹁@w﹁χ都属于Γ。但这是不可能的，因为根据Self-Dual有@w﹁χ属于Γ，矛盾。所以Δw是极大的。

条款2。我们有@wφ∈Δv当且仅当 @v@wφ∈Γ。根据Scope，@v@wφ∈Γ当且仅当@wφ∈Γ。

条款3。根据假定，Γ至少包含一个状态符号；令它是w。如果能证明Γ=Δw，我们将得到所要的结果。假定φ∈Γ，因为w∈Γ，根据Introduction，@wφ∈Γ，因此φ∈Δw。反过来，如果φ∈Δw，那么@wφ∈Γ。所以，因为w∈Γ，根据Elimination我们有φ∈Γ。

条款4。使用Introduction和Elimination。

条款5。令Δv满足w∈Δv，我们将证明Δv=Δw。因为w∈Δv，我们有@vw∈Γ。根据Swap，也有@wv∈Γ。首先我们有Δv⊆Δw。因为，如果φ∈Δv，那么@vφ∈Γ。又因为@wv∈Γ，所以根据Nom得@wφ∈Γ，因此φ∈Δw。类似地可证明Δw⊆Δv。

引理4.4(扩充的Lindenbaum引理) 令L和L+是可数多模态语言，L+是L用新名词性词的一个可数无穷多集合扩充的结果。于是每个L-公式的一致集合可以扩充为一个由一个名词性词标记的粘贴的L+-MCS。

现在进行粘贴。列举L+的所有公式，定义Θ0为Θt，并假定已经定义了Θm，其中m≥0。令φm+1是列举中的第m+1个公式，定义Θm+1如下。如果Θm+1∪{φm+1}是不一致的，那么Θm+1=Θm。否则：

1．Θm+1=Θm∪{φm+1}，如果φm+1不是形如@w〈c〉φ的。这里w是一个状态符号。

令Θ=∪n≥0Θn。显然这个集合是由名词性词t标记的并且是极大的和粘贴的。而且，它还是一致的，因为这个膨胀的唯一非-平凡的方面是由第2条定义的，而Paste规则保证了这一步是保持一致性的。

定义4.5(标记的模型) 令Γ是一个由一个名词性词标记的粘贴的MCS。对于所有状态符号w，令Δw是{φ|@wφ∈Γ}，并定义W为{Δw|w是状态符号}。于是我们定义由Γ生成的标记的模型M为(W,R,V)，其中R和V是(典型关系)Rc和(典型赋值)Vc在W上的限制。

标记的模型有我们需要的所有结构。首先，根据引理4.2的条款3，Γ∈W，根据条款5，V是一个赋值，g是一个指派。还需要保证这样的模型关于模态是定义明确的，即我们需要存在引理。

引理4.6(存在(Existence)引理) 令M=(W,R,V)是由某名词性词标记的粘贴的集合Γ生成的模型。假定Θ∈W并且〈c〉φ∈Θ，那么存在Φ∈W使得ΘRΦ并且φ∈Φ。

引理4.7(真值引理) 令Θ是M中的被标记的MCS。对于所有公式φ，φ∈Θ当且仅当M, Θφ。

证明：根据归纳，原子的、布尔的和模态的步骤是标准的，略。我们需要证明关于满足算子@的情形。证明如下：M,Θ@wψ当且仅当M,Δwψ(根据引理4.2的条款5，Δw是唯一包含w的MCS，而且，根据本引理的原子情形，它是M中w在其中为真的唯一状态)，当且仅当ψ∈Δw(归纳假设)，当且仅当@wψ∈Δw(根据w∈Δw的事实，并且对从左到右的方向使用Introduction，对从右到左的方向使用Elimination)，当且仅当@wψ∈Θ(根据引理4.2的条款2)。这最后一步是证明完全性的关键！于是所有情形都已经被证明了，根据归纳，真值引理成立。

定理4.8(完全性) 可数多模态语言L中公式的每个H[@](S)-(极大)一致集合在可数标准模型中关于标准指派函数是可满足的。

证明：给定公式的H[@](S)-(极大)一致集合∑，使用扩充的Lindenbaum引理把它扩充为由可数语言L+的某名词性词标记的粘贴的集合∑+。令M=(W,R,V)是由∑+生成的标记的模型。根据引理4.2条款3，∑+∈W。根据真值引理，M,∑+∑+,进而有M,∑+∑。因为M中的每个状态是由L+的某名词性词标记的，并且名词性词只有可数多个，所以模型M是可数的。

[1] CARNIELLI W，PIZZI C.Modalities and multimodalities[M].Dordrecht：Springer,2008.

[2] 霍书全.普莱尔混合时态逻辑的思想基础[J].逻辑学研究，2016(2)：45-60.

[3] BRAüNER T.Hybrid logic and its proof-theory[M].New York：Springer,2011.

[4] BLACKBURN P.Nominal tense logic [J].Notre Dame Journal of Formal Logic,1993,34(1)：56-83.

[5] BLACKBURN P,DE RIJKE M,VENEMA Y.Modal logic [M].Cambridge:Cambridge University Press,2001.