霍 旭

(安徽大學(xué) 數(shù)學(xué)科學(xué)學(xué)院， 安徽 合肥 230601)

多模態(tài)邏輯是單模態(tài)邏輯的擴(kuò)充，它包含有兩個(gè)或兩個(gè)以上乃至可數(shù)無(wú)窮多個(gè)初始模態(tài)詞，如時(shí)態(tài)邏輯和認(rèn)知邏輯系統(tǒng)都是多模態(tài)邏輯。要把多模態(tài)邏輯作為一類對(duì)象來(lái)研究就要引進(jìn)能涵蓋更多多模態(tài)系統(tǒng)的一般理論。Walter Carnielli和Claudio Pizzi在專著ModalitiesandMultimodalities中提出了更為一般化的多模態(tài)邏輯系統(tǒng)，證明了這些系統(tǒng)的完全性[1]。把模態(tài)邏輯混合化的工作始于新西蘭籍邏輯學(xué)家亞瑟·普萊爾(Arthur N.Prior)[2]。Torben Braüner在其專著HybridLogicanditsProof-Theory中對(duì)經(jīng)典模態(tài)邏輯的混合化的工作進(jìn)行了系統(tǒng)的研究[3]。把多模態(tài)邏輯完全性和混合邏輯完全性證明合并起來(lái)可以證明多模態(tài)混合系統(tǒng)的完全性，但是還沒(méi)有相關(guān)文獻(xiàn)給出詳細(xì)的證明，本文將給出。

一、多模態(tài)語(yǔ)言

一個(gè)多模態(tài)命題語(yǔ)言(multimodal propositional language)定義為用原子模態(tài)參數(shù)(atomic modal parameters)的(固定的)集合Φ0擴(kuò)充的正規(guī)模態(tài)命題語(yǔ)言。這種語(yǔ)言除了包含在Var(變?cè)募?中的命題變?cè)?，符?hào)⊥和→之外，基本字母表還包括原子模態(tài)參數(shù)a,b,c,…。模態(tài)參數(shù)是用來(lái)標(biāo)示模態(tài)算子的，其中有兩個(gè)特殊的參數(shù)：空參數(shù)，記為0；同一參數(shù)，記為1。

Φ0上的模態(tài)參數(shù)類Φ定義為根據(jù)Φ0在如下運(yùn)算∪和⊙下封閉的集合：

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

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

由模態(tài)參數(shù)標(biāo)示的模態(tài)算子的類Ξ定義為：如果a∈Φ，那么[a]∈Ξ。

把Ξ的元素看作用組合代理人(agent)標(biāo)記的模態(tài)算子，這些代理人相互的態(tài)度由這些多模態(tài)算子控制，這樣可以給多模態(tài)語(yǔ)言一個(gè)直觀的解釋。例如，我們可以把多模態(tài)算子[a∪b]解釋為由代理人a和b分享的“知道”“必然”或“義務(wù)”。類似地，[a⊙b]可以表示代理人a相對(duì)于(依賴于)b的“知道”“必然”或“義務(wù)”。當(dāng)然這些解釋不是唯一的。

多模態(tài)算子可以看作程序(process)的標(biāo)簽。于是，多模態(tài)系統(tǒng)是看作對(duì)串行程序(serial processes)(在a⊙b的情形)和并行程序(parallel processes)(在a∪b的情形)的邏輯的形式化，[1]被看作恒等程序(identity process)，[0]被看作程序中的終止條款(halting clause)。

多模態(tài)合式公式按照通常的方式定義，如果涉及到多模態(tài)算子，再加上如下條款：

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

對(duì)任何模態(tài)算子[a]，我們定義〈a〉如下：

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

用于定義多模態(tài)語(yǔ)義的關(guān)鍵思想是，關(guān)系Ra和每個(gè)模態(tài)參數(shù)a相關(guān)，使得模態(tài)公式[a]φ和〈a〉φ在模型M的世界w∈W中的可滿足性由如下兩個(gè)條件決定：

(1)M,w[a]φ 當(dāng)且僅當(dāng)對(duì)所有w′∈W，wRaw′蘊(yùn)涵M,w′φ。

