何鍵楓 王軼

1 引言

認(rèn)知邏輯（[7,10,11]）及其簡(jiǎn)單動(dòng)態(tài)擴(kuò)充——公開(kāi)宣告邏輯（[6,12]）在過(guò)去數(shù)十年間得到了廣泛關(guān)注。上述框架可以模擬主體在公開(kāi)宣告前后知識(shí)或信念的變化。現(xiàn)實(shí)生活中的人們?cè)谥贫ㄓ?jì)劃、計(jì)算得失并作出決定之前，往往會(huì)考慮盡量多的情形，將其中不可能的情形加以排除則是常見(jiàn)的獲取知識(shí)或信念的做法?；谡J(rèn)知邏輯考察知識(shí)、信念與宣告時(shí)，也不可避免地運(yùn)用到可能情形（在不同場(chǎng)合中也常被稱為狀態(tài)、可能性或可能世界等）這一概念。本文嘗試在公開(kāi)宣告邏輯的框架下突出對(duì)可能情形的刻畫，允許在語(yǔ)言中直接訴說(shuō)可能情形，由此得到一種混合邏輯（[1,3,5,13]）。

混合公開(kāi)宣告邏輯并不是公開(kāi)宣告邏輯和混合邏輯的簡(jiǎn)單結(jié)合，這方面的研究也不是堆砌式的技術(shù)工作。公開(kāi)宣告邏輯的語(yǔ)義通過(guò)刪除可能情形來(lái)實(shí)現(xiàn)對(duì)知識(shí)更新的模擬，而這在語(yǔ)言中包含了用于表示可能情形的常元（在混合邏輯中稱為專名）之后就出現(xiàn)了問(wèn)題。例如在公開(kāi)宣告邏輯中，公式[φ]i（“公式φ被公開(kāi)宣告之后，i是現(xiàn)實(shí)情形”）中的算子[φ]（“φ被公開(kāi)宣告”）被解釋為在模型中刪除一切非φ的可能情形，其中或許已包括情形i，這將導(dǎo)致專名i在更新后的模型中失去定義。通過(guò)允許專名指稱空集，[9]在技術(shù)上回避了上述問(wèn)題。然而這樣的處理方法允許專名沒(méi)有指稱，并不合理，至少會(huì)令“專名”這一稱呼不再貼切。更有甚者，采用[9]中的定義將允許公式@i(φ ∨?φ)（“在情形i中，φ或者非φ”）為假。

本文堅(jiān)持按照經(jīng)典混合邏輯的做法將每個(gè)專名都解釋為單一的可能情形，并采用[8,第5.2.1 節(jié)]中提出的“刪鏈”語(yǔ)義學(xué)，將[φ]解釋為刪除全部指向非φ情形的鏈接（但不在模型中刪除那些情形）。這樣既實(shí)現(xiàn)對(duì)不可能情形的排除，又保證了專名都有指稱。然而缺點(diǎn)是，由鏈接所表示的二元關(guān)系將不必具有自反性與持續(xù)性。因此這一做法對(duì)知識(shí)模型S5 和信念模型KD45 并不適用。本文采用信念邏輯K45，并在此基礎(chǔ)上探討公開(kāi)宣告邏輯的混合化。

混合公開(kāi)宣告邏輯可以表達(dá)直接公開(kāi)宣告之外的行動(dòng)。有時(shí)需要表達(dá)在某一情形下作出了宣告（但在其他情形中可能并未作出），本文稱之為間接公開(kāi)宣告。公式[φ]xψ讀作“當(dāng)φ在情形x中被宣告后，ψ（在現(xiàn)實(shí)情形中）為真”。這樣的語(yǔ)言在技術(shù)上也有優(yōu)勢(shì)，具體見(jiàn)第5.2–5.3 節(jié)。

文章結(jié)構(gòu)如下：第2 節(jié)介紹基于信念模型的混合邏輯。第3 節(jié)對(duì)本文將探討的邏輯進(jìn)行梳理。第4 節(jié)中考察允許進(jìn)行假宣告的混合公開(kāi)宣告邏輯，而在第5節(jié)中則僅允許真宣告。第5.1–5.3 節(jié)探討語(yǔ)言中帶算子↓的擴(kuò)充，在第5.4 節(jié)則轉(zhuǎn)向不帶該算子的邏輯。第6 節(jié)將對(duì)全文進(jìn)行總結(jié)。

2 背景：基于信念模型的混合邏輯

信念模型是滿足如下條件的三元組(W,R,V)：（1）W為非空的可能情形集；（2）R為每個(gè)主體賦予W上的一個(gè)具有傳遞性和歐性的二元關(guān)系；（3）賦值函數(shù)V為每個(gè)命題賦予一集可能情形。如此定義的信念模型也稱為K45模型，它不一定滿足持續(xù)性（要求滿足持續(xù)性的信念模型通常稱為KD45 模型）。

混合邏輯通過(guò)在模態(tài)語(yǔ)言中增加專名（用于表達(dá)可能情形的常元）以及其他混合算子（如@和↓等）擴(kuò)充而成。其中只添加專名的混合語(yǔ)言以H表示。在H的基礎(chǔ)上繼續(xù)添加的其他算子在括號(hào)內(nèi)標(biāo)注，例如H(@)、H(↓)和H(@,↓)等都是混合語(yǔ)言。本文只關(guān)注H(@)和H(@,↓)這兩個(gè)常用混合語(yǔ)言：前者在標(biāo)準(zhǔn)語(yǔ)義下能得到一個(gè)理想的、可判定的混合邏輯；后者得到的邏輯雖然不可判定，卻擁有接近一階邏輯的表達(dá)能力。

本文預(yù)設(shè)一個(gè)非空的有窮主體集Ag，以及可數(shù)無(wú)窮的命題變?cè)疨r、專名集Nom 和變名集Var。語(yǔ)言H(@)和H(@,↓)由以下語(yǔ)法給出（其中p ∈Pr，a ∈Ag，i ∈Nom 且s ∈Var）：

專名i和變名s都是公式，分別為指稱可能情形的常元和變?cè)iφ和@sφ分別表示在i和s所指稱的情形中φ成立，而↓sφ表示將現(xiàn)實(shí)情形命名為s時(shí)φ成立。Baφ表示主體a相信φ。Ba的對(duì)偶算子記為，即代表?Ba?φ。命題聯(lián)結(jié)詞→、∨和?等采用通常方式定義。

混合的信念模型（簡(jiǎn)稱為模型）通過(guò)修改信念模型得到，使得每個(gè)專名都指稱模型里的一個(gè)可能情形。準(zhǔn)確地說(shuō)，在模型(W,R,V)中，賦值函數(shù)V的定義域?yàn)镻r∪Nom，值域?yàn)?(W)∪W，滿足將命題變?cè)加成錇橐患赡芮樾危╓的某個(gè)子集），并且將專名都映射為一個(gè)可能情形（W的某個(gè)元素）。結(jié)合指派g:Var→W以及現(xiàn)實(shí)情形w ∈W，可以得到所謂的點(diǎn)模型，并根據(jù)以下遞歸定義計(jì)算任意公式的真值（其中除=w外與g相同；其他經(jīng)典信念邏輯公式如常定義，可參考[6]）：

有效式與邏輯后承等概念類似于經(jīng)典模態(tài)邏輯加以定義。當(dāng)語(yǔ)言中不含算子↓時(shí)則無(wú)需考慮指派g。

語(yǔ)言H(@)和H(@,↓)采用上述語(yǔ)義解釋得到的邏輯分別記為H@和H@↓。圖1 中給出了邏輯H@和H@↓可靠且強(qiáng)完全的公理系統(tǒng)K45@和K45@↓。兩個(gè)系統(tǒng)的可靠性和完全性證明不妨參考[1]。

3 概覽

在公開(kāi)宣告邏輯中，宣告公式φ（被宣告的公式必須在現(xiàn)實(shí)情形中為真）意味著排除所有φ不為真的可能情形。盡管宣告可以反復(fù)進(jìn)行，宣告的內(nèi)容也可以不斷變化，僅僅通過(guò)宣告卻依然無(wú)法保證在最后消除所有不確定性以找出真實(shí)情形，更不用說(shuō)找出宣告是在哪個(gè)情形中作出的。1信念模型中的可能情形對(duì)所有公式的真假都可斷言，任意公式在其中或?yàn)檎妗⒒驗(yàn)榧?，而日常語(yǔ)言中的情形則常常代表了一類“可能情形”?！扒樾巍币辉~在兩者之間有所出入。使用足以刻畫可能情形的語(yǔ)言是本文在公開(kāi)宣告邏輯中引入專名的一個(gè)主要?jiǎng)訖C(jī)。

圖1:公理系統(tǒng)K45@與K45@↓

引言中已經(jīng)解釋過(guò)，在混合語(yǔ)言下解釋公開(kāi)宣告時(shí)，排除不可能情形可以像[9]那樣處理為將不可能情形直接刪除，但這會(huì)引發(fā)較多問(wèn)題。本文采用公開(kāi)宣告的“刪鏈”語(yǔ)義學(xué)（[8]），將其適當(dāng)修改后用于混合公開(kāi)宣告邏輯。這種處理方式不會(huì)導(dǎo)致可能情形被刪除后專名失去指稱，而且還使得對(duì)宣告假公式的解釋成為可能。文章將探討如下的兩種語(yǔ)義設(shè)定：（1）作出的宣告可真也可假（宣告可假），（2）作出的宣告必須為真（宣告須真）。

本文將混合語(yǔ)言H(@)和H(@,↓)擴(kuò)充以直接宣告算子和（或）間接宣告算子。直接宣告算子即經(jīng)典公開(kāi)宣告邏輯中的宣告算子；間接宣告算子以[φ]x（x為專名或變名）表示，讀作“當(dāng)φ在x所指稱的情形下被公開(kāi)宣告后，ψ在現(xiàn)實(shí)情形中為真”。簡(jiǎn)言之，間接宣告允許在某個(gè)可能情形中進(jìn)行，而不像直接宣告那樣僅限于在現(xiàn)實(shí)情形中進(jìn)行。由此帶來(lái)了三個(gè)混合宣告語(yǔ)言，H([],@)、H([],@,↓)和H([]x,@,↓)（本文不考慮語(yǔ)言H([]x,@)以免陷入太多組合）；考慮到行文的簡(jiǎn)潔，分別將它們簡(jiǎn)記為L(zhǎng)1、L2和L3。這三個(gè)語(yǔ)言和上一段提到的兩種語(yǔ)義設(shè)定將帶來(lái)五個(gè)邏輯（本文不考慮語(yǔ)言L3配以宣告可假的語(yǔ)義，L3將主要用于輔助其他邏輯所涉及的證明，參見(jiàn)第5.2–5.3 節(jié)）。

文章將對(duì)比五個(gè)邏輯和兩個(gè)基本混合語(yǔ)言的表達(dá)能力，并給出五個(gè)邏輯的可靠且完全的公理系統(tǒng)，為方便查找，將相關(guān)語(yǔ)言、語(yǔ)義設(shè)定以及對(duì)應(yīng)的邏輯及其公理系統(tǒng)整理匯總至表1。

接下來(lái)第4 節(jié)首先探討宣告可假的兩個(gè)邏輯L1u 和L2u，然后到第5 節(jié)再采用宣告須真的語(yǔ)義設(shè)定。

表1:邏輯與公理系統(tǒng)的記法

4 宣告可假的邏輯

本節(jié)將會(huì)探討在宣告可以為假的語(yǔ)義設(shè)定下的兩個(gè)混合公開(kāi)宣告邏輯L1u 和L2u，并給出它們的公理系統(tǒng)L1u 和L2u。這兩個(gè)系統(tǒng)通過(guò)歸約方法分別由第2節(jié)中介紹的混合信念邏輯的公理系統(tǒng)K45@和K45@↓得到。

4.1 邏輯L1u

在混合語(yǔ)言H(@)中增加經(jīng)典公開(kāi)宣告算子，由此得到的語(yǔ)言H([],@)簡(jiǎn)記為L(zhǎng)1。

定義1(語(yǔ)言L1).L1公式由以下規(guī)則遞歸定義：

其中a ∈Ag，p ∈Pr 且i ∈Nom。命題聯(lián)結(jié)詞如常定義，與?φ?分別為Ba與[φ]的對(duì)偶算子。

宣告可假意味著公式φ被宣告無(wú)需先決條件，具體語(yǔ)義定義如下。

定義2(L1u 語(yǔ)義).任給模型M=(W,R,V)和可能情形w ∈W，原子公式、布爾公式和認(rèn)知公式的語(yǔ)義解釋如常定義（不妨參見(jiàn)[6]），混合公式的語(yǔ)義解釋參見(jiàn)第2 節(jié)。形如[φ]ψ的公式的語(yǔ)義解釋如下：

其中更新模型Mφ=(W,RM,φ,V)滿足任給主體a，

即Mφ是將M中所有指向φ為假的情形的鏈接刪除后得到的模型。

需要注意的是，即使M是持續(xù)模型，更新模型Mφ也可能不再具有持續(xù)性。這是本文不要求模型具有持續(xù)性的技術(shù)性原因。不難驗(yàn)證Mφ依然滿足傳遞性和歐性。以歐性為例。如果成立而不成立，則有M,tφ。此時(shí)可得不成立，矛盾。上述更新方式保持傳遞性和歐性，因此適用于基于信念模型K45 的混合模型。

由所有有效公式（即在所有模型的所有可能情形下都為真的公式）組成的集合視為語(yǔ)言L1在上述語(yǔ)義下的邏輯，記為L(zhǎng)1u。下面給出L1u 的一些有效式，證明較為簡(jiǎn)單，故略去。以這些有效式作為歸約原則，可以將所有L1公式轉(zhuǎn)化為與之等值的不含宣告算子的公式（即轉(zhuǎn)化為等值的H(@)公式）。

命題3.任給L1公式φ、ψ和χ，命題變?cè)猵，主體a和專名i，如下公式都是L1u的有效式：

將上述命題中的有效式作為歸約公理添加到邏輯H@ 的公理系統(tǒng)K45@ 中就可以得到L1u 的公理系統(tǒng)L1u，如圖2 所示。

圖2:公理系統(tǒng)L1u

定理4(L1u 可靠性).L1u 是可靠的，即如果?L1uφ則有|=L1uφ。

由K45@的可靠性和命題3 不難得到上述可靠性定理。反過(guò)來(lái)，要證明L1u的完全性，需要證明公式集Φ 的所有語(yǔ)義后承φ都可在L1u 中以Φ 為前提推演得到。任給L1公式φ，存在H(@)公式φ′滿足?L1uφ ?φ′。由L1u 的可靠性得知，φ′同樣是Φ 的語(yǔ)義后承。由K45@的完全性可知Φ?K45@φ′。由于L1u 是K45@的擴(kuò)充，Φ?L1uφ′，再通過(guò)分離規(guī)則即可推演出φ。因此，L1u 完全性證明的核心任務(wù)是找到L1公式的H(@)翻譯，而這恰恰是歸約公理的用途。

定義5(L1到H(@)的翻譯).遞歸定義t:L1→H(@)如下：

為了證明?L1uφ ?t(φ)，定義復(fù)雜度函數(shù)c:L1→N 如下：

引理6.任給L1公式φ、ψ和χ，命題變?cè)猵，主體a和專名i，

引理7.任給L1公式φ，都有?L1uφ ?t(φ)。

定理8(L1u 完全性). 對(duì)任意L1公式集Φ 和公式φ，如果。證明.假設(shè)。以t(Φ)表示{t(ψ)|ψ ∈Φ}，則；因?yàn)榉駝t存在Φ 的有窮子集Ψ 滿足，此時(shí)根據(jù)引理7 可得，矛盾。由K45@ 的完全性可得。故有模型M及其中的可能情形w使得對(duì)于任意t(ψ)∈t(Φ)均有M,且。由于定義5中翻譯t是保真的（根據(jù)引理7 以及L1u 的可靠性），對(duì)于任意公式ψ ∈Φ 均有M,，即。

4.2 邏輯L2u

在混合語(yǔ)言H(@,↓)中添加經(jīng)典宣告算子，所得語(yǔ)言H([],@)簡(jiǎn)記為L(zhǎng)2。

定義9(語(yǔ)言L2).L2公式由以下規(guī)則遞歸定義：

其中a ∈Ag，p ∈Pr，i ∈Nom 且s ∈Var。相關(guān)約定與定義1 中相似。

L2在宣告可假的語(yǔ)義設(shè)定下所得邏輯記為L(zhǎng)2u。

定義10(L2u 語(yǔ)義).任給模型M=(W,R,V)、指派g和可能情形w ∈W，原子公式、布爾公式和認(rèn)知公式的語(yǔ)義解釋如常定義，混合公式的語(yǔ)義解釋與前文相同。形如[φ]ψ的公式的語(yǔ)義解釋如下：

其中更新模型Mg,φ=(W,RM,g,φ,V)使得對(duì)任意主體a，

語(yǔ)言L2中含有變名，對(duì)其處理類似于一階邏輯中的變?cè)阕觿t類似于量詞，由此可以定義公式中變名的自由出現(xiàn)。將公式φ中的所有自由變名的集合記為Free(φ)。

下面的命題說(shuō)明了公式[φ]↓sψ ?↓s[φ]ψ（其中s/∈Free(φ)）是關(guān)于宣告和↓算子的有效歸約原則。

命題11.任給L2公式φ和ψ，以及變名s/∈Free(φ)，公式[φ]↓sψ ?↓s[φ]ψ是有效的。

證明.任給模型M、指派g和可能情形w使得。由語(yǔ)義定義可得。假設(shè)，則，因此。由于，不難驗(yàn)證故，矛盾。相反方向可類似證得。

由此可以得到圖3 所示的公理系統(tǒng)L2u。可以采用與證明L1u 完全性類似的

圖3:公理系統(tǒng)L2u

方法將L2u 歸約為K45@↓，從而得到系統(tǒng)的完全性。在使用公理“公開(kāi)宣告與↓”進(jìn)行歸約時(shí)需要考慮邊際條件。如果變名s在公式φ中自由出現(xiàn)，則可能需要首先將約束變名s易字以實(shí)現(xiàn)歸約；采用類似于一階邏輯中的前束范式方法可以解決這個(gè)問(wèn)題。相關(guān)細(xì)節(jié)此處從略。

5 宣告須真的邏輯

本節(jié)探討在宣告必須為真的語(yǔ)義設(shè)定下的混合公開(kāi)宣告邏輯。語(yǔ)言L1和L2在該語(yǔ)義設(shè)定下的邏輯分別記為L(zhǎng)1t 和L2t。形如[φ]@aψ的公式無(wú)法找到將宣告消去的歸約原則，使得尋找公理系統(tǒng)的難度增加。

將專名引入語(yǔ)言后，很自然地會(huì)考慮到間接宣告這一概念。公式[φ]xψ讀作“當(dāng)φ在x所指稱的情形下被宣告后，ψ（在現(xiàn)實(shí)情形中）為真”。將L2中經(jīng)典宣告算子（稱為直接宣告算子）替換為間接宣告算子[φ]x后得到的語(yǔ)言即L3，該語(yǔ)言下的邏輯記為L(zhǎng)3t。邏輯L3t 可以帶來(lái)技術(shù)上的便利。文章將證明邏輯L2t 和L3t 具有相同的表達(dá)能力。通過(guò)找到后者的可靠且完全的公理系統(tǒng)，就可以得到前者的對(duì)應(yīng)結(jié)果。

本節(jié)最后第5.4 節(jié)中將討論技術(shù)上更復(fù)雜的邏輯L1t。

5.1 邏輯L2t

下面給出語(yǔ)言L2（見(jiàn)定義9）在宣告須真設(shè)定下的語(yǔ)義定義。

定義12(L2t 語(yǔ)義).任給模型M=(W,R,V)、指派g和可能情形w ∈W，公式[φ]ψ的語(yǔ)義解釋如下：

其中Mg,φ=(W,RM,g,φ,V)與定義10 中相同，其他類型公式的語(yǔ)義解釋也與定義10 相同。

由此得到的邏輯記為L(zhǎng)2t。公式φ中所有自由變名的集合仍然記為Free(φ)。以下結(jié)果值得討論。

命題13.|=L2t@iBa?φ →[φ]@iBaψ

上述命題中的有效式可以讀作“如果主體在某種情況下相信非φ，則當(dāng)φ在該情形中被宣告后，主體將相信一切”。在L2t 語(yǔ)義中，假設(shè)φ在主體相信其為假的情況實(shí)際上是真的，則φ被宣告后將導(dǎo)致主體產(chǎn)生沖突信念，從而令主體相信一切。

命題14.任給φ,ψ ∈L2，x ∈Nom ∪Var和s ∈Var使得s/∈Free(φ)，如下結(jié)論成立：

根據(jù)上述結(jié)果，倘若公式[φ]↓sψ中不含@算子且s/∈Free(φ)，則該公式可歸約為不含宣告算子的公式。不過(guò)由于宣告與@的歸約原則的缺失，不足以形成L2t 邏輯的完整歸約原則。因此難以通過(guò)歸約的方法得到L2t 邏輯的公理系統(tǒng)。為解決這一問(wèn)題，下面首先引入邏輯L3t 并在第5.3 節(jié)重新探討L2t 的公理化。

5.2 邏輯L3t

盡管未能為宣告和@找到歸約原則，這卻并不意味著L2t 的表達(dá)能力嚴(yán)格強(qiáng)于H@↓。本節(jié)使用間接宣告算子替換直接宣告算子，并考察兩者之間的關(guān)系，最后給出混合間接公開(kāi)宣告邏輯的公理系統(tǒng)。

將語(yǔ)言L2中的直接宣告算子替換為間接宣告算子，得到的語(yǔ)言記為L(zhǎng)3。其準(zhǔn)確定義如下：

定義15(語(yǔ)言L3).L3公式由以下規(guī)則給出：

其中a ∈Ag，p ∈Pr，i ∈Nom 且s ∈Var。語(yǔ)言中的約定如前。

當(dāng)考慮L3公式中變名的自由或約束時(shí)，[φ]s算子不構(gòu)成對(duì)s的約束。公式φ中自由變名的集合仍然記為Free(φ)。

語(yǔ)言L3在宣告須真設(shè)定下的語(yǔ)義定義如下：

定義16(L3t 語(yǔ)義).任給模型M=(W,R,V)、指派g和可能情形w ∈W，只需要補(bǔ)充形如[φ]iψ和[φ]sψ公式的語(yǔ)義解釋（其他同定義12）：

其中Mg,φ=(W,RM,g,φ,V)與定義10 中相同。由此得到的邏輯記為L(zhǎng)3t。

命題17.令x為一專名或變名，且變名s/∈Free(φ′)∪Free(ψ′)∪{x}。如果L2公式φ和ψ分別與L3公式φ′和ψ′邏輯等值，則：

1.[φ]ψ與↓s[φ′]sψ′邏輯等值；

2.[φ′]xψ′與↓s@x[φ]@sψ邏輯等值。

由上述命題很容易得到如下推論。

推論18.L2t 與L3t 具有相同表達(dá)能力。即，

1.任給L2公式φ，存在L3公式φ′使得對(duì)所有模型M、指派g和可能情形w，M,g,w |=L2tφ當(dāng)且僅當(dāng)M,g,w |=L3tφ′；

2.任給L3公式φ，存在L2公式φ′使得對(duì)所有模型M、指派g和可能情形w，M,g,w |=L3tφ當(dāng)且僅當(dāng)M,g,w |=L2tφ′。

邏輯L3t 中可以得到完整的歸約原則。

命題19.任給L3公式φ、ψ和θ，主體a，命題變?cè)猵和x,y ∈Nom ∪Var。令且s/∈Free(φ)。則如下公式都是L3t 的有效式：

下面給出L3t 的其他一些有效式，有助于更好地理解該邏輯。

命題20.任給L3公式φ，主體a，專名或變名x和y。則，

對(duì)于第一條有效式，宣告真實(shí)情形將所有其他（虛假）情形全都排除，這樣的宣告起到的效果是真實(shí)信息全都被相信。至于第二條有效式，首先，@x的跳轉(zhuǎn)使得間接宣告算子[@xφ]y中的y不起作用；其次，@xφ如果在某個(gè)可能情形下為真，則在所有可能情形下都為真，在宣告須真語(yǔ)義設(shè)定下不會(huì)引起模型更新。

將命題19 中的歸約原則添加至H@↓的公理系統(tǒng)K45@↓（圖1），就得到了L3t 的公理系統(tǒng)L3t，如圖4 所示。

圖4:公理系統(tǒng)L3t（其中sx 且sFree(φ)）

命題21(L3t 可靠性).L3t 是可靠的，即由?L3tφ可得|=L3tφ。

證明公理系統(tǒng)L3t 完全性的途徑是將其歸約為已知可靠且完全的系統(tǒng)K45@↓。具體方法類似于第4.1 和4.2 節(jié)的完全性證明。下面列出關(guān)鍵的定義與引理，但省略具體細(xì)節(jié)。

定義22(L3到H(@,↓)的翻譯).定義t:L3→H(@,↓)如下（其中a ∈Ag，p ∈Pr，x ∈Nom∪Var 且s ∈Var 使得且Free(φ)）：

定義23.復(fù)雜度函數(shù)c:L3→N 遞歸定義如下：

引理24.任給L3公式φ、ψ和θ，命題變?cè)猵，主體a，專名或變名x和y以及變名s使得且s/∈Free(φ)。則，

引理25.對(duì)任意L3公式φ，均有?L3tφ ?t(φ)。

定理26(L3t 完全性).任給L3公式集Φ 和公式φ，如果Φ|=L3tφ，則有Φ?L3tφ。

5.3 邏輯L2t 的公理系統(tǒng)

在上節(jié)給出L3t 的公理系統(tǒng)后，本節(jié)重新探討邏輯L2t 的公理系統(tǒng)。思路是利用命題17 將公理系統(tǒng)L3t 使用語(yǔ)言L2加以改寫。

定義27.翻譯τ:L2→L3定義如下（其中s為不出現(xiàn)于[φ]ψ中的某個(gè)變名）：

任給L2公式φ，τ(φ)是它在語(yǔ)言L3中的改寫。類似地可以定義從L3到L2的改寫函數(shù)ρ。然而，ρ必須被小心處理。簡(jiǎn)單地說(shuō)，任給某個(gè)L3公式，其所有形如[φ]xψ的子公式都必須被替換為↓t@x[φ]@tψ，其中t是未在該公式內(nèi)自由出現(xiàn)的新變名。下面給出具體定義。

定義28.翻譯ρ:L3→L2定義如下：

其中s是不在[φ]xψ中出現(xiàn)的某個(gè)變名，t是新的變名。

需要注意的是，上面定義的ρ翻譯實(shí)際使用過(guò)程中最好從極小子公式開(kāi)始逐步進(jìn)行改寫，而不是從公式最外層開(kāi)始，否則機(jī)械地來(lái)講可能會(huì)出現(xiàn)違背t是新變名要求的情況。

命題29.任給L2公式φ,|=L2tφ ?ρ(τ(φ))。

使用改寫規(guī)則可以將公理系統(tǒng)L3t 轉(zhuǎn)化為L(zhǎng)2t 的公理系統(tǒng)L2t（圖5）。

圖5:公理系統(tǒng)L2t

L2t 的可靠性與強(qiáng)完全性可以通過(guò)改寫技巧證得。這里省略具體細(xì)節(jié)，僅通過(guò)圖6 說(shuō)明證明的過(guò)程（注意需要從左上方經(jīng)過(guò)下方迂回到達(dá)右上方）。

5.4 邏輯L1t

圖6:L2t 完全性證明流程圖

最后回到語(yǔ)言L1，在宣告須真的語(yǔ)義設(shè)定下加以考察，具體語(yǔ)義定義同定義12，由此得到的邏輯記為L(zhǎng)1t。第4 節(jié)已經(jīng)證明了邏輯L1u 與邏輯H@具有相同的表達(dá)能力，然而那是在宣告可假的語(yǔ)義設(shè)定下。要求宣告須真時(shí)，未能為宣告與@算子找到歸約原則。至于L1u 的表達(dá)能力是否嚴(yán)格強(qiáng)于H@也尚未明朗。本節(jié)將致力于給出一個(gè)可靠且完全的公理系統(tǒng)。

下面是L1t 的一些有效式，他們的相似版本此前在其他邏輯中已有討論（參見(jiàn)命題13 和20）。

命題30.如下L1公式都是L1t 的有效式：

L1t 的公理系統(tǒng)L1t 可在公理系統(tǒng)K45@的基礎(chǔ)上增加額外公理和規(guī)則得到。為使行文簡(jiǎn)介，將縮寫為，并將縮寫為。L1t 的額外公理與規(guī)則列舉如下：

上述公理系統(tǒng)中的某些公理可以使用更簡(jiǎn)單的公理替代。例如Agree′可以換成Agree（圖1），通過(guò)Agree、NA、K[]、N@和K@可以推出Agree′。

L1t 的可靠性不難驗(yàn)證。L1t 的強(qiáng)完全性可以通過(guò)修改K45@的完全性證明以包含宣告算子的情形而加以證明。類似于將[4,第7.3 節(jié)]和[2]中的方法相疊加，具體證明過(guò)于枯燥和煩復(fù)，本文從略。

6 結(jié)語(yǔ)

本文探討了混合公開(kāi)宣告邏輯，這并不是公開(kāi)宣告邏輯和混合邏輯的簡(jiǎn)單拼湊。在此邏輯中可以選擇宣告須真和宣告可假兩種語(yǔ)義設(shè)定，且易于探討直接宣告和間接宣告這兩種行動(dòng)。文章采用了有別于文獻(xiàn)[9]中的處理方法，并相信這一做法更好地遵守了公開(kāi)宣告邏輯和混合邏輯各自的傳統(tǒng)。

文章討論了三個(gè)語(yǔ)言L1、L2和L3，其中L3源于引入間接宣告這一概念。依據(jù)是否允許進(jìn)行假宣告，文章選擇性地考察了五個(gè)邏輯，即L1u、L2u、L1t、L2t和L3t，分別給出它們的公理系統(tǒng)。此外，文中雖未準(zhǔn)確定義，但已經(jīng)在很大程度上對(duì)比了有關(guān)邏輯的表達(dá)能力。具體結(jié)果如下圖所示，其中：(1)三橫線（含實(shí)線和虛線）所連接的兩個(gè)邏輯表達(dá)能力相同；(2)箭頭（含實(shí)線箭頭和虛線箭頭）所指向的邏輯其表達(dá)能力強(qiáng)于箭頭出發(fā)處的邏輯；(3)實(shí)線所連接的兩個(gè)邏輯的表達(dá)能力對(duì)比由直接結(jié)論（主要是歸約原則）得到，而虛線表示作為推論得到；(4)標(biāo)有問(wèn)號(hào)的箭頭表示相應(yīng)的表達(dá)能力對(duì)比關(guān)系尚未得到證明，這些將留待未來(lái)加以完成。

細(xì)心的讀者已經(jīng)發(fā)現(xiàn)，本文僅選擇探討了五個(gè)混合公開(kāi)宣告邏輯（表1）。未加討論的有邏輯L3u、語(yǔ)言H([]x,@)及其在兩種語(yǔ)義設(shè)定下的邏輯，它們分別又有什么特點(diǎn)？本文并未選擇窮盡所有這些邏輯，探討邏輯L3t 主要是為了將其公理系統(tǒng)改寫為邏輯L2t 的公理系統(tǒng)。間接宣告算子[φ]x值得進(jìn)行更多的研究，我們已將其作為后續(xù)工作。

本文只考慮了個(gè)體信念，在此基礎(chǔ)上考察群體信念是值得在未來(lái)去嘗試的工作。文獻(xiàn)[9]中所采用的方法，即通過(guò)刪除可能情形來(lái)解釋宣告的做法可能更適合于模擬S5 知識(shí)。探討基于知識(shí)模型的混合動(dòng)態(tài)認(rèn)知邏輯將是后續(xù)任務(wù)之一。