徐康

浙江水利水電學(xué)院 社科部xukanguuu@163.com

王軼?

浙江大學(xué) 哲學(xué)系、語言與認(rèn)知研究中心ynw@xixilogic.org

1 引言

公開宣告邏輯（[13]）在經(jīng)典認(rèn)知邏輯（[8,6,12]）的基礎(chǔ)上擴(kuò)充以表達(dá)公開宣告的算子，是最簡單的動(dòng)態(tài)認(rèn)知邏輯之一。任意公開宣告邏輯（[2]）在此基礎(chǔ)上添加任意公開宣告算子，從而允許使用諸如“在某個(gè)公開宣告后知道φ”的語句；這樣的語句可以簡單理解為“φ（通過宣告）可知”。群體宣告邏輯（[1]）則關(guān)注不同主體的宣告所帶來的動(dòng)態(tài)變化。公式〈G〉Kiφ表示“群體G中的主體可以同時(shí)做出某種公開宣告，以使得主體i知道φ”；這也是一種“φ可知”語句，只不過知識(shí)的獲取僅能經(jīng)由群體同時(shí)宣告實(shí)現(xiàn)。任意公開宣告邏輯并不能歸約為群體宣告邏輯；反過來，群體宣告邏輯是否可以歸約為任意公開宣告邏輯，則仍然是一個(gè)懸而未決的問題。

群體宣告邏輯的常用例子是諸如泥孩難題、俄羅斯卡牌問題（[5,第4.12節(jié)]）等需要對群體同時(shí)宣告前后情況變化進(jìn)行推理的問題。這些例子中宣告的內(nèi)容既可以是一階知識(shí)（即對事實(shí)的認(rèn)識(shí)），比如甲宣告自己知道頭上有泥巴；也可以是高階知識(shí)，比如甲宣告自己知道乙知道甲手上的卡牌。如果僅從解答問題的角度考慮，這些例子中允許宣告高階知識(shí)無可厚非，甚至從協(xié)議1俄羅斯卡牌問題中要求甲和乙進(jìn)行公開的信息傳遞并使丙無法獲知實(shí)際信息（甲和乙手上是哪些卡牌），其解答可被視為構(gòu)建一個(gè)信息傳遞協(xié)議。的安全性角度考慮，使用高階知識(shí)似乎更易被接受。

然而現(xiàn)實(shí)情況下很多時(shí)候并不接受宣告高階知識(shí)。例如，當(dāng)評審委員會(huì)審議到底錄用哪位應(yīng)聘者時(shí)，各位評委通常只能針對應(yīng)聘者的情況給出事實(shí)性的宣告，這樣的宣告常常體現(xiàn)在該評委說出“我認(rèn)為（或不認(rèn)為）這位候選人……”這樣的話；一位評委通常很少采用“我認(rèn)為另一位評委認(rèn)為（或不認(rèn)為）……”這樣的表述，否則這位評委的話容易給旁聽者以不客觀或有其它所指等印象。人類務(wù)實(shí)交流過程中通常追求簡單明確，而允許宣告高階知識(shí)的場合，很多時(shí)候與智力游戲或是特定領(lǐng)域的深入探索等有關(guān)。

基于上述考慮，本文引入群體簡單宣告邏輯。公式〈G〉Kiφ表示“群體G中的每個(gè)主體可以同時(shí)公開宣告某個(gè)一階知識(shí)，以使主體i知道φ”，亦即“φ通過群體一階知識(shí)宣告可知”。群體簡單宣告邏輯在很多地方與群體宣告邏輯相似，但也不盡然；最突出的差別有兩點(diǎn)。一是在群體宣告邏輯中，有窮規(guī)則R[G]不可靠，其已知的公理系統(tǒng)使用了基于容許型的無窮規(guī)則；而類似的有窮規(guī)則在群體簡單宣告邏輯中保持有效性，從而使其公理系統(tǒng)更美觀。二是公式〈G〉〈H〉φ→〈G∪H〉φ，可直觀解讀為“多群依次宣告可由一次宣告實(shí)現(xiàn)”；該公式在群體宣告邏輯中有效，但在群體簡單宣告邏輯中卻不是有效式。

本文將對群體簡單宣告邏輯的表達(dá)能力和公理系統(tǒng)進(jìn)行探討。首先對群體簡單宣告邏輯的有效式和歸約式進(jìn)行梳理。在表達(dá)能力方面，主要與公開宣告邏輯進(jìn)行對比。公理系統(tǒng)以及完全性定理的證明基本采用[2]中的方法，但在完全性證明中本文改為使用經(jīng)典的“理論”定義，從而適度簡化證明過程。順便一提，[4,3]宣稱提供了任意公開宣告邏輯完全性的更簡單證明方法，但簡化程度有待商榷。

論文結(jié)構(gòu)安排如下：第2節(jié)簡要介紹經(jīng)典認(rèn)知邏輯、公開宣告邏輯和群體宣告邏輯等基礎(chǔ)理論。第3節(jié)證明[2]中提出的有窮規(guī)則是不可靠的。第4節(jié)引入群體簡單宣告邏輯，之后的第5和第6兩節(jié)分別探討群體簡單宣告邏輯的表達(dá)能力和公理系統(tǒng)。第7節(jié)進(jìn)行總結(jié)。

2 背景

本節(jié)簡要介紹經(jīng)典認(rèn)知邏輯、公開宣告邏輯和群體宣告邏輯，這些內(nèi)容都是論文主體部分的所依賴的背景知識(shí)。

本文設(shè)定pr是可數(shù)非空的命題變元集，ag是一個(gè)有窮非空的主體集合，gr是所有群體的集合，即gr=?(ag)；在此設(shè)定下可考慮空群，記為?。

2.1 認(rèn)知邏輯（EL）和公開宣告邏輯（PAL）

在命題邏輯（簡稱PL）基礎(chǔ)上增加刻畫“知道”的模態(tài)算子可以得到經(jīng)典認(rèn)知邏輯（[8,6,12]，簡稱EL）。公開宣告邏輯（[13]，簡稱PAL）在經(jīng)典認(rèn)知邏輯基礎(chǔ)上進(jìn)一步增加對公開宣告的刻畫，是最簡單的動(dòng)態(tài)認(rèn)知邏輯之一。本節(jié)簡要介紹經(jīng)典認(rèn)知邏輯和公開宣告邏輯以方便后文的敘述，對這兩類邏輯的更詳細(xì)介紹參見[5]。

上述三個(gè)邏輯的語言由如下語法規(guī)則分別給出（其中p∈pr且i∈ag）：

Ki的對偶算子記為形式上將視為?Ki?φ的縮寫。類似地，[φ]的對偶算子為 〈φ〉，并且 〈φ〉ψ 視為 ?[φ]?ψ 的縮寫。

公式[φ]ψ可以直觀理解為“公開宣告φ之后，ψ成立”。而〈φ〉ψ可以理解為“并非在公開宣告φ之后，?ψ成立”，亦即“公開宣告φ，且此后ψ成立”。通常使用面向認(rèn)知解釋的可能世界模型來給出PAL的形式語義。三元組M=(W,～,V)稱為知識(shí)模型（簡稱模型、亦稱S5模型），如果滿足：

·W是非空集合，其中元素稱為可能世界、狀態(tài)或點(diǎn)；

對于所有s∈W，稱(M,s)為知識(shí)狀態(tài)；簡單起見，外層括號常被省略。PAL的形式語義給出如下。令p∈pr，i∈ag，(M,s)=((W,～,V),s)為知識(shí)狀態(tài)，滿足關(guān)系（符號|=PAL）由如下條件給出：

M,s|=PALp 當(dāng)且僅當(dāng) s∈V(p)

M,s|=PAL?φ 當(dāng)且僅當(dāng) 并非M,s|=PALφ

M,s|=PAL(φ∧ψ) 當(dāng)且僅當(dāng) M,s|=PALφ且M,s|=PALψ

M,s|=PALKiφ 當(dāng)且僅當(dāng) 對所有t，如果s～it，則M,t|=PALφ

M,s|=PAL[φ]ψ 當(dāng)且僅當(dāng) 如果M,s|=PALφ，則M|φ,s|=PALψ

其中M|φ=(W′,～′,V′)是M 的子模型，滿足：

·W′={s′∈ W|M,s′|=PALφ}；

·～′∶ag → ?(W′×W′)使得對任意

·V′(p)=V(p)∩ W′。

稱PAL公式φ（在PAL中）有效，當(dāng)且僅當(dāng)對所有知識(shí)狀態(tài)(M,s)，M,s|=PALφ。下列公式是PAL的有效式：

PAL與EL的表達(dá)能力相同。圖1中展示EL公理系統(tǒng)S5，以及在S5的基礎(chǔ)上增加歸約公理而得到的PAL公理系統(tǒng)PAL。（[13,9,10]）

圖1:公開宣告邏輯的公理系統(tǒng)PAL，其子系統(tǒng)S5由(PC),(K),(T),(5),(MP)和(N)組成。去掉宣告規(guī)則（RA）所得到的系統(tǒng)并不會(huì)丟失任何定理，但對于公開宣告邏輯的某些擴(kuò)張（例如帶公共知識(shí)的公開宣告邏輯）這條規(guī)則可能無法省略，因此為避免遺失，這里統(tǒng)一添加上。4公理（即Kiφ→KiKiφ，正自省公理）常常也被包含在上述系統(tǒng)中，但它可由S5推演得到。

2.2 群體宣告邏輯（GAL）

群體宣告邏輯（[1]，簡稱GAL）以公開宣告邏輯為基礎(chǔ)，關(guān)注公開宣告的群體行為。群體宣告邏輯的語言是對公開宣告邏輯語言的真擴(kuò)張，增加一組群體宣告算子[G]（G∈gr）。具體定義如下：

定義2.1(語言L) 群體宣告邏輯的語言L由如下規(guī)則給出（其中p∈pr，i∈ag且G∈gr）：

L采用跟 PAL語言一樣的設(shè)定，此外 [G]的對偶算子記為 〈G〉，即 〈G〉φ視為?[G]?φ的縮寫。當(dāng)G是某個(gè)單點(diǎn)集{i}時(shí)，一般將算子[{i}]和〈{i}〉分別簡寫為 [i]和 〈i〉。類似地，算子[ij]和 〈ij〉分別是 [{i,j}]和 〈{i,j}〉的縮寫。

直觀上來講，[G]φ將被用于表示“G中主體同時(shí)做出任意宣告，φ都成立”，〈G〉φ則表示“G中主體同時(shí)做出的某個(gè)宣告能使得φ成立”。GAL中要求每次群體宣告的內(nèi)容滿足：(1)必須是真實(shí)知識(shí)，即每個(gè)主體所宣告的內(nèi)容都是該主體的知識(shí)；(2)必須是公開的，即在群體宣告發(fā)生后所有主體都能夠獲取該群體宣告的信息；(3)群體中的所有主體同時(shí)做出宣告（多次群體宣告中的每次宣告都需要滿足此要求，但不同批次的宣告具有先后性）。

假設(shè)p∈pr、i∈ag、G∈gr且(M,s)是知識(shí)狀態(tài)，則群體宣告邏輯的語義滿足關(guān)系（符號|=GAL）在PAL語義的基礎(chǔ)上增加如下歸納條件：

相對于公開宣告邏輯，[1]中提供了群體宣告邏輯中如下一些額外的有效式（其中p∈pr、i,j∈ag、G,H ∈gr且φ是任意GAL公式）：

(1)群體宣告不改變原子命題的真值：

(2) 〈i〉Kjp ? 〈j〉Kip

(3) 空群宣告退化為未宣告：〈?〉φ ? [?]φ 和 [?]φ ? φ

(4)群體宣告全稱消去和存在引入（其中ψi是EL公式）：

(5)平凡宣告退化為未宣告：[G]φ→φ和φ→〈G〉φ

(6)同群多次宣告可由一次宣告實(shí)現(xiàn)：[G]φ→[G][G]φ和〈G〉〈G〉φ→〈G〉φ

(+) 由 (5)和 (6)可得到 [G]φ ? [G][G]φ 和 〈G〉φ ? 〈G〉〈G〉φ

(7)多群依次宣告可由一次宣告實(shí)現(xiàn)（不確定蘊(yùn)涵反方向是否有效）：

(8)Church-Rosser公式：〈G〉[G]φ → [G]〈G〉φ（不確定蘊(yùn)涵反方向是否有效）

(9)廣義Church-Rosser公式：〈G〉[H]φ → [H]〈G〉φ（蘊(yùn)涵反方向不有效）

(10)“必然會(huì)知道”當(dāng)且僅當(dāng)“知道必然會(huì)”：

(11)“知道如何做”就“知道能做”：

(12)“知道如何做”當(dāng)且僅當(dāng)“知道知道如何做”：

2.2.1 群體宣告邏輯的公理系統(tǒng)

在介紹群體宣告邏輯的公理系統(tǒng)之前首先引入如下定義。

定義2.2(容許型；Goldblatt[7,p.55]) 容許型由如下語法規(guī)則給出：

其中#是給定符號，φ是GAL公式，且i∈ag。

如果A是容許型，那么A(φ)表示用φ替換A中#后得到的公式。不難發(fā)現(xiàn)，任給公式φ和容許型A，A(φ)是GAL公式。

[1]中提供了GAL的一個(gè)可靠且完全的公理系統(tǒng)，它包含PAL的所有公理和規(guī)則以及以下三條公理或規(guī)則：

(1)[G]φ → [∧i∈GKiψi]φ，其中所有 ψi是 EL 公式；

(2)由φ得到[G]φ；

(3) 由 A([∧i∈GKiαi]φ)得到 A([G]φ)，其中所有 αi都是 EL 公式。

[1]中將上述第(3)條規(guī)則稱為Rω([G])，其中的上標(biāo)“ω”直觀上表明該條規(guī)則本身代表了可數(shù)無窮多種形式，這樣的規(guī)則有時(shí)被稱為無窮規(guī)則（infinitary rule）。[1]中還曾給出另一規(guī)則R[G]：

·由 φ → [χ][∧i∈GKipi]ψ 得到 φ → [χ][G]ψ，其中所有pi都不在 φ、ψ 和 χ中出現(xiàn)。

規(guī)則R[G]被稱為有窮規(guī)則（finitary rule）2這里稱其為有窮規(guī)則并不意味著該公理系統(tǒng)是有窮的公理系統(tǒng)；后者要求公理系統(tǒng)只使用有窮多條公理，以具備更美觀的數(shù)學(xué)形式。本文的公理系統(tǒng)通過公理模式給出，并不是有窮的公理系統(tǒng)；此類系統(tǒng)如果要轉(zhuǎn)變?yōu)橛懈F系統(tǒng)，通?？梢允褂么胍?guī)則實(shí)現(xiàn)。然而公理AP導(dǎo)致代入規(guī)則不可靠，因此無法簡單地轉(zhuǎn)變?yōu)橛懈F的公理系統(tǒng)，甚至很有可能不是有窮可公理化的。。[1]中試圖證明將無窮規(guī)則Rω([G])替換為有窮規(guī)則R([G])后得到的公理系統(tǒng)與原系統(tǒng)等價(jià)，并因此也是GAL的具有可靠性與完全性的公理系統(tǒng)。然而這一證明中存在錯(cuò)誤（文中Lemma 16無法得到），使用有窮規(guī)則的系統(tǒng)并不可靠，下節(jié)中證明其不可靠性。

3 有窮規(guī)則不是可靠的群體宣告邏輯規(guī)則

第2.2.1節(jié)中提到，[1]中提出使用有窮規(guī)則R[G]的公理系統(tǒng)，即包含PAL的所有公理和規(guī)則外加以下三條公理或規(guī)則的公理系統(tǒng)：

·[G]φ → [∧i∈GKiψi]φ，其中所有 ψi是 EL 公式；

·由φ得到[G]φ；

·規(guī)則R[G]：由 φ → [χ][∧i∈GKipi]ψ 得到 φ → [χ][G]ψ，其中所有pi都不在

φ、ψ和χ中出現(xiàn)。

然而該公理系統(tǒng)不是群體宣告邏輯的可靠系統(tǒng)。本節(jié)證明，R[G]不是群體宣告邏輯的可靠規(guī)則，即：

定理1在GAL中，規(guī)則R[G]不保持有效性。

下面給出定理1具體證明。只需找到具體反例，使得規(guī)則的前提有效但結(jié)論不有效。準(zhǔn)確說來，在規(guī)則R[G]中?。?/p>

引理1

證明:假設(shè)存在知識(shí)狀態(tài)(M,s)不滿足該公式，則如下兩項(xiàng)成立：

由M|Kiq,s|=Kip知M|Kiq,s|=p，則M,s|=p，并因此由（縮小模型不會(huì)減少一階知識(shí)，這一結(jié)論將在下面反復(fù)使用）。再由(1)知?jiǎng)t有：

由M,s|=Kiq知對所有t～is，有M,t|=Kiq，即t∈ M|Kiq。因M|Kiq,s|=Kip，對所有t～is，有M|Kiq,t|=p，故M,t|=p，因此有M,s|=Kip，所以：

接下來證明u2M|Kiq。假設(shè)u2∈M|Kiq。由u1∈M|Kiq且M|Kiq,u1|=KjKip（見u1引入處）知對所有u4∈M|Kiq使得u1～ju4，都有M|Kiq,u4|=Kip；同理M|Kiq,u2|=Kip（據(jù)本段假設(shè)及u1～ju2）。因此矛盾。

根據(jù)u2M|Kiq知存在u5∈M使得u2～iu5且M,u5|=?q。由u1～ju2、u2～iu5和M,u1|=p可得因此且矛盾。因此假設(shè)不成立，引理得證。□

引理2

證明:需找到一個(gè)知識(shí)狀態(tài)(M,s)，使得定義知識(shí)模型M=(W,～,V)滿足如下條件：

·W={s,t1,t2,t3,t4,t5,t6,t7}；

·～使得：～i是二元關(guān)系{(s,t4),(t1,t2),(t5,t6)}的自反對稱傳遞閉包，～j是{(s,t1),(t2,t3),(t4,t5),(t6,t7)}的自反對稱傳遞閉包，且對任意不同于i和j的主體k，都有～k=?；

·V使得：V(p)={s,t4}，V(r)={t3}，且對任意q∈pr{p,r}，V(q)=?。M的直觀如下圖所示（其中在狀態(tài)的上標(biāo)中明確標(biāo)注的命題在該狀態(tài)中為真，其它未標(biāo)注的命題在該狀態(tài)中皆為假）：

需要指出的是，[11]為APAL公理系統(tǒng)中的有窮規(guī)則找出的反例對于本節(jié)證明中反例的尋找有幫助。這里反例的復(fù)雜程度更高一些。

4 群體簡單宣告邏輯

在第2.2節(jié)給出的群體宣告邏輯（GAL）中，算子[G]的語義要求宣告內(nèi)容為EL公式。但正如引言中所提到的那樣，在實(shí)際中，理性主體的宣告往往只是用于陳述事實(shí)的一階知識(shí)，本節(jié)將引入新的邏輯以刻畫這類問題。

群體簡單宣告邏輯（Group Simple Announcement Logic，簡稱GSAL）是在群體宣告邏輯的基礎(chǔ)上，規(guī)定群體宣告的內(nèi)容只能是基于命題公式的一階知識(shí)而得到的邏輯系統(tǒng)。

GSAL使用與GAL完全一樣的語言，即語言L（定義2.1）。本文從現(xiàn)在開始以L為默認(rèn)語言，除明確指定，“公式”即指語言L中的公式。

GSAL的語義與GAL稍有不同。群體G中主體宣告的內(nèi)容必須是真實(shí)的、公開的，且由G中的主體同時(shí)做出宣告。但是宣告內(nèi)容有所不同，GSAL要求宣告的是命題邏輯的公式，這可以從如下語義解釋中看到。

定義4.1(滿足) 假設(shè)p∈pr、i∈ag、G∈gr且(M,s)是知識(shí)狀態(tài)，則群體簡單宣告邏輯的語義滿足關(guān)系（符號|=）由如下歸納條件給出：

其中M|φ的定義參考PAL語義。稱公式φ（在GSAL中）有效，記為|=GSALφ或簡單寫成|=φ，當(dāng)且僅當(dāng)對所有知識(shí)狀態(tài)(M,s)，M,s|=φ。

根據(jù)上述定義，對于[G]的對偶算子〈G〉，不難發(fā)現(xiàn)M,s|=〈G〉φ當(dāng)且僅當(dāng)存在 PL 公式集 {αi|i∈ G} 使得 M,s|= 〈∧i∈GKiαi〉φ。

類似于GAL，在GSAL中[G]φ直觀上仍被用于表示“G中主體同時(shí)做出任意宣告，φ都成立”，只不過這里將群體宣告的內(nèi)容限制為PL公式而GAL中允許EL公式，也就是說GSAL中群體任意宣告的內(nèi)容不能是高階知識(shí)，比如“別人知道某某事情”。3某個(gè)主體i宣告α實(shí)際起到的效果是Kiα被宣告，即“我知道α”。因此根據(jù)所知皆真和正內(nèi)省定理（可以得到|=Kiα?KiKiα），群體任意宣告的內(nèi)容實(shí)際上可以是“我知道我知道α”這樣的自指高階知識(shí)。

在EL、PAL和GAL中互模擬都對公式的滿足關(guān)系封閉，GSAL中也是如此，即如下命題成立：

命題4.1(互模擬性質(zhì)) 任給認(rèn)知狀態(tài)(M,s)和(M′,s′)，任給公式φ，如果(M,s)和(M′,s′)互模擬，則M,s|=φ當(dāng)且僅當(dāng)M′,s′|=φ。

GAL的有效式多數(shù)仍然是GSAL的有效式：

命題4.2令p∈pr、i,j∈ag、G,H∈gr且φ是任意公式，則下列公式都是有效式（證明從略）：

(1)p→ [G]p、?p→ [G]?p、〈G〉p→ p和 〈G〉?p → ?p

(2) 〈i〉Kjp ? 〈j〉Kip

(3) 〈?〉φ ? [?]φ 和 [?]φ ? φ

(4)[G]φ → [∧i∈GKiαi]φ 和 〈∧i∈GKiαi〉φ → [G]φ，其中 αi都是 PL 公式

(5)[G]φ → φ 和 φ → 〈G〉φ

(6)[G]φ → [G][G]φ 和 〈G〉〈G〉φ → 〈G〉φ

(+) 由 (5)和 (6)可得到 [G]φ ? [G][G]φ 和 〈G〉φ ? 〈G〉〈G〉φ

(7) 〈G〉[G]φ → [G]〈G〉φ（不確定蘊(yùn)涵反方向是否有效）

(8) 〈G〉[H]φ → [H]〈G〉φ（蘊(yùn)涵反方向不有效）

不難發(fā)現(xiàn)，GSAL的有效式有兩條與GAL不同：

2.GAL中有一條有效式：[G∪H]φ→[G][H]φ，而這不是GSAL的有效式（參見定理2）。

定理2假設(shè)G,H∈gr，則：

證明:定理1、2兩項(xiàng)等價(jià)，這里證明第2項(xiàng)?？紤]滿足如下條件的知識(shí)模型M=(W,～,V)：

·W={s,t,u,v}；

·～使得：～i為{(s,t),(u,v)}的自反對稱傳遞閉包，～j為{(s,u),(s,v)}的自反對稱傳遞閉包，且對任意k∈gr{i,j}，～k=?；

·V使得：V(p)={s}，V(q)={s,t,u}，且對任意r∈pr{p,q}，V(r)=?。模型M的直觀形式可以下圖(1)表示：

根據(jù)語義定義，M,s|=〈ij〉Kip當(dāng)且僅當(dāng)存在PL公式α和β使得M,s|=〈Kiα ∧Kjβ〉Kip，當(dāng)且僅當(dāng)存在 PL公式 α 和 β 使得 M,s|=Kiα ∧Kjβ 且M|(Kiα∧Kjβ),s|=Kip。要使M,s|=Kiα∧Kjβ，必須有α在s和t上真，且β在s、u和v上都真。又因?yàn)閠和u的賦值完全相同，因此α和β在兩個(gè)世界上同真同假，即有如下情況：

因此，模型M|(Kiα∧Kjβ)或者等同于M本身，或者等同于M|Kiq；在兩種情況下Kip都為假。即M,s|=Kiα ∧Kjβ 不成立，因此M,s〈ij〉Kip。

除了上面所提到的以外，還可以發(fā)現(xiàn)一些額外的有效式：

命題4.3(群體宣告歸約性質(zhì)) 假設(shè)φ和ψ是公式且α是PL公式，則下列公式是有效式：

1.[G](φ ∧ ψ)? ([G]φ ∧ [G]ψ)

2.[G]φ → φ

3.[G]?α ? ?[G]α

4.[G]α ? α

5 表達(dá)能力

本節(jié)主要證明GSAL的表達(dá)能力嚴(yán)格強(qiáng)于PAL。假設(shè)語言L和L′是通過同一模型類進(jìn)行解釋的兩個(gè)邏輯語言，稱：

·L′至少與L有相同的表達(dá)力，記為LL′，當(dāng)且僅當(dāng)對于所有的L公式φ，都存在L′公式ψ，使得φ和ψ在同一模型的同一狀態(tài)上的取值相同；

·L與L′有相同的表達(dá)力，記為L≡L′，當(dāng)且僅當(dāng)LL′且L′L；

·L′比L表達(dá)力強(qiáng)，記為L?L′，當(dāng)且僅當(dāng)LL′且L?L′；

·L和L′不可比較，當(dāng)且僅當(dāng)LL′且L′L。已經(jīng)知道的結(jié)論有（參見[5,1]）：

·如果|ag|=1（語言中只有一個(gè)主體），那么PAL≡GAL；

·如果|ag|≥2，那么PAL?GAL。

定理3如果|ag|=1，那么PAL≡GSAL。

證明:在|ag|=1的情況下，|=[i]φ?φ，因此PAL≡GSAL。 □

定理4如果|ag|≥2，那么PAL?GSAL。

證明:PALGSAL顯然成立。要證明PALGSAL，需要證明存在GSAL公式φ，但找不到PAL（或EL）公式ψ 使得|= φ ? ψ。令φ = 〈{a,b,c}〉〈Kip∧?KjKip〉。假設(shè)存在EL公式ψ使得|=φ?ψ，令q和r是不在ψ中出現(xiàn)的命題變元，不難定義如下圖所示的模型M和M′:

6 公理系統(tǒng)

群體簡單宣告邏輯的公理系統(tǒng)GSAL如圖2所示。GSAL包括PAL的所有

圖2:群體簡單宣告邏輯的公理系統(tǒng)GSAL

公理和規(guī)則以及以下三條公理或規(guī)則：

·AG：群體宣告化簡公理（Axiom of Group Announcement Simplification）

·RG1：群體宣告引入規(guī)則（Rule of Group Announcement Introduction）

·RG2：群體宣告歸納規(guī)則（Rule of Group Announcement Induction）

GSAL是PAL的擴(kuò)張，包含PAL的所有公理和規(guī)則。GSAL沒有關(guān)于算子[G]的可歸約的公理，這與語義情況一致。

6.1 等值置換規(guī)則

等值置換規(guī)則是非常重要但常被疏忽的一條規(guī)則。很多公理系統(tǒng)中無此規(guī)則，但該規(guī)則可容許，而有些系統(tǒng)中不容許此規(guī)則。在后一種情況下，一旦證明中用到此規(guī)則就可能得到錯(cuò)誤結(jié)論。本節(jié)中將對此規(guī)則加以探討。

所謂等值置換規(guī)則，是指由(ψ?χ)得到(φ?φ′)，其中φ′是將φ中的某個(gè)ψ替換為χ后得到的公式。

上述規(guī)則可以分別從語義和語法兩個(gè)角度來看。對GSAL而言，從語義方面來看，下面的定理說明等值置換規(guī)則保持語義有效性。

定理5等值置換規(guī)則在GSAL中保持語義有效性。即任給公式ψ和χ使得|=ψ?χ，任給公式φ。以φ′表示將φ中某個(gè)子公式ψ替換為χ后得到的公式，則|=φ?φ′。

從語法方面看，則是說在公理系統(tǒng)中該規(guī)則可容許，亦即如下性質(zhì)：

“任給公式ψ和χ使得?ψ?χ，任給公式φ，并以φ′表示將φ中某個(gè)子公式ψ替換為χ后得到的公式，則?φ?φ′。”

GSAL中并未明確允許使用等值置換規(guī)則，如果要用，則需要首先證明上述性質(zhì)成立。然而要證明這一點(diǎn)存在一定的困難。事實(shí)上，對上述性質(zhì)使用歸納證明（施歸納于φ的結(jié)構(gòu)）時(shí)，當(dāng)φ形如p、?λ、(λ∧δ)、Kiλ、[G]λ時(shí)都可以得到證明，唯獨(dú)[λ]δ情形存在問題，對此情形需要分別證明（其中λ′和δ′分別是將λ和δ中某個(gè)子公式ψ替換為與之等值的χ后得到的公式）：

上述結(jié)論1也很容易證明，這里無法提供結(jié)論2的證明。

當(dāng)然，根據(jù)定理5和下面將要證明的完全性定理，不難發(fā)現(xiàn)等值置換規(guī)則確實(shí)是GSAL可容許的規(guī)則。只是這樣一來，在完全性定理的整個(gè)證明中必須保證不使用該規(guī)則，否則將陷入循環(huán)證明。

6.2 連續(xù)宣告

連續(xù)進(jìn)行多次宣告有一些有意思的結(jié)論，而這些結(jié)論有些在某篇論文的某個(gè)證明用到，有些則從未被證明。本節(jié)將嘗試對連續(xù)宣告進(jìn)行系統(tǒng)化的梳理，一來便于讀者查閱相關(guān)結(jié)論，二來也有助于下面的證明。

定理6(方形連續(xù)宣告) 任給自然數(shù)n（n≥1），命題變元p，公式ψ、χ和公式序列φ1,...,φn，如下公式是GSAL的定理：

定理7(菱形連續(xù)宣告) 任給自然數(shù)n（n≥1），命題變元p，公式ψ、χ和公式序列φ1,...,φn，如下公式是GSAL的定理：

6.3 與GSAL證明能力相同的公理系統(tǒng)

本節(jié)中將引入兩個(gè)與GSAL證明能力相同的兩個(gè)公理系統(tǒng)：GSAL′和GSAL′′（圖3），其目的是便于后文中完全性定理的證明。這兩個(gè)公理系統(tǒng)與GSAL的差

圖3:群體簡單宣告邏輯的公理系統(tǒng)GSAL′和GSAL′′

上面定義的公式復(fù)雜度有時(shí)也稱為模態(tài)度（modaldegree）。每條公式的復(fù)雜度都是一個(gè)自然數(shù)。所有PL公式的復(fù)雜度都為0，且[G]ψ的復(fù)雜度高于∧i∈GKiαi（其中αi是PL公式）。

引理3令Q={q1,...,qn,...}為一集命題變元，Γ={α1,...,αk}是一集PL公式，使得Γ中出現(xiàn)的命題變元與Q中的命題變元不相交。對任意GSAL公式別在于將規(guī)則RG2分別替換為RG2′和RG2′′（其中A是定義2.2中引入的容許型概念的GSAL版本）：

·RG2′：由 A([∧i∈GKipi]φ)得 A([G]φ)，其中所有 pi都不在 A 和 φ 中出現(xiàn)。

·RG2′′：由 A([∧i∈GKiαi]φ)得 A([G]φ)，其中所有 αi都是 PL 公式。

有窮規(guī)則RG2與RG2′具有同等的推演能力，這可以采用類似于[1,Lemma 17]的證明得到。另一方面，有窮規(guī)則RG2′不比無窮規(guī)則RG2′′弱：滿足RG2′′的前提則也滿足RG2′的前提。

由此首先可以得到GSAL和GSAL′是證明能力相同的系統(tǒng)：這兩個(gè)系統(tǒng)的定理集完全一致。GSAL′′的證明能力則不強(qiáng)于GSAL′，即前者的定理集是后者定理集的子集。在第6.4節(jié)給出完全性結(jié)論后，事實(shí)上知道GSAL′′的證明能力并不弱于GSAL′。因此結(jié)論是，這三個(gè)系統(tǒng)的證明能力相同。

所有GSAL的定理都是有效的，是為系統(tǒng)GSAL的可靠性（soundness）。要證明這個(gè)結(jié)論，只需要證明相應(yīng)公理系統(tǒng)的所有公理都有效，并且所有規(guī)則都可靠（即保持有效性）即可。就GSAL而言，PAL公理的有效性和規(guī)則的可靠性已知，此外不難證明規(guī)則AG和RG1的可靠性。需要證明的主要是規(guī)則RG2的可靠性。與之等價(jià)地可以證明RG2′的可靠性，并由此知規(guī)則RG2′′的可靠性。接下來給出證明RG2′的可靠性證明。

首先定義GSAL公式的復(fù)雜度，這樣做是為了使公式[G]φ的復(fù)雜度高于φ和群體宣告的內(nèi)容∧i∈GKiαi，從而實(shí)現(xiàn)歸納證明。

定義6.1(公式復(fù)雜度) 公式φ的復(fù)雜度c(φ)由如下條件歸納得到：ψ，考慮兩個(gè)對其進(jìn)行代入后得到的公式：ψα表示而ψ?α表示則對任意模型M，存在模型M′，使得：

(1) 對任意 i∈ {1,...,k}，?qi?M′= ?αi?M′= ?αi?M；

(2) 對任意GSAL 公式 φ，?φ?M′= ?φα?M。

其中，對任意公式 φ和模型 M，?φ?M表示 φ在 M 中的真值集，即 ?φ?M={s|M,s|= φ}（下同）。

證明:類似于[1,Lemma 8]的證明。 □

引理4任給群體G={1,...,n}，GSAL公式ψ和不在ψ中出現(xiàn)的一組命題變元 p1,...,pn。如果知識(shí)狀態(tài) (M,s)使得（其中對任意i∈G，αi是PL公式），則存在模型N使得：①②對ψ中出現(xiàn)的所有命題變元r都有?r?N=?r?M，且③對任意i∈G都有?pi?N=?αi?M。

證明:假設(shè)引理的前提成立。令P={p1,...,pn,...}為一集命題變元，使得其中每個(gè)元素都不在ψ中出現(xiàn)。令Q={q1,...,qn,...}為一集新的命題變元，其中每個(gè)元素都不在P、ψ和任意αi（i∈G）中出現(xiàn)；公式即由引理3(2)知存在M′使得對所有pQ都有?p?M′=?p?M（引理3(2)中的“φα”在此時(shí)是pα，即p），且由引理3(1)知對所有i∈G有 ?qi?M′= ?αi?M；再由假設(shè)和引理 3(2)知

將P視為引理3前提中的Q，將{q1,...,qn}視為{α1,...,αk}。對所有qP，由引理3(2)知存在N 使得，?q?N= ?q?M′（引理3(2)中的“φα”在此時(shí)是qα，即q），且由引理 3(1)知對所有 i∈ G，?pi?N= ?qi?M′。在引理3(2)中，將視為φ，則（因P∩Q=?），即又因（上一段已證），有此外，對于ψ中出現(xiàn)的所有命題變元r，因?yàn)镻、Q和ψ中出現(xiàn)的命題變元互不相交，有rP且rQ，根據(jù)前面的結(jié)論知?r?N=?r?M′=?r?M且對所有i∈G，?pi?N= ?qi?M′= ?αi?M。 □

引理5任給群體G={1,...,n}，容許型A，GSAL公式ξ和一組不在A([G]ξ)中出現(xiàn)的命題變元pi(i∈G)。如果存在知識(shí)狀態(tài)(M,s)=((W,～,V),s)使得 M,sA([G]ξ)，則存在模型 M′=(W,～,V′)，使得 M′,sA([∧i∈GKipi]ξ)且對A([G]ξ)中出現(xiàn)的所有命題變元r都有V′(r)=V(r)。

證明:任給群體G，容許型A，GSAL公式ξ和一組不在A([G]ξ)中出現(xiàn)的命題變元pi(i∈G)。首先，對任意知識(shí)狀態(tài)(M,s)，容許型A和GSAL公式ξ，如果M,s ?A([G]ξ)，則存在 PL 公式集 {αi|i∈ G}，使得 M,s ?A([∧i∈GKiαi]ξ)。通過施歸納于A的結(jié)構(gòu)不難證明。

根據(jù)上述結(jié)論，要證本引理，證明如下結(jié)論足矣：對任意知識(shí)狀態(tài)(M,s)=((W,～,V),s)，容許型 A 和給定的 ξ，如果 M,sA([∧i∈GKiαi]ξ)，則存在模型M′=(W,～,V′)使得：①M(fèi)′,sA([∧i∈GKipi]ξ)，②對A(ξ)中出現(xiàn)的所有命題變元r都有V′(r)=V(r)，且③對任意i∈G都有V′(pi)=?αi?M。

施歸納于容許型A的結(jié)構(gòu)：

(1)A=#：此時(shí) A([∧i∈GKiαi]ξ)=[∧i∈GKiαi]ξ，可由引理 4 得到結(jié)論。

(2)A=KiA′：此時(shí) A([∧i∈GKiαi]ξ) 為 KiA′([∧i∈GKiαi]ξ)。如果 M,s ?KiA′([∧i∈GKiαi]ξ)，則存在 t～is 使得 M,tA′([∧i∈GKiαi]ξ)。根據(jù)歸納假設(shè)，存在 M′=(W,～,V′)使得 M′,tA′([∧i∈GKipi]ξ)，對 A′(ξ)中（即 KiA′(ξ)中）出現(xiàn)的所有命題變元r都有V′(r)=V(r)，且對任意i∈G都有V′(pi)=?αi?M。此時(shí)有 M′,sKiA′([∧i∈GKipi]ξ)。

(3)A=[φ]A′：此時(shí) A([∧i∈GKiαi]ξ) 為 [φ]A′([∧i∈GKiαi]ξ)。如果 M,s[φ]A′([∧i∈GKiαi]ξ)，則 M,s|= φ 且 M|φ,sA′([∧i∈GKiαi]ξ)。根據(jù)歸納假設(shè)，存在與M|φ僅賦值上有區(qū)別的模型(M|φ)′=(W|φ,～|φ,(V|φ)′)使得：①(M|φ)′,sA′([∧i∈GKipi]ξ)，②對A′(ξ)中出現(xiàn)的所有命題變元r都有(V|φ)′(r)=(V|φ)(r)，且③對任意i∈G都有(V|φ)′(pi)=?αi?M|φ。定義模型M′=(W,～,V′)使得：

·對所有在 [φ]A′(ξ)中出現(xiàn)的命題變元 p，V′(p)=V(p)；

·對所有 i∈ G，V′(pi)= ?αi?M；

·對所有其它命題變元 q，V′(q)=(V|φ)′(q)。不難驗(yàn)證：

·?φ?M′= ?φ?M，M′,s|= φ，且 M′|φ =(M|φ)′；所以有 M′|φ,sA′([∧i∈GKipi]ξ)，并因此 M′,s[φ]A′([∧i∈GKipi]ξ)；

·對所有在[φ]A′(ξ)中出現(xiàn)的命題變元r，V′(r)=V(r)（由定義給定）；

·對所有 i∈ G，V′(pi)= ?αi?M（由定義給定）。

(4)A=(φ → A′)：此時(shí) A([∧i∈GKiαi]ξ) 為 φ → A′([∧i∈GKiαi]ξ)。對任意知識(shí)狀態(tài) (M,s)=((W,～,V),s)，如果 M,sφ → A′([∧i∈GKiαi]ξ)，則M,s|= φ 且 M,sA′([∧i∈GKiαi]ξ)。根據(jù)歸納假設(shè)，存在模型M′=(W,～,V′)使得：①M(fèi)′,sA′([∧i∈GKipi]ξ)，②對A′(ξ)中出現(xiàn)的所有命題變元r都有V′(r)=V(r)，且③對任意i∈G都有V′(pi)=?αi?M。

然而模型M′未必能夠使得M′,s|=φ。為此定義模型M′′=(W,～,V′′)，其中對所有在φ中出現(xiàn)的命題變元p，都有V′′(p)=V(p)；對其余命題變元q，有V′′(q)=V′(q)。不難驗(yàn)證 A′([∧i∈GKipi]ξ在 M′和 M′′中的所有狀態(tài)上同真同假（根據(jù)定義pi(i∈ G)不在φ中出現(xiàn)，因此V′′(pi)=V′(pi)；而A′(ξ)中出現(xiàn)的所有任意變元r，如果r在φ中出現(xiàn)則V′′(r)=V(r)=V′(r)，如果不在φ中出現(xiàn)則仍有 V′′(r)=V′(r)），因此 M′′,s ?A′([∧i∈GKipi]ξ。

對{pi|i∈G}不在其中出現(xiàn)的任意公式ψ，定義模型N=(W,～,U)使得：

·對所有在ψ中出現(xiàn)的命題變元p，都有U(p)=V(p)；且

·對所有其它命題變元q，有U(q)=V′(q)。

下面證明結(jié)論：對M和N的所有具有相同個(gè)體域的子模型Ms和Ns，對任意狀態(tài)w和任意公式ψ使得{pi|i∈G}不在其中出現(xiàn)，Ms,w|=ψ當(dāng)且僅當(dāng)Ns,w|=ψ。由此可得M′′,s|=φ。施歸納于c(ψ)：基本情形和命題聯(lián)結(jié)詞情形易證，下面證明模態(tài)詞的情形。

·Kiχ情形：Ms,s|=Kiχ，當(dāng)且僅當(dāng)對所有t∈ Ms，如果s～it則Ms,t|= χ，當(dāng)且僅當(dāng)對所有t∈Ns，如果s～it則Ns,t|=χ（歸納假設(shè)）,當(dāng)且僅當(dāng)Ns,s|=Kiχ。

·[ψ1]ψ2情形：Ms,s|=[ψ1]ψ2，當(dāng)且僅當(dāng)如果 Ms,s|= ψ1則 Ms|ψ1,s|= ψ2，當(dāng)且僅當(dāng)如果Ns,s|=ψ1則Ns|ψ1,s|=ψ2（Ms|ψ1和Ns|ψ1有相同個(gè)體域），當(dāng)且僅當(dāng) Ns,s|=[ψ1]ψ2。

·[G]χ情形：Ns,s ?|=[G]χ，當(dāng)且僅當(dāng)存在PL公式集{βi|i∈ G}使得Ns,s|=使得（由 N 的定義和 ③ 知 U(pi)=V′(pi)= ?αi?M，故由歸納假設(shè)當(dāng)且僅當(dāng)

由上述結(jié)論知：M′′,s|=φ，因此如下結(jié)論都成立：

·M′′,sφ → A′([∧i∈GKipi]ξ)；

·對φ→A′(ξ)中出現(xiàn)的所有命題變元r都有V′′(r)=V(r)（根據(jù)定義，對φ中出現(xiàn)的所有命題變元p，V′′(p)=V(p)；而A′(ξ)中出現(xiàn)的所有任意變元r，如果r在φ中出現(xiàn)則V′′(r)=V(r)=V′(r)，如果不在φ中出現(xiàn)則仍有V′′(r)=V′(r)）；

·對任意i∈G都有V′′(pi)=?αi?M（因?yàn)閜i不在φ中出現(xiàn)，所以由V′′定義和 ③ 知 V′′(pi)=V′(pi)= ?αi?M）。

因此，M′′是滿足條件的模型。

(1)–(4)完成了對容許型的歸納，證明完畢。 □

上述引理與[1,Lemma 16]非常相似，但那里是針對GAL的證明，其中的錯(cuò)誤在于歸納步驟A=(φ→A′)無法得到。上述引理中針對GSAL則該步可以通過。

引理6規(guī)則RG2′在GSAL中保持有效性。

證明:假設(shè)RG2′不保持有效性。則存在容許型A使得A([∧i∈GKipi]φ)有效且A([G]φ)不有效。因此存在知識(shí)狀態(tài)不滿足A([G]φ)。由引理5知存在知識(shí)狀態(tài)不滿足 A([∧i∈GKipi]φ)，與假設(shè)矛盾。 □

定理8 GSAL、GSAL′和GSAL′′都是可靠的。

6.4 完全性

本節(jié)主要證明系統(tǒng)GSAL′′的完全性定理，由此可以得到GSAL的完全性（GSAL是比GSAL′′證明能力更強(qiáng)的系統(tǒng)）。GSAL′′完全性定理的證明使用常見的典范模型方法（canonical model method），證明過程類似于[2,第4節(jié)]。4除了邏輯和公理系統(tǒng)的差別，本文與參考文獻(xiàn)中的不同還在于對極大一致理論的定義不同[2,第4節(jié)]中使用的極大一致理論定義不同于常見定義，本文重新用回常見定義以便于閱讀，證明過程并未復(fù)雜化），并且本文證明強(qiáng)完全性定理而非弱完全性定理。

任給公式集Φ和公式φ，稱Φ推出φ（記為Φ?φ），如果存在Φ的有窮子集Ψ使得以Ψ為前提集可構(gòu)造以φ結(jié)束的GSAL′′證明序列。稱Φ一致（consistent），如果ΦGSAL′′⊥。稱Φ極大一致（maximal consistent），如果Φ一致且真包含Φ的任何公式集都不一致。極大一致的公式集也被稱為極大一致理論，簡稱理論。

理論的上述定義與經(jīng)典定義并無二致，具有對命題聯(lián)結(jié)詞的一些封閉性質(zhì)，這里不再贅述。Lindenbaum引理同樣成立，即任何公式集都可以擴(kuò)充為理論，證明從略。

定義6.2(典范模型) Mc=(Wc,～c,Vc)稱為典范模型（canonical model），如果：

·Wc是所有理論的集合；

·～c∶ag→ ?(W ×W)使得當(dāng)且僅當(dāng){φ|Kiφ ∈ x}={φ|Kiφ ∈y}；

·Vc∶pr→ ?(W)：x∈ Vc(p)當(dāng)且僅當(dāng)p∈x。

定義6.3(按序宣告) 任給有窮公式序列〉和理論Φ。稱Φ對按序宣告封閉，當(dāng)且僅當(dāng) ψ1∈ Φ，[ψ1]ψ2∈ Φ，……且 [ψ1]···[ψk?1]ψk∈ Φ。

上述定義將有助于接下來對真值引理的敘述和證明。

引理7(真值引理) 令φ為一公式。對于所有的理論x和所有有窮公式序列如果 x 對按序宣告封閉，則 Mc|ψ1|···|ψk,x|= φ 當(dāng)且僅當(dāng)[ψ1]···[ψk]φ ∈ x。

證明:施歸納于c(φ)：

基本情形：結(jié)論對所有PL公式成立。證明較簡單，此處略去。

Kiχ 情形。從右至左：證明其逆否命題；令 Mc|ψ1|···|ψk,xKiχ，由語義定義，存在理論 y 使得：且 Mc|ψ1|···|ψk,yχ——其中 ～′是模型Mc|ψ1|···|ψk三元組的第二個(gè)元素——故有(Mc,y)滿足按序宣告，再反復(fù)使用歸納假設(shè)可得y對按序宣告封閉。因而由歸納假設(shè)可得[ψ1]···[ψk]χy。由x～iy知{φ|Kiφ∈x}={φ|Kiφ∈y}，因此[ψ1]···[ψk]χx，故而Ki[ψ1]···[ψk]χx。由公理AK可得[ψ1]···[ψk]Kiχx。從左至右：證明其逆否命題；假設(shè)[ψ1]···[ψk]Kiχx，由引理前提和定理6可得Ki[ψ1]···[ψk]χx。令y={φ |Kiφ ∈ x}∪{?[ψ1]···[ψk]χ}。y 一致（假設(shè)不一致，則存在 φ1,...,φn∈{φ |Kiφ ∈ x} 使得 ? (φ1∧···∧φn)→ [ψ1]···[ψk]χ，因此? (Kiφ1∧···∧Kiφn)→Ki[ψ1]···[ψk]χ，并進(jìn)一步有 Ki[ψ1]···[ψk]χ ∈ x，與假設(shè)矛盾）。將 y 擴(kuò)充為理論y′，則{φ|Kiφ∈x}?y′且[ψ1]···[ψk]χy′。因此且y′對于按序宣告封閉。由歸納假設(shè)，Mc|ψ1|···|ψk,y′?χ。因此 Mc|ψ1|···|ψk,x ?Kiχ。

[χ]ξ情形：假設(shè) Mc|ψ1|···|ψk,x[χ]ξ，則 Mc|ψ1|···|ψk,x|= χ 且 Mc|ψ1|···|ψk|χ,xξ。由合取支前者、歸納假設(shè)和引理的按序宣告封閉條件知 [ψ1]···[ψk]χ∈x，由此再根據(jù)歸納假設(shè)和引理?xiàng)l件可得[ψ1]···[ψk][χ]ξx。反過來，假設(shè)[ψ1]···[ψk][χ]ξx，則 ?[ψ1]···[ψk][χ]ξ∈x，則〈ψ1〉···〈ψk〉〈χ〉?ξ∈x，根據(jù)定理 7，有 [ψ1]···[ψk]χ ∈ x。因此 x 對 〈φ1,...,φk,χ〉按序宣告封閉，由歸納假設(shè)，Mc|ψ1|···|ψk|χ,xξ。因此，Mc|ψ1|···|ψk,x[χ]ξ。

[G]χ 情形：假設(shè) Mc|ψ1|···|ψk,x[G]φ，則存在 PL 公式序列 {αi|i ∈G}，使得 Mc|ψ1|···|ψk,x[∧i∈GKiαi]φ，則 Mc|ψ1|···|ψk,x|= ∧i∈GKiαi且Mc|ψ1|···|ψk|∧i∈GKiαi,xφ。根據(jù)歸納假設(shè)，[ψ1]···[ψk]∧i∈GKiαi∈ x，并因此 x 對 〈ψ1,...,ψk,∧i∈GKiαi〉按序宣告封閉。使用歸納假設(shè)可得 [ψ1]···[ψk][∧i∈GKiαi]φx。由公理[G]φ→[∧i∈GKiαi]φ 和宣告規(guī)則RA，可得[ψ1]···[ψk][G]φx。

反過來，假設(shè)[ψ1]···[ψk][G]φx，根據(jù)規(guī)則RG2′′和理論的定義可知，[ψ1]···（其中所有 αi都是PL公式）。由理論的性質(zhì)知?[ψ1]···[ψk]因此由定理7 知 [ψ1]···[ψk]前者結(jié)合引理中的按序宣告封閉條件可得 x 對按序宣告封閉；后者結(jié)合公理 ([φ]?ψ ?(φ → ?[φ]ψ))和理論的性質(zhì)可得根據(jù)歸納假設(shè)，因此，Mc|ψ1|···|ψk,x[G]φ?！?/p>

定理9(強(qiáng)完全性) 任給公式集Φ，如果在GSAL′′中Φ一致，則Φ可滿足。（這等價(jià)于：任給公式集Ψ和公式φ，如果Ψ|=φ則Ψ?GSAL′′φ。）

證明:首先使用Lindenbaum引理將Φ擴(kuò)充為理論Φ+。由真值引理知Mc,Φ+|=φ當(dāng)且僅當(dāng)φ∈Φ+。因此Mc,Φ+|=Φ，即Φ可滿足。 □

7 結(jié)論

本文探討了一種特殊的群體宣告邏輯：僅允許群體宣告一階知識(shí)，這一設(shè)定適用于很多實(shí)際場合；文中稱這類邏輯為群體簡單宣告邏輯。群體簡單宣告邏輯與公開宣告邏輯（[13]）、任意公開宣告邏輯（[2]）、群體宣告邏輯（[1]）等一脈相承，在邏輯性質(zhì)和證明方法等方面與群體宣告邏輯頗為相似，但也有很多不同之處；突出的例子如，對后者不可靠的有窮規(guī)則對前者可靠，后者的有效式〈G〉〈H〉φ→〈G∪H〉φ（“多群依次宣告可由一次宣告實(shí)現(xiàn)”）不是前者的有效式。文章對群體簡單宣告邏輯進(jìn)行了細(xì)致的探索，包括邏輯有效式、表達(dá)能力、公理系統(tǒng)及其完全性證明等，也附帶著對群體宣告邏輯進(jìn)行了梳理。

我們嘗試將群體簡單宣告邏輯的表達(dá)能力與群體宣告邏輯進(jìn)行對比，但尚未得到結(jié)論，因此在第5節(jié)中避而不談，只能將這一開放性問題留待今后解決。在群體（簡單）宣告邏輯（以及任意公開宣告邏輯）中添加公共知識(shí)和分布式知識(shí)等群體知識(shí)算子是下一步工作的主要目標(biāo)之一，比如群體宣告與群體知識(shí)如何形成互動(dòng)就是一個(gè)有意思的問題。計(jì)算復(fù)雜性問題也同樣值得探索。在群體宣告中允許事實(shí)改變或非公開宣告等想法都是一直被提及卻從未被解決的問題。我們將在今后逐步探索下去，但這些都超出了本文所能涵蓋的范圍。

[1]T.?gotnes,P.Balbiani,H.van Ditmarsh and P.Seban,2010,“Group announcement logic”,Journal of Applied Logic,8(1):62–81.

[2]P.Balbiani,A.Baltag,H.van Ditmarsh,A.Herzig,T.Hoshi and T.de Lima,2008,“‘Knowable’as ‘known after an announcement’”,Review of Symbolic Logic,1(3):305–334.

[3]P.Balbiani,2015,“PuttingrightthewordingandtheproofofthetruthlemmaforAPAL”,Journal of Applied Non-Classical Logics,25(1):2–19.

[4]P.Balbiani and H.P.van Ditmarsch,2015,“A simple proof of the completeness of APAL”,Studies in Logic,8(1):65–78.

[5]H.van Ditmarsh,W.van der Hoek and B.Kooi,2007,Dynamic Epistemic Logic,Netherlands:Springer.

[6]R.Fagin,J.Y.Halpern,Y.Moses and M.Y.Vardi,1995,Reasoning about Knowledge,Cambridge,MA:The MIT Press.

[7]R.Goldblatt,1982,Axiomatising the Logic of Computer Programming,Berlin:Springer-Verlag.

[8]J.Hintikka,1962,Knowledge and Belief:An Introduction to the Logic of Two Notions,Ithaca,New York:Cornell University Press.

[9]B.Kooi and J.van Benthem,2004,“Reduction axioms for epistemic actions”,Proc.Advances in Modal Logic,pp.197–211.

[10]B.Kooi,2007,“Expressivity and completeness for public update logics via reduction axioms”,Journal of Applied Non-Classical Logics,17(2):231–253.

[11]L.B.Kuijer,Unsoundness of R(□),http://personal.us.es/hvd/errors.html.

[12]J.-J.C.Meyer and W.van der Hoek,1995,Epistemic Logic for AI and Computer Science,New York:Cambridge University Press.

[13]J.A.Plaza,1989,“Logics of public communications”,in M.L.Emrich,M.S.Pfeifer,M.Hadzikadic and Z.W.Ras(eds.),Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems(ISMIS ’89),pp.201–216.