(2)M,w〈a〉φ當(dāng)且僅當(dāng)存在w′∈W，wRaw′并且M,w′φ。

二、多模態(tài)邏輯的公理

基本的多模態(tài)系統(tǒng)是最小模態(tài)邏輯系統(tǒng)的多模態(tài)擴(kuò)充。由這個(gè)系統(tǒng)加上一系列的公理模式可以得到更復(fù)雜的多模態(tài)系統(tǒng)，如基底系統(tǒng)(basilar systems)、肯定系統(tǒng)(affirmative systems)、Catach-Sahlqvist系統(tǒng)(Catach-Sahlqvist systems)等等[1]213。本文主要給出標(biāo)準(zhǔn)的(Standard)正規(guī)的(Normal)多模態(tài)邏輯，它就是最小模態(tài)系統(tǒng)的多模態(tài)版本。

定義2.1 所有基于模態(tài)參數(shù)的集族(collection)Φ的多模態(tài)系統(tǒng)SΦ，是包含所有PC(經(jīng)典命題邏輯)重言式的(多)模態(tài)公式的集族，并且在經(jīng)典命題規(guī)則(MP)和(US)(代入規(guī)則)下封閉。

首先假定我們所說(shuō)的多模態(tài)系統(tǒng)都包含定義2.2中的公理，即正規(guī)的和標(biāo)準(zhǔn)的多模態(tài)系統(tǒng)。在不引起混淆的情況下可以把它僅僅記作S而不是SΦ。

定義2.2 令SΦ是一個(gè)多模態(tài)系統(tǒng)，那么SΦ被稱為：

(a)正規(guī)的，如果它對(duì)每個(gè)原子模態(tài)參數(shù)a∈Φ0，公式φ和ψ，滿足正規(guī)性公理(Normality Axiom)(K[a])：

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

和必然化規(guī)則(Necessitation Rule)(Nec[a])：

(b)標(biāo)準(zhǔn)的，如果它對(duì)每個(gè)a,b∈Φ和公式φ，滿足多模態(tài)算子的公理(Axioms for Multimodal Operators)：

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

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

對(duì)原子模態(tài)參數(shù)引進(jìn)的正規(guī)性公理和必然化規(guī)則，可以擴(kuò)展到所有模態(tài)算子，這就是下面的命題。

命題2.3 對(duì)每個(gè)多模態(tài)系統(tǒng)S和c∈Φ，下面條款成立：

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

證明：

(1) 根據(jù)對(duì)多模態(tài)算子的復(fù)雜性實(shí)施歸納。如果c是原子的，根據(jù)定義結(jié)果成立。如果c是a∪b，則

1.[a∪b](φ→ψ) [假設(shè)]

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

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

6.[a]φ→[a]ψ [4,歸納假設(shè)]

7.[b]φ→ [b]ψ [5,歸納假設(shè)]

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

如果c是a⊙b,證明類似。

命題2.4 多模態(tài)算子的公理(即定義2.2中的公理(MM1)-(MM4))等價(jià)于如下條款：

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

(4) 〈1〉φ≡φ

證明：直接根據(jù)多模態(tài)算子的公理和定義〈a〉φ=df﹁[a]﹁φ實(shí)施歸納。

標(biāo)準(zhǔn)正規(guī)多模態(tài)系統(tǒng)、基底系統(tǒng)、肯定系統(tǒng)、Catach-Sahlqvist系統(tǒng)的完全性采用極大一致集(MCS)方法已經(jīng)給出了證明[1]222-235。

三、@算子的引進(jìn)

本文給出的混合多模態(tài)邏輯是通過(guò)在正規(guī)多模態(tài)邏輯中增加被稱為名詞性詞(nominal)的第二類命題符號(hào)和滿足算子而得到的[4]。用w，v，u，t等表示狀態(tài)和名詞性詞的變?cè)~性詞用來(lái)命名狀態(tài)，這里用同樣的符號(hào)表示而不加區(qū)分。符號(hào)@w稱為滿足算子。如果φ是合式公式，@wφ也是合式公式。

現(xiàn)在考慮增加部分的語(yǔ)義。令M=(W,R,V)是一個(gè)模型，g是M上的一個(gè)指派，Den(w)是狀態(tài)符號(hào)w的指稱(即如果w是狀態(tài)變?cè)?，Den(w)是g(w)；如果w是名詞性詞，Den(w)是V(w))。于是：

M,g,v@wφ當(dāng)且僅當(dāng)M,g,Den(w)φ,即滿足算子@w讓我們跳到w的指稱，并在那里對(duì)φ的變?cè)x值。

我們通過(guò)在S中增加關(guān)于@的公理和規(guī)則，將會(huì)得到混合化的公理系統(tǒng)，記為H[@](S)。

下面給出@的公理和規(guī)則。首先引進(jìn)@w-必然化規(guī)則：

除了這個(gè)規(guī)則之外，下面還將引進(jìn)被稱為Name和Paste的規(guī)則。

下面引進(jìn)@的公理，共有3組。第一組：

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

Self-Dual @wφ?﹁@w﹁φ

其中，K是模態(tài)分配模式，因?yàn)槲覀冇蠤w-必然化規(guī)則，所以@w是正規(guī)模態(tài)算子。Self-Dual告訴我們@w是一個(gè)其轉(zhuǎn)換關(guān)系是一個(gè)函數(shù)的模態(tài)。Introduction告訴我們?nèi)绾我M(jìn)@算子轄域下的信息。我們根據(jù)Introduction和Self-Dual可得到消解(Elimination)模式：

第二組公理是標(biāo)記的模態(tài)理論(modal theory of labeling)(或者稱為狀態(tài)等式的模態(tài)理論(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的情形，事實(shí)上在c∈Φ時(shí)它們也成立，因此有需要證明的命題3.1。

命題3.1 當(dāng)c∈Φ時(shí)Back和Bridge公理成立。

證明：

(1)證明Back公理。根據(jù)多模態(tài)算子的復(fù)雜性實(shí)施歸納。當(dāng)c是原子時(shí)，所證成立。

當(dāng)c是a∪b時(shí)，則

1．〈a〉@wφ→@wφ [歸納假設(shè)]

2．〈b〉@wφ→@wφ [歸納假設(shè)]

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

當(dāng)c是a⊙b時(shí)，則

1．〈a〉@wφ→@wφ [歸納假設(shè)]

2．〈b〉@wφ→@wφ [歸納假設(shè)]

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公理。同樣用歸納法。當(dāng)c是原子時(shí)，所證成立。

當(dāng)c是a∪b時(shí)，則

當(dāng)c是a⊙b時(shí)，則

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]

由上面所證可知命題成立。

下面再引進(jìn)兩個(gè)規(guī)則：

在兩個(gè)規(guī)則中，v必須是不同于w的不在φ或θ中出現(xiàn)的狀態(tài)符號(hào)(當(dāng)然v和w可以用同一個(gè)名詞性詞代換)，c∈Φ0。

Paste規(guī)則在c∈Φ0時(shí)也成立，我們需要證明下面的命題。

命題3.2 當(dāng)c∈Φ時(shí)Paste規(guī)則也成立。

證明：根據(jù)多模態(tài)算子的復(fù)雜性實(shí)施歸納。當(dāng)c是原子時(shí)，所證成立。當(dāng)c=0，1時(shí)，所證顯然成立。

當(dāng)c是a∪b時(shí)，則

7．@w〈a〉φ→θ [5，歸納假設(shè)]

8．@w〈b〉φ→θ [6，歸納假設(shè)]

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

當(dāng)c是a⊙b時(shí)，則

6．@u〈b〉φ→(@w〈a〉u→θ) [5，歸納假設(shè)]

8．@w〈a〉〈b〉φ→θ [7，歸納假設(shè)]

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

由上面所證可知命題成立。

事實(shí)上，因?yàn)槟B(tài)詞至多有可數(shù)無(wú)窮多個(gè)，Back和Bridge公理和Paste規(guī)則中的條件c∈Φ0直接替換為c∈Φ也是成立的。命題3.1和3.2說(shuō)明，正規(guī)多模態(tài)混合系統(tǒng)的模態(tài)詞可以用原子參數(shù)標(biāo)示的模態(tài)詞表達(dá)出來(lái)，這有利于簡(jiǎn)化系統(tǒng)。至此我們得到公理系統(tǒng)H[@](S)。該系統(tǒng)可靠性易證，證明過(guò)程在此省略。

四、完全性證明

單模態(tài)詞的混合邏輯系統(tǒng)的完全性已由P.Blackburn,M.de Rijke和Y.Venema給出了證明[5]434-443，下面參照他們的工作對(duì)標(biāo)準(zhǔn)正規(guī)多模態(tài)系統(tǒng)的完全性給出證明。

定義4.1(典型模型) 對(duì)于可數(shù)多模態(tài)語(yǔ)言L，典型模型Mc是(Wc,Rc,Vc)。其中Wc是所有L-MCS(公式的極大一致集)；Rc是Wc上的二元關(guān)系，定義為：ΓRcΔ當(dāng)且僅當(dāng)對(duì)所有L-公式φ，[a]φ∈Γ蘊(yùn)涵φ∈Δ。Vc是賦值，定義為：Vc(α)={?！蔠c|α∈Γ}，其中α是一個(gè)命題符號(hào)或名詞性詞。

為便于證明下面的引理，稱一個(gè)MCS是被標(biāo)記的(labeled)當(dāng)且僅當(dāng)它包含一個(gè)狀態(tài)符號(hào)；如果一個(gè)狀態(tài)符號(hào)屬于一個(gè)MCS，我們稱它是那個(gè)MCS的標(biāo)記(label)。

引理4.2 令Γ是一個(gè)被標(biāo)記的MCS，并且對(duì)所有狀態(tài)符號(hào)w，令Δw是{φ|@wφ∈Γ}。于是，

1．對(duì)每個(gè)狀態(tài)符號(hào)w，Δw是包含w的被標(biāo)記的MCS。

2．對(duì)所有狀態(tài)符號(hào)w和v，@wφ∈Δv當(dāng)且僅當(dāng)@wφ∈Γ。

3．存在一個(gè)狀態(tài)符號(hào)w使得Γ=Δw。

4．對(duì)所有狀態(tài)符號(hào)w，Δw={φ|@wφ∈Δw}。

5．對(duì)所有狀態(tài)符號(hào)w和v，如果w∈Δv，那么Δv=Δw。

證明：

還需要證Δw是極大的。假定不是，那么存在一個(gè)公式χ使得χ和﹁χ都不在Δw中。但是這樣有@wχ和@w﹁χ都不屬于Γ，根據(jù)Γ的極大一致性，﹁@wχ和﹁@w﹁χ都屬于Γ。但這是不可能的，因?yàn)楦鶕?jù)Self-Dual有@w﹁χ屬于Γ，矛盾。所以Δw是極大的。

條款2。我們有@wφ∈Δv當(dāng)且僅當(dāng) @v@wφ∈Γ。根據(jù)Scope，@v@wφ∈Γ當(dāng)且僅當(dāng)@wφ∈Γ。

條款3。根據(jù)假定，Γ至少包含一個(gè)狀態(tài)符號(hào)；令它是w。如果能證明Γ=Δw，我們將得到所要的結(jié)果。假定φ∈Γ，因?yàn)閣∈Γ，根據(jù)Introduction，@wφ∈Γ，因此φ∈Δw。反過(guò)來(lái)，如果φ∈Δw，那么@wφ∈Γ。所以，因?yàn)閣∈Γ，根據(jù)Elimination我們有φ∈Γ。

條款4。使用Introduction和Elimination。

條款5。令Δv滿足w∈Δv，我們將證明Δv=Δw。因?yàn)閣∈Δv，我們有@vw∈Γ。根據(jù)Swap，也有@wv∈Γ。首先我們有Δv?Δw。因?yàn)?，如果φ∈Δv，那么@vφ∈Γ。又因?yàn)锧wv∈Γ，所以根據(jù)Nom得@wφ∈Γ，因此φ∈Δw。類似地可證明Δw?Δv。

引理4.4(擴(kuò)充的Lindenbaum引理) 令L和L+是可數(shù)多模態(tài)語(yǔ)言，L+是L用新名詞性詞的一個(gè)可數(shù)無(wú)窮多集合擴(kuò)充的結(jié)果。于是每個(gè)L-公式的一致集合可以擴(kuò)充為一個(gè)由一個(gè)名詞性詞標(biāo)記的粘貼的L+-MCS。

現(xiàn)在進(jìn)行粘貼。列舉L+的所有公式，定義Θ0為Θt，并假定已經(jīng)定義了Θm，其中m≥0。令φm+1是列舉中的第m+1個(gè)公式，定義Θm+1如下。如果Θm+1∪{φm+1}是不一致的，那么Θm+1=Θm。否則：

1．Θm+1=Θm∪{φm+1}，如果φm+1不是形如@w〈c〉φ的。這里w是一個(gè)狀態(tài)符號(hào)。

令Θ=∪n≥0Θn。顯然這個(gè)集合是由名詞性詞t標(biāo)記的并且是極大的和粘貼的。而且，它還是一致的，因?yàn)檫@個(gè)膨脹的唯一非-平凡的方面是由第2條定義的，而Paste規(guī)則保證了這一步是保持一致性的。

定義4.5(標(biāo)記的模型) 令Γ是一個(gè)由一個(gè)名詞性詞標(biāo)記的粘貼的MCS。對(duì)于所有狀態(tài)符號(hào)w，令Δw是{φ|@wφ∈Γ}，并定義W為{Δw|w是狀態(tài)符號(hào)}。于是我們定義由Γ生成的標(biāo)記的模型M為(W,R,V)，其中R和V是(典型關(guān)系)Rc和(典型賦值)Vc在W上的限制。

標(biāo)記的模型有我們需要的所有結(jié)構(gòu)。首先，根據(jù)引理4.2的條款3，?！蔠，根據(jù)條款5，V是一個(gè)賦值，g是一個(gè)指派。還需要保證這樣的模型關(guān)于模態(tài)是定義明確的，即我們需要存在引理。

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

引理4.7(真值引理) 令Θ是M中的被標(biāo)記的MCS。對(duì)于所有公式φ，φ∈Θ當(dāng)且僅當(dāng)M, Θφ。

證明：根據(jù)歸納，原子的、布爾的和模態(tài)的步驟是標(biāo)準(zhǔn)的，略。我們需要證明關(guān)于滿足算子@的情形。證明如下：M,Θ@wψ當(dāng)且僅當(dāng)M,Δwψ(根據(jù)引理4.2的條款5，Δw是唯一包含w的MCS，而且，根據(jù)本引理的原子情形，它是M中w在其中為真的唯一狀態(tài))，當(dāng)且僅當(dāng)ψ∈Δw(歸納假設(shè))，當(dāng)且僅當(dāng)@wψ∈Δw(根據(jù)w∈Δw的事實(shí)，并且對(duì)從左到右的方向使用Introduction，對(duì)從右到左的方向使用Elimination)，當(dāng)且僅當(dāng)@wψ∈Θ(根據(jù)引理4.2的條款2)。這最后一步是證明完全性的關(guān)鍵！于是所有情形都已經(jīng)被證明了，根據(jù)歸納，真值引理成立。

定理4.8(完全性) 可數(shù)多模態(tài)語(yǔ)言L中公式的每個(gè)H[@](S)-(極大)一致集合在可數(shù)標(biāo)準(zhǔn)模型中關(guān)于標(biāo)準(zhǔn)指派函數(shù)是可滿足的。

證明：給定公式的H[@](S)-(極大)一致集合∑，使用擴(kuò)充的Lindenbaum引理把它擴(kuò)充為由可數(shù)語(yǔ)言L+的某名詞性詞標(biāo)記的粘貼的集合∑+。令M=(W,R,V)是由∑+生成的標(biāo)記的模型。根據(jù)引理4.2條款3，∑+∈W。根據(jù)真值引理，M,∑+∑+,進(jìn)而有M,∑+∑。因?yàn)镸中的每個(gè)狀態(tài)是由L+的某名詞性詞標(biāo)記的，并且名詞性詞只有可數(shù)多個(gè)，所以模型M是可數(shù)的。

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

[2] 霍書全.普萊爾混合時(shí)態(tài)邏輯的思想基礎(chǔ)[J].邏輯學(xué)研究，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.