混合公開宣告邏輯

何鍵楓 王軼

1 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

3 概覽

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

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

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

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

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

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

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

4 宣告可假的邏輯

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

4.1 邏輯L1u

在混合語言H(@)中增加經(jīng)典公開宣告算子，由此得到的語言H([],@)簡記為L1。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

引理6.任給L1公式φ、ψ和χ，命題變元p，主體a和專名i，

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

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

4.2 邏輯L2u

在混合語言H(@,↓)中添加經(jīng)典宣告算子，所得語言H([],@)簡記為L2。

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

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

L2在宣告可假的語義設(shè)定下所得邏輯記為L2u。

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

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

語言L2中含有變名，對其處理類似于一階邏輯中的變元，而↓算子則類似于量詞，由此可以定義公式中變名的自由出現(xiàn)。將公式φ中的所有自由變名的集合記為Free(φ)。

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

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

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

由此可以得到圖3 所示的公理系統(tǒng)L2u?？梢圆捎门c證明L1u 完全性類似的

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

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

5 宣告須真的邏輯

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

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

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

5.1 邏輯L2t

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

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

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

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

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

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

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

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

5.2 邏輯L3t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

將命題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)鍵的定義與引理，但省略具體細節(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公式φ、ψ和θ，命題變元p，主體a，專名或變名x和y以及變名s使得且s/∈Free(φ)。則，

引理25.對任意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 使用語言L2加以改寫。

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

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

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

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

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

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

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

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

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

5.4 邏輯L1t

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

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

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

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

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

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

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

6 結(jié)語

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

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

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

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