宋鵬飛 熊衛(wèi)

1 引言

動(dòng)態(tài)認(rèn)知邏輯（Dynamic Epistemic Logic，[8]）涉及兩個(gè)主要的信息動(dòng)態(tài)變化：公開宣告（Public Announcement）和個(gè)體信念更新（Private Belief Update）。信息的動(dòng)態(tài)變化不僅會導(dǎo)致知識和信念的改變，也會導(dǎo)致覺知（Awareness）的改變。本文主要討論個(gè)體信念更新1本文中，如果模型滿足定義7，則該模型刻畫了知識，此時(shí)的信念更新也是知識更新。及其相應(yīng)的覺知變化，比如下面的例子：

例1.小張住在酒店，他知道酒店的餐廳有提供咖啡的服務(wù)，但是不確定餐廳今天是否提供咖啡。另外，小張對于餐廳有提供茶水的服務(wù)沒有覺知。這時(shí)，小張聽到有人說，今天餐廳不會同時(shí)提供咖啡和茶水。得知這個(gè)消息之后，小張雖然仍不知道餐廳今天是否提供咖啡和茶水，但是覺知到了餐廳有提供茶水的服務(wù)這件事。事實(shí)上，今天餐廳既不會提供咖啡，也不會提供茶水。令p為“餐廳今天提供咖啡”，q為“餐廳今天提供茶水”。小張的知識變化如圖1 所示。

圖1 是兩個(gè)單主體模型。左邊的模型表示小張得到信息之前的認(rèn)知狀態(tài)，其中只包含一個(gè)原子命題p，實(shí)心點(diǎn)是p為真的可能世界，空心點(diǎn)是p為假的可能世界，有下劃線的可能世界是當(dāng)前的可能世界，模型中的箭頭表示主體的可通達(dá)關(guān)系，顯然它是等價(jià)關(guān)系；右邊的模型表示小張得到信息之后的認(rèn)知狀態(tài)，其中包含兩個(gè)原子命題p和q，每個(gè)可能世界有兩個(gè)點(diǎn)，左邊的點(diǎn)表示p的真值，右邊的點(diǎn)表示q的真值，實(shí)心為真，空心為假，與左側(cè)模型一樣，有下劃線的可能世界為當(dāng)前可能世界，箭頭表示主體的可通達(dá)關(guān)系，它也是等價(jià)關(guān)系。

在模態(tài)邏輯中，不確定性可以通過命題在不同可能世界中的不同取值來刻畫。對于某一主體在某一可能世界，如果一個(gè)命題在所有可通達(dá)的可能世界為真，則該主體相信（或知道）該命題為真。例1 描述了一個(gè)很簡單的場景，圖1 的可能世界模型刻畫了該場景。但是，例1 與通過模態(tài)邏輯來刻畫知識和信念的經(jīng)典方法有所不同。在模態(tài)邏輯中，我們假設(shè)任一主體都能夠覺知到所有相關(guān)的原子命題，這一假設(shè)被稱為封閉世界假設(shè)（Closed World Assumption，[3]），而例1 中的主體得到信息導(dǎo)致模型增加了新的原子命題，顯然，其不符合這一假設(shè)。因此，研究者嘗試修改和完善克里普克模型，以支持主體對命題或公式有不同程度的覺知，以及主體的覺知發(fā)生變化。與此同時(shí)，在相應(yīng)的邏輯語言中，也需要在認(rèn)知邏輯中增加覺知算子以及導(dǎo)致覺知發(fā)生變化的動(dòng)態(tài)算子。

形式刻畫覺知的方案主要有兩種：句法進(jìn)路（[9-11]）和語義進(jìn)路（[13,14,21,22]）。這兩種方案的差異主要體現(xiàn)在哲學(xué)觀點(diǎn)的不同。其中，句法進(jìn)路認(rèn)為，每一個(gè)可能世界都是客觀的，所有的原子命題在任一可能世界都有取值；而語義進(jìn)路則認(rèn)為，可能世界是主觀的，是存在于主體的思想中的，因此，那些沒有被主體覺知到的原子命題就會在相應(yīng)的可能世界上沒有取值。具體而言，句法進(jìn)路在可能世界語義中增加了覺知函數(shù)，使每一個(gè)主體在每一個(gè)可能世界對應(yīng)一個(gè)公式集；而語義進(jìn)路則是將克里普克語義結(jié)構(gòu)擴(kuò)展為所有主觀可能世界構(gòu)成的完全格。

由于上述兩種方案都是在克里普克語義上加以擴(kuò)展，因此，在處理個(gè)體信念更新的問題時(shí)，都會產(chǎn)生同樣的問題，即，當(dāng)某一主體接收到某一條信息，原本的認(rèn)知模型需要被復(fù)制成兩個(gè)副本，一個(gè)副本用來刻畫接收到信息的主體的認(rèn)知狀態(tài)，另一個(gè)副本用來刻畫未接收到信息的主體的認(rèn)知狀態(tài)。這樣做的結(jié)果是，在一系列個(gè)體信念更新之后，認(rèn)知模型會發(fā)生幾何級數(shù)的增長。

由羅里尼（Lorini）提出的信念態(tài)度邏輯（Logic of Doxastic Attitude，[16,17]）能夠有效地規(guī)避上述問題。信念態(tài)度邏輯是以信念庫（Belief Base，[12,20,23,24]）為基礎(chǔ)的邏輯，而信念庫則是信念更新的AGM 方案（[1]）的重要概念。在信念態(tài)度邏輯中，對于個(gè)體信念更新，只需要改變該個(gè)體的信念庫，而其他個(gè)體的信念庫保持不變。由此，信念態(tài)度邏輯給出了個(gè)體信念更新的一種“節(jié)省的”方案，避免了復(fù)制模型導(dǎo)致的模型復(fù)雜度的幾何級數(shù)增加。至此，有兩種個(gè)體信念更新方式，即，通過改變信念庫而實(shí)現(xiàn)的個(gè)體信念更新和通過復(fù)制模型而實(shí)現(xiàn)的個(gè)體信念更新，羅里尼（[17]）證明了這兩種個(gè)體信念更新所產(chǎn)生的模型具有互模擬關(guān)系。但是，羅里尼的理論中并不包含覺知，因而不能涵蓋前文提到的例子。對此，羅里尼等人在[18,19]提出了包含覺知算子的信念態(tài)度邏輯，并形成了與上述兩種方案并列的第三種刻畫覺知的方案——信念庫進(jìn)路（Belief Base Approach）。以此為基礎(chǔ)，本文將在包含覺知算子的情況下證明上述兩種信念更新產(chǎn)生的模型具有互模擬關(guān)系，并給出其成立的條件。另外，雖然[19]列出了該邏輯的個(gè)體信念更新擴(kuò)充的公理，但并未證明這一擴(kuò)充的可靠性和完全性。對此，本文將使用句法翻譯的方法（[8]）證明該擴(kuò)充相對于多主體信念庫語義的可靠性和完全性。

本文的各部分內(nèi)容安排：第2 節(jié)到第4 節(jié)是對[18]的回顧，在第2 節(jié)，我們定義了包含覺知的信念態(tài)度邏輯的邏輯語言；第3 節(jié)給出信念庫語義模型的定義，進(jìn)而規(guī)定不同的模型類；第4 節(jié)介紹了靜態(tài)信念態(tài)度邏輯的公理系統(tǒng)以及該系統(tǒng)中不同的公理集合對于相應(yīng)模型類的可靠性和完全性定理；從第5 節(jié)開始是本文的核心內(nèi)容，在介紹了該邏輯在增加個(gè)體更新動(dòng)態(tài)算子之后的擴(kuò)充后（[19]），我們用句法翻譯的方法證明了該擴(kuò)充對于信念庫語義模型的可靠性和完全性；第6節(jié)將信念態(tài)度邏輯的個(gè)體信念更新與命題覺知邏輯的個(gè)體信念更新作比較，展現(xiàn)了前者在保持模型簡潔性方面的優(yōu)勢，最后我們證明了這兩種動(dòng)態(tài)過程產(chǎn)生的模型具有互模擬關(guān)系；第7 節(jié)得出文章的結(jié)論并介紹后續(xù)工作。

2 邏輯語言

在這一節(jié)，我們回顧了包含覺知的信念態(tài)度邏輯LDAA（Logic of Doxastic Attitudes with Awareness，[18]）的語言。令A(yù)tm{p,q,...}是可數(shù)無限的原子命題集，令A(yù)gt{1,...,n}是有限的主體集。LDAA 的語言由下面兩層定義給出。首先是L0(Atm,Agt)：

其中p ∈Atm，i ∈Agt。LLDAA(Atm,Agt)是在L0(Atm,Agt)的基礎(chǔ)上增加隱信念算子得到的語言：

其中，α ∈L0(Atm,Agt)，i ∈Agt。

當(dāng)前后文明確時(shí)，可以將L0(Atm,Agt)簡寫為L0，將LLDAA(Atm,Agt)簡寫為LLDAA。其他布爾連接詞∨,→,?,?,⊥則是由?和∧通過標(biāo)準(zhǔn)的方式定義。公式△iα讀作“主體i顯相信α為真”，公式○iα讀作“主體i覺知到α”。算子△i可以被疊加，這說明LLDAA可以表達(dá)高階信念，例如△i△jα，讀作“主體i顯相信主體j顯相信α為真”。疊加可能是顯信念算子和覺知算子的混合，例如△i ○jα，讀作“主體i顯相信主體j覺知到α”。

公式□iφ讀作“主體i隱相信φ為真”。它的對偶?i定義為：

?iφ讀作“φ與主體i的顯信念有一致性”。

值得注意的是，模態(tài)詞○i在邏輯語言的兩層定義中都有出現(xiàn)，而模態(tài)詞△i只出現(xiàn)在第一層。因此，覺知算子可以出現(xiàn)在顯信念算子的轄域中，而隱信念算子不能出現(xiàn)在顯信念算子的轄域中2這里對句法做出限制的原因是，在下一節(jié)的語義定義中，主體的信念可通達(dá)關(guān)系是由該主體的顯信念計(jì)算出的，也就是說，隱信念是通過顯信念來定義的。因此，如果隱信念算子出現(xiàn)在顯信念算子的轄域中，將會產(chǎn)生循環(huán)定義的問題。規(guī)避這一問題方式是用“固定點(diǎn)”的方式來定義隱信念，而這會顯著增加語義的復(fù)雜性。。另外，顯信念算子和隱信念算子都能出現(xiàn)在覺知算子的轄域中。這是因?yàn)?，本文研究的覺知是命題覺知，即關(guān)于原子命題的覺知，其含義是，主體覺知到某一公式等價(jià)于覺知到構(gòu)成該公式的所有原子命題。令A(yù)tm(φ)表示出現(xiàn)在公式φ中的原子命題的集合，其遞歸定義如下：

令Γ?LLDAA是有限的公式集，定義Atm(Γ)∪

φ∈ΓAtm(φ)。

3 形式語義

這一部分回顧了包含覺知的信念庫語義。（[18]）不同于克里普克語義的是，信念庫語義中的可通達(dá)關(guān)系不是模型的初始條件，而是從信念庫中計(jì)算得出的。這里首先給出“狀態(tài)”的定義，它類似于克里普克語義中的可能世界。

定義1.一個(gè)狀態(tài)是一個(gè)多元組S(B1,...,Bn,A1,...,An,V)，其中，

?Bi ?L0是主體i的信念庫，其中，i ∈Agt，

?AiAtm(Bi)是主體i的覺知集合，其中，i ∈Agt，

?V ?Atm是該狀態(tài)中那些為真的原子命題集。

S 是所有狀態(tài)的集合。下面的定義給出L0公式的語義解釋。

定義2.對任意S(B1,...,Bn,A1,...,An,V)∈S：

定義3.包含覺知的多主體信念庫語義模型MABA（Multi-agent Belief Model with Awareness）是一個(gè)二元組(S,Cxt)，其中，S ∈S，Cxt ?S。

Cxt是所有主體的語境或共同背景（Common Ground，[25]），指的是所有主體共同分享的信息。從這些信息和各自的顯信念中，主體能夠做出推理。下面的定義規(guī)定了主體的信念可通達(dá)關(guān)系是由信念庫計(jì)算出的。

定義4.對任意i ∈Agt，Ri是S 上的二元關(guān)系，其定義為：對任意S(B1,...,Bn,A1,...,An,V),S′

在定義了可通達(dá)關(guān)系的基礎(chǔ)上，可以給出LLDAA公式的語義解釋。其中，布爾公式與標(biāo)準(zhǔn)的定義保持一致，此處省略。

定義5.令(S,Cxt)是MABA，其中，S(B1,...,Bn,A1,...,An,V)。有如下等價(jià)關(guān)系：

下面兩個(gè)定義給出了MABA 的屬性，它們分別對應(yīng)克里普克模型的自返性和持續(xù)性。

定義6.MABA(S,Cxt)滿足全局可持續(xù)性GC（Global Consistency）當(dāng)且僅當(dāng)，對于所有i ∈Agt和所有S′ ∈({S}∪Cxt)，存在S′′ ∈Cxt滿足(S′,S′′)∈Ri。

定義7.MABA(S,Cxt)滿足信念正確BC（Belief Correctness）當(dāng)且僅當(dāng)S ∈Cxt且對于所有i ∈Agt和所有S′ ∈Cxt，(S′,S′)∈Ri。

對于X?{GC,BC}，MABAX是滿足X 中的所有條件的MABA 模型類。MABA?是所有MABA 模型構(gòu)成的模型類，簡記為MABA。很容易證明MABA{BC}MABA{GC,BC}。

令φ ∈LLDAA，φ對于MABAX模型類有效，當(dāng)且僅當(dāng)，對所有(S,Cxt)∈MABAX，(S,Cxt)|φ，簡記為φ。φ對于MABAX模型類可滿足，當(dāng)且僅當(dāng)，?φ對于MABAX模型類不是有效的。

4 公理化

這一部分首先給出LDAA 邏輯對于不同模型類的公理集，然后介紹它們關(guān)于相應(yīng)模型類的可靠性和完全性定理及證明思路。

基本的LDAA 邏輯是在經(jīng)典命題邏輯的基礎(chǔ)上增加以下公理和推理規(guī)則的擴(kuò)充（[18]）：

對于X?令LDAAX是LDAA 邏輯增加下述公理的擴(kuò)充：

對于邏輯LDAAX，X?，其中任意公式φ ∈LLDAA，用φ來表示φ是LDAAX的定理。對于LLDAA的公式集Γ，如果不存在公式φ1,...,φm ∈Γ滿足(φ1∧...∧φm)→⊥，則Γ 與LDAAX一致。特別地，φ與LDAAX一致當(dāng)且僅當(dāng){φ}與LDAAX一致。

接下來將介紹可靠性和完全性定理，由于其證明過程較長，這里只闡述[18]的證明思路?？煽啃缘淖C明比較簡單，只需要驗(yàn)證每一個(gè)公理對于相應(yīng)的模型類有效，每一個(gè)推理規(guī)則都能保持公式的有效性。對于完全性的證明，需要定義典范模型，而典范模型的定義需要克里普克語義結(jié)構(gòu)，因此，需要給出LDAA 的兩種類似克里普克結(jié)構(gòu)的語義模型，它們被稱為概念語義和準(zhǔn)概念語義，在這兩種語義中，可通達(dá)關(guān)系是模型的初始條件，然后只需證明信念庫語義與這兩種語義具有等價(jià)性。接下來只需要用典范模型的方法證明LDAAX對于具有相應(yīng)性質(zhì)的準(zhǔn)概念模型具有完全性，即可得出完全性定理。

定理1.令X?。LDAAX對于模型類是可靠和完全的。（[18]）

證明.過程參見[18]的第三節(jié)和第四節(jié)。

5 LDAA 的個(gè)體信念更新

這一部分首先給出LDAA 在增加個(gè)體信念更新算子之后的擴(kuò)充。（[19]）具體來說，在LLDAA(Atm,Agt)的基礎(chǔ)上增加算子[+iα]，可以得到語言LLDAA-PBE(Atm,Agt)：

其中，i ∈Agt，α ∈L0，LDAA-PBE 讀作“包含覺知與個(gè)體信念擴(kuò)張的信念態(tài)度邏輯”，PBE 是Private Belief Expansion 的簡寫。

與第2 節(jié)類似，LLDAA-PBE(Atm,Agt)可被記作LLDAA-PBE。公式[+iα]φ讀作“主體i的信念庫增加α后，φ為真”。在定義5 的基礎(chǔ)上增加如下可滿足關(guān)系的定義，動(dòng)態(tài)算子[+iα]可在MABA 中得到解釋。

定義8.令(S,Cxt)是MABA，其中S(B1,...,Bn,A1,...,An,V)。有如下等價(jià)關(guān)系：

事件+iα只包含主體i得到信息α并將α增加到其信念庫中，而其他主體的信念庫保持不變。因?yàn)橛X知集合是由信念庫計(jì)算得出的，所以，在這一過程中，主體i的覺知集合間接地受到影響。

另外，個(gè)體信念更新不能保持模型的信念正確BC 或全局可持續(xù)性GC，因此，對個(gè)體信念更新的討論是相對于所有MABA 構(gòu)成的模型類MABA。

邏輯LDAA-PBE 在LDAA 的基礎(chǔ)上增加如下公理和推理規(guī)則的擴(kuò)充3注意到，LDAA-PBE 中并不包含個(gè)體更新算子疊加的公理，即對應(yīng)定義9 第13 項(xiàng)的公理。其原因是，證明LDAA-PBE 的完全性并不是直接通過LDAA-PBE 的公理，而是利用定義9 的歸約函數(shù)將所有LDAA-PBE 公式轉(zhuǎn)化為LDAA 公式。LDAA-PBE 新增加的六條公理已經(jīng)能夠確保該歸約函數(shù)可以將所有的LDAA-PBE 轉(zhuǎn)化為LDAA公式。：

任意公式φ ∈LLDAA-PBE，用?LDAA-PBEφ來表示φ是LDAA-PBE 的定理。根據(jù)上述公理，可以給出歸約函數(shù)redLDAA-PBE的遞歸定義，該函數(shù)將LLDAA-PBE的公式可以轉(zhuǎn)化為等價(jià)的LLDAA公式。

定義9.函數(shù)redLDAA-PBE遞歸定義如下：

覺知的歸約公式的意思是：通過將α增加到信念庫中，主體i將出現(xiàn)在α的原子命題增加到他的覺知集合中；隱信念的歸約公式的意思是，主體i在信念庫中增加α后能夠推出φ，當(dāng)且僅當(dāng)，在信念更新之前，主體i就能夠推出α蘊(yùn)涵φ；顯信念的歸約公式的意思是，主體i的信念庫增加α，其他主體的信念庫保持不變。

接下來，我們對[19]的內(nèi)容做補(bǔ)充，證明LDAA-PBE 相對于MABA 的可靠性和完全性。在證明可靠性和完全性之前，需要首先說明上述歸約函數(shù)redLDAA-PBE給出的等價(jià)式是LDAA-PBE 的定理，即，對于所有的φ ∈LLDAA-PBE，有?φ ?redLDAA-PBE(φ)。這里存在一個(gè)問題，在做歸納證明時(shí)，通常需要將歸納假設(shè)應(yīng)用在某一公式的所有子公式上，但是，對于包含個(gè)體信念更新算子的公式，這一方法是不夠的。例如，?[+iα]ψ并不是[+iα]?ψ的子公式。因此，需要定義如下的公式復(fù)雜度函數(shù)，然后針對公式復(fù)雜度來提出歸納假設(shè)。

定義10.公式復(fù)雜度函數(shù)c:LLDAA-PBE→N 的定義如下：

公式復(fù)雜度函數(shù)c最后一項(xiàng)的參數(shù)2 并不是任意的，它是保證下面的不等式成立的最小自然數(shù)。

引理1.對于所有α,β ∈L0，以及所有φ,ψ,ψ1,ψ2∈LLDAA-PBE，

證明.只需要逐項(xiàng)驗(yàn)證這些不等式成立即可。

上述不等式說明被歸約前的公式的復(fù)雜度大于歸約得到的公式的復(fù)雜度4需要注意的是，引理1 省略了歸約函數(shù)redLDAA-PBE 中那些不等關(guān)系顯然成立的部分。。有了這一結(jié)果，我們可以對公式復(fù)雜度做數(shù)學(xué)歸納來證明下面的命題。

命題1.令φ ∈LLDAA-PBE?？梢缘玫剑?/p>

證明.對c(φ)做歸納：

當(dāng)φ是原子命題p時(shí)，?LDAA-PBEp ?p顯然成立。

假設(shè)對于所有c(φ)≤n的φ，有?LDAA-PBEφ ?redLDAA-PBE(φ)，其中，n ∈N。

當(dāng)φ的形式如?ψ、ψ1∧ψ2、△iα、□iψ、○iψ時(shí)，結(jié)論可從歸納假設(shè)和引理1 的第一項(xiàng)得證。

當(dāng)φ是[+iα]p時(shí)，結(jié)論可從公理AI、歸納假設(shè)、定義10 得證。

當(dāng)φ是[+iα]?φ時(shí)，結(jié)論可從公理PE&N、歸納假設(shè)、引理1 的第2 項(xiàng)得證。

當(dāng)φ是[+iα](φ1∧φ2)時(shí)，結(jié)論可從公理PE&C、歸納假設(shè)、引理1 的第3項(xiàng)得證。

當(dāng)φ是[+iα]□jφ時(shí)，其中ij，結(jié)論可從公理PE&IB、歸納假設(shè)、引理1 的第4 項(xiàng)得證。

當(dāng)φ是[+iα]□iφ時(shí)，結(jié)論可從公理PE&IB、歸納假設(shè)、定義10 得證。

當(dāng)φ是[+iα]△jβ時(shí)，結(jié)論可從公理PE&EB、歸納假設(shè)、定義10 得證。

當(dāng)φ是[+iα]○jφ時(shí)，其中，ij或Atm(φ)?Atm，結(jié)論可從公理PE&A、歸納假設(shè)、定義10 得證。

當(dāng)φ是[+iα]○jφ且并非是前一種情況時(shí)，結(jié)論可從公理PE&A、歸納假設(shè)、引理1 的第5 項(xiàng)得證。

當(dāng)φ是[+iα][+jβ]φ時(shí)，由redLDAA-PBE的定義，可轉(zhuǎn)化為上述情況。

下面的命題說明歸約函數(shù)redLDAA-PBE確實(shí)可以將LLDAA-PBE公式轉(zhuǎn)化為LLDAA公式。

命題2.令φ ∈LLDAA-PBE。則，redLDAA-PBE(φ)∈LLDAA。

證明.對c(φ)做歸納即可給出證明，此處省略具體步驟。

根據(jù)上述結(jié)果，我們可以證明LDAA-PBE 的可靠性和完全性定理。

定理2.LDAA-PBE 對于模型類MABA 是可靠和完全的。證明.對于可靠性，只需要驗(yàn)證每一個(gè)公理都是有效的，每一個(gè)推理規(guī)則都能在模型類MABA 保持有效性。因?yàn)長DAA 對于MABA 是可靠的，只需要驗(yàn)證新增的公理和推理規(guī)則，而其中大多數(shù)都是顯然的，這里只證明公理PE&A 是有效的。當(dāng)ij時(shí)，根據(jù)語義，[+iα]○jφ ?○jφ顯然成立。當(dāng)Atm(φ)?Atm(α)時(shí)，根據(jù)語義，△iα →○iφ是重言式。由此可得，[+iα](△iα →○iφ)是重言式。由前面的等價(jià)式可知，后者等價(jià)于[+iα]△iα →[+iα]○iφ。因?yàn)閇+iα]△iα ??，可以得到[+iα]○i φ ??。對于其他情況，由○iφ ?∧p∈Atm(φ)Atm(α)○ip ∧∧p∈Atm(φ)∩Atm(α)○ip可以得到[+iα]○iφ ?[+iα]∧p∈Atm(φ)Atm(α)○ip ∧[+iα]∧p∈Atm(φ)∩Atm(α)○ip。根據(jù)前一種情況，很容易得出[+iα]∧p∈Atm(φ)∩Atm(α)○ip ??。因此，有[+iα]○iφ ?[+iα]∧p∈Atm(φ)Atm(α)○ip。因?yàn)閜∈Atm(α)，對p的覺知不受[+iα]事件的影響，可以得出，[+iα]○iφ ?∧p∈Atm(φ)Atm(α)○ip。對于完全性，令|MABAφ。根據(jù)LDAA-PBE 的可靠性以及?LDAA-PBEφ ?redLDAA-PBE(φ)，可得|MABAredLDAA-PBE(φ)。因?yàn)閞edLDAA-PBE(φ)不包含任何動(dòng)態(tài)算子，所以，由LDAA 的完全性可得，?LDAAredLDAA-PBE(φ)。由于LDAA 是LDAA-PBE的子系統(tǒng)，可以得到?LDAA-PBEredLDAA-PBE(φ)。根據(jù)命題1，有?LDAA-PBEφ。

6 LDAA-PBE 與命題覺知邏輯的個(gè)體信念更新

在這一部分，我們將針對個(gè)體信念更新的問題比較LDAA-PBE 與命題覺知邏輯LPA（Logic of Propositional Awareness），后者首先出現(xiàn)在[10]，是一般覺知邏輯LGA（Logic of General Awareness，[9]）的特殊情況。

LPA 的語言LLPA(Atm,Agt)由下面的語法給出：

其中，p ∈Atm，i ∈Agt。公式Biφ讀作“主體i隱相信φ為真”，公式Aiφ讀作“主體i覺知到φ”，公式Xiφ讀作“主體i顯相信φ為真”。與前文一致，其他布爾連接詞∨,→,?,?,⊥由?和∧通過標(biāo)準(zhǔn)的方式定義，LLPA(Atm,Agt)簡寫為LLPA。在語義層面，只需要將LGA 的語義模型的覺知函數(shù)的取值設(shè)定為原子命題集的冪集，就可以得到LPA 的語義模型。

定義11.命題覺知模型PAM（Propositional Awareness Model）是一個(gè)四元組M(Ω,?,ρ,π)，其中，

? Ω 是非空的可能世界集，

??:Agt×Ω?→2Ω是信念可通達(dá)函數(shù)，

?ρ:Agt×Ω?→2Atm是命題覺知函數(shù)，

?π:Atm ?→2Ω是賦值函數(shù)。

PAM 是所有PAM 構(gòu)成的集合。對于PAMM(Ω,?,ρ,π)及s ∈Ω，二元組(M,s)被稱為PAM 的點(diǎn)模型。t ∈?(i,s)可記作s ?i t。下面給出LLPA的公式相對于PAM 的點(diǎn)模型的語義解釋。

定義12.給定PAMM(Ω,?,ρ,π)及可能世界s ∈Ω，對于LLPA的公式，有如下等價(jià)關(guān)系：

對比LPA 和LDAA 的定義，可以看出這兩種邏輯是基于不同的哲學(xué)出發(fā)點(diǎn)。在LPA 的語義中，主體的信念可通達(dá)關(guān)系和覺知集合都是模型的初始條件，而主體的顯信念是由這兩個(gè)條件計(jì)算得出的；而在LDAA 的語義中，模型唯一的初始條件是主體的顯信念，而隱信念和覺知都是由顯信念計(jì)算得出的。由此可見，LDAA減少了理論的前提假設(shè)，更符合奧卡姆剃刀的原則。另外，這兩種邏輯刻畫了不同意義的顯信念概念。在下面給出的翻譯函數(shù)中也能看出這種差異，LPA 的顯信念并沒有直接對應(yīng)LDAA 的顯信念，而是對應(yīng)LDAA 的隱信念和覺知的合取。實(shí)際上，LDAA 的顯信念表示當(dāng)前活躍在主體認(rèn)知中的信念，即工作記憶中的信念（主體的信念庫即該主體的工作記憶）；而LPA 的顯信念表示，在主體覺知到的原子命題構(gòu)成的信念中，該主體相信為真的那些信念，這樣的信念并不一定處在工作記憶中，但是能被主體所理解。值得重視的是，[18]建立了由LPA 到LDAA 的多項(xiàng)式嵌入，這說明后者以更少的前提假設(shè)提供了更強(qiáng)的表達(dá)力。

接下來，為了證明互模擬定理，需要定義LLPA和LLDAA之間的翻譯函數(shù)：

需要注意的是tr←并不是tr的反函數(shù)，因?yàn)樾枰趖r←中給出△i算子的翻譯，而tr不會涉及到△i算子。實(shí)際上，tr←是一個(gè)偏函數(shù)，其自變量如果是顯信念的否定式，它的函數(shù)值為空。這樣做的原因是，如果將LDAA 的顯信念的否定直接翻譯成LPA 的顯信念否定，有可能會產(chǎn)生矛盾。根據(jù)[17]，LDAA 的顯信念表示主體的工作記憶，所以有可能α不在主體i的工作記憶中，但□iα ∧○iα為真。

以PAM 為基礎(chǔ)，范·迪特瑪希（van Ditmarsch）等人刻畫了信念和命題覺知的動(dòng)態(tài)變化（[3-5,7]），其中，個(gè)體層面的動(dòng)態(tài)在[5]得到研究，其方法是使用行動(dòng)模型（[2,15]）。它存在的問題是，在一系列個(gè)體信念更新的操作之后，通過與行動(dòng)模型做乘積計(jì)算得出的PAM 會呈現(xiàn)幾何級數(shù)增長。為解決這一問題，在羅里尼提出的信念態(tài)度邏輯中（[17]），初始的信念庫模型經(jīng)過一系列個(gè)體信念更新之后，其數(shù)量級只會發(fā)生相對于信念更新次數(shù)的線性增長。然而，羅里尼只給出了以信念庫語義模型為基礎(chǔ)的個(gè)體信念更新過程，且不包含覺知。為應(yīng)對這一問題，接下來，我們將以PAM 作為初始模型得出互模擬的結(jié)論，其中同時(shí)包含覺知的變化。

[18]的第3 節(jié)給出了LDAA 的三種語義對于一個(gè)有限公式集成立，而將PAM轉(zhuǎn)換為MABA 也需要利用這個(gè)語義等價(jià)性的結(jié)論，因此，這里我們也只考慮LLDAA的有限公式集。

信念庫模型的個(gè)體信念更新

令M(Ω,?,ρ,π)是PAM（Ω 有可能是無限集），Σ?LLPA是對子公式封閉的公式集，tr(Σ){tr(φ):φ ∈Σ}。為了證明的方便，令Σ′Σ∪{Aip:p ∈Σ,i ∈Agt}。很顯然，tr(Σ′)?LLDAA是一個(gè)有限集，且對子公式封閉。

根據(jù)[18] 的定理3 和第3 節(jié)的語義等價(jià)性證明，可以找到一個(gè)有限集Cxt和一個(gè)滿射σ:Ω→Cxt滿足，對每一個(gè)s ∈Ω，如果σ(s)S，其中S(B1,...,Bn,A1,...,An,V)，那么，

? 對每一個(gè)p ∈Σ′：tr(p)∈V當(dāng)且僅當(dāng)s ∈π(p)，

? 對每一個(gè)Bi和每一個(gè)p ∈Σ′：tr(p)∈Atm(Bi)當(dāng)且僅當(dāng)p ∈ρ(i,s)∩Σ′5這一項(xiàng)解釋了為什么我們令Σ′包括{Aip : p ∈Σ,i ∈Agt}。如果不這樣做，對模型的過濾就不能保證主體i 在某一信念庫的覺知集合與Σ 和主體i 在PAM 的相應(yīng)可能世界的覺知集合的交集相等。為了證明互模擬關(guān)系，需要保證覺知集合在Σ 的限定內(nèi)是不變的。，

? 對每一個(gè)Ai：AiAtm(Bi)，

? 對每一個(gè)t ∈Ω：如果s ?i t，那么(S,σ(t))∈Ri，

? 對每一個(gè)S′ ∈Cxt:如果(S,S′)∈Ri，那么存在t ∈?(i,s)滿足S′σ(t)。

很容易驗(yàn)證，對于每一個(gè)S ∈Cxt，(S,Cxt)是MABA，對每一個(gè)φ ∈Σ′和每一個(gè)s ∈Ω，(M,s)當(dāng)且僅當(dāng)(σ(s),Cxt)(φ)。

接下來對(S,Cxt)應(yīng)用個(gè)體信念更新。假設(shè)主體i的信念庫增加了α，其中，α ∈L0(Atm(tr(Σ′),Agt)，tr←(△iα)∈Σ′。然后，根據(jù)定義8，可以得到(S+iα,Cxt)。

為了證明互模擬關(guān)系，需要將(S+iα,Cxt)翻譯回PAMM′(Ω′,?′,ρ′,π′)：

? 對每一個(gè)i ∈Agt和每一個(gè)sS′ ∈Ω′：

? 對每一個(gè)i ∈Agt和每一個(gè)sS′ ∈Ω′:ρ′(i,sS′)A′,

? 對每一個(gè)p ∈Atm(Σ′):π′(p){sS′ ∈Ω′:p ∈V ′}。

PAM 的個(gè)體信念更新

與前一部分相類似，我們用過濾的方法將M(Ω,?,ρ,π) 轉(zhuǎn)換成有限的PAMMΣ′(ΩΣ′,?Σ′,ρΣ′,πΣ′)。由庫伊和雷恩（Kooi&Renne，[15]）提出的箭頭更新模型（Arrow Update Model），這里定義該模型相對于PAM 的形式。

定義13.一個(gè)箭頭更新模型是一個(gè)三元組U{O,τ,A}，其中，

? O 是非空的輸出集，其中每一個(gè)元素被稱為一個(gè)輸出，

?τ:Agt×O×O→LLPA×LLPA是一個(gè)偏函數(shù)，

?A:Agt×O→2Atm是覺知變化函數(shù)。

為了表達(dá)上的方便，對每一個(gè)i ∈Agt和每一個(gè)o′,o′′ ∈O，如果τ(i,o′,o′′)(φ,ψ)，用τ1(i,o′,o′′)來表示φ，用τ2(i,o′,o′′)來表示ψ。

箭頭更新模型(U,o)作用于PAM 點(diǎn)模型(M,s)之后，產(chǎn)生一個(gè)新的PAM 點(diǎn)模型，我們稱之為乘積模型。下面是乘積模型的定義。

定義14.令(U,o)是一個(gè)箭頭更新模型，其中，U{O,τ,A}。令(M,s)是一個(gè)PAM 點(diǎn)模型，其中，M(Ω,?,ρ,π)。(U,o)作用于(M,s)產(chǎn)生的乘積模型是(M ?U,(s,o))，其中，M ?U(Ω′,?′,ρ′,π′)：

箭頭更新模型以|O|為倍數(shù)增大了初始模型。具體來說，對每一個(gè)輸出o′ ∈O和PAM 的每一個(gè)可能世界s′，會產(chǎn)生s′的一個(gè)增加了下標(biāo)o′的復(fù)制(s′,o′)。而且，對每一個(gè)i ∈Agt和每一個(gè)輸出對(o′,o′′)，箭頭更新模型指定了起始條件τ1(i,o′,o′′)和目標(biāo)條件τ2(i,o′,o′′)，它們分別被s′和s′′滿足，進(jìn)而保證在乘積模型中，(s′,o′)和(s′′,o′′)具有i-可通達(dá)關(guān)系。這樣規(guī)定使得，可通達(dá)關(guān)系在乘積模型中被保留的充分必要條件為相應(yīng)的兩個(gè)初始可能世界對應(yīng)于該輸出分別滿足起始條件和目標(biāo)條件。A函數(shù)的功能是擴(kuò)大主體的覺知集合。具體來說，它將每一個(gè)主體和每一個(gè)輸出對應(yīng)一個(gè)原子命題集，在乘積模型中，這一原子命題集將是該主體在被該輸出下標(biāo)的可能世界的覺知集合的子集。直觀上講，這意味著在乘積模型中，主體的覺知集合因?yàn)樵黾恿艘恍┰用}作為元素而被擴(kuò)大。

為了刻畫在其他主體的信念不變的情況下某一主體的信念更新，需要定義一個(gè)特殊的箭頭更新模型——個(gè)體箭頭更新模型（Private Arrow Update Model）。它只包含兩個(gè)輸出：o1和o2。對于輸出o1，他的覺知集合在每一個(gè)可能世界都會擴(kuò)大，而在φ為真的可能世界，主體i減少他的可通達(dá)世界；對于輸出o2，沒有任何事發(fā)生。

定義15.對于主體i、公式φ、覺知擴(kuò)張集合AE ?Atm，其中Atm(φ)?AE，相應(yīng)的個(gè)體更新模型是U(φ,AE)i(O,τ,A)，定義如下：

? 對于每一個(gè)k,h ∈{1,2}和每一個(gè)j ∈Agt，τ(j,ok,oh) 有定義當(dāng)且僅當(dāng)（k1 且h2）或kh2，

?τ(i,o1,o2)(?,φ)且τ(i,o2,o2)(?,?)，

? 對所有ji，τ(j,o1,o2)(?,?)且τ(j,o2,o2)(?,?)，

? 如果ij且k1，A(j,ok)AE，

否則，A(j,ok)?。

令U(tr←(α),Atm(α))i(O,τ,A) 是對于主體i、公式tr←(α)、覺知擴(kuò)張集合Atm(α)的個(gè)體箭頭更新模型。給定PAM 點(diǎn)模型(M,s)，其中M(Ω,?,ρ,π),M ?U(tr←(α),Atm(α))i,(s,o1))是(M,s)和(U(tr←(α),Atm(α))i,o1)的乘積模型。具體來說，PAMM ?U(tr←(α),Atm(α))i(Ω′,?′,ρ′,π′)的定義如下：

? Ω′{(s′,o1):s′ ∈Ω}∪{(s′,o2):s′ ∈Ω}，

? 對所有s′ ∈Ω 和所有j ∈Agt：

? 對所有p ∈Atm：

在下文中，將(M ?U(tr←(α),Atm(α))i,(s,o1))記作(M,s)(tr←(α),Atm(α))i。

互模擬

接下來我們證明兩種個(gè)體信念更新產(chǎn)生的模型具有互模擬關(guān)系。在此之前，有兩點(diǎn)需要注意。第一，互模擬關(guān)系應(yīng)該局限在原子命題集的一個(gè)有限子集內(nèi)；第二，與標(biāo)準(zhǔn)的克里普克模型的互模擬不同，這里的互模擬關(guān)系應(yīng)該將模型中的覺知函數(shù)考慮在內(nèi)。范·迪特瑪希等人提供了包含覺知的互模擬定義（[6]），在他們的文章中，這一互模擬被稱為標(biāo)準(zhǔn)互模擬。

定義16.令Q?Atm，給定兩個(gè)PAMM(Ω,?,ρ,π)和M′(Ω′,?′,ρ′,π′)，這兩個(gè)模型的Q 標(biāo)準(zhǔn)互模擬是關(guān)系R(Q)?Ω×Ω′滿足，對每一個(gè)(s,s′)∈R(Q)，每一個(gè)i ∈Agt，和每一個(gè)p ∈Q：

? 原子命題：s ∈π(p)當(dāng)且僅當(dāng)s′ ∈π′(p)，

? 覺知：Q∩ρ(i,s)Q∩ρ′(i,s′)，

? 正向條件：如果s ?i t，那么存在t′ ∈?′(i,s′)滿足(t,t′)∈R(Q)，

? 反向條件：如果s′ ?i t′，那么存在t ∈?(i,s)滿足(t,t′)∈R(Q)。

對于兩個(gè)PAM 點(diǎn)模型(M,s)和(M′,s′)，其中M(Ω,?,ρ,π)，M′(Ω′,?′,ρ′,π′)，如果存在互模擬關(guān)系R(Q)，且(s,s′)∈R(Q)，則這兩個(gè)點(diǎn)模型有Q 互模擬關(guān)系，記做(M,s)Q(M′,s′)。

根據(jù)[6]的命題21，可以得到，如果(M,s)Q(M′,s′)，那么(M,s)和(M′,s′)滿足LLPA(Q,Agt)中的相同的公式。

下面的定理是這一部分的核心結(jié)論，這一互模擬關(guān)系的左右兩邊各是一個(gè)PAM 點(diǎn)模型，其中，左邊的模型是通過信念庫語義的個(gè)體信念更新得到的，右邊的模型是通過個(gè)體箭頭更新模型得到的。

定理3.(M′,sS+iα)Atm(Σ)(MΣ′,[s]Σ′)(tr←(α),Atm(α))i

證明.令M′(Ω′,?′,ρ′,π′)，將M ?U(tr←(α),Atm(α))i記做M′′，令M′′(Ω′′,?′′,ρ′′,π′′)，令初始PAMM(Ω,?,ρ,π)。很容易得到：

定義二元關(guān)系R(Atm(Σ))?Ω′×Ω′′如下：

用常規(guī)的方式就可以驗(yàn)證R(Atm(Σ)) 定義了M′和M′′的標(biāo)準(zhǔn)互模擬關(guān)系，因此，具有互模擬關(guān)系。

值得注意的是，定理3 的成立需要滿足四個(gè)條件：第一，具有互模擬關(guān)系的兩個(gè)模型都是有限模型，因此，需要將初始模型用對子公式封閉的公式集來過濾得到有限模型；第二，過濾時(shí)，對子公式封閉的公式集Σ 需要轉(zhuǎn)化為Σ′，從而包括所有主體對Σ 的原子命題的覺知命題；第三，如果α是主體i的信念庫中增加的公式，那么，tr←(△iα)是Σ′中的公式；最后，α是L0公式。

在證明過程中，定理3 與[17]的定理11 使用的方法有一些相同點(diǎn)和不同點(diǎn)。相同點(diǎn)是，在模型的動(dòng)態(tài)變化過程中，兩者都使用了信念庫的更新和個(gè)體箭頭更新模型。不同點(diǎn)是，前者以PAM 作為證明的起始模型，而后者以信念庫語義模型作為證明的起始模型，基于[18]的由LPA 到LDAA 的多項(xiàng)式嵌入，以PAM 作為證明的起始模型允許我們將LDAA 的技術(shù)直接應(yīng)用在LPA 上；由于證明的起始模型的不同，兩者在證明過程中需要對模型做不同的處理，前者需要將模型過濾以得到有限模型，進(jìn)而通過[18]的模型轉(zhuǎn)化方法得到MABA，而后者則是將所有顯信念公式作為原子命題來處理，進(jìn)而從信念庫語義模型得到克里普克模型；最重要的是，相比于后者，前者的模型中包含覺知，因此，定義14 給出的個(gè)體箭頭更新模型的最后一項(xiàng)是對主體覺知的更新，定義16 提出了互模擬需要滿足覺知相等的條件。

更進(jìn)一步，定理3 為LDAA 和LPA 的語義在技術(shù)方面和哲學(xué)方面的差異提供了很好的說明。技術(shù)方面，在LPA 的語義模型PAM 中，需要通過主體的信念可通達(dá)關(guān)系來確認(rèn)該主體的隱信念，而顯信念又是通過隱信念和覺知計(jì)算出的，因此，主體的個(gè)體信念更新意味著需要為每一個(gè)這樣的主體復(fù)制整個(gè)模型；反觀LDAA的語義模型MABA，每個(gè)主體的信念庫都是相互獨(dú)立的，認(rèn)知模型是從主體的信念庫構(gòu)造出來的，這意味著，當(dāng)某一主體的顯信念發(fā)生變化時(shí)，認(rèn)知模型也會自動(dòng)發(fā)生變化。哲學(xué)方面，對于PAM，隱信念和覺知都是模型的初始條件，因此，為實(shí)現(xiàn)主體顯信念的更新，需要同時(shí)改變主體的隱信念和覺知；而MABA 與之不同，我們只需要更新主體信念庫中的公式集即可實(shí)現(xiàn)該主體的顯信念更新。

圖2：圖表展示了以PAM 為初始模型的兩種個(gè)體信念更新方案的關(guān)系。其中，PBE 指信念庫的個(gè)體信念更新，PAU 指個(gè)體箭頭更新。

圖3：這是用個(gè)體箭頭更新過程來展示例1 的模型變化過程。圖中有兩個(gè)單主體模型。左邊的模型是信念更新之前小張的認(rèn)知狀態(tài)，右邊的模型信念更新之后的認(rèn)知狀態(tài)。大括號中的原子命題表示小張?jiān)谠摽赡苁澜绲挠X知集合，模型中其他元素的解釋與圖1 保持一致。

圖4：這是用信念庫語義模型的個(gè)體信念更新過程來展示例1 的模型變化過程。大括號中的公式表示小張信念庫中的公式，圖中的其他元素的含義與圖1 保持一致。

圖2 展示了這一節(jié)的完整過程。通過本節(jié)我們證明了，盡管LPA 的顯信念算子Xi被翻譯成LDAA 的□i和○i算子，針對△i算子的個(gè)體信念更新仍然可以用在基于PAM 的動(dòng)態(tài)變化中?；氐轿恼麻_頭提出的例子，圖3 和圖4 分別展示了這兩種信念更新的模型變化過程。很容易看出，基于信念庫語義模型的個(gè)體信念更新大大簡化了模型的轉(zhuǎn)化過程，避免了模型的復(fù)制。

7 結(jié)論與后續(xù)工作

本文證明了以信念庫語義為基礎(chǔ)的個(gè)體信念更新的動(dòng)態(tài)邏輯LDAA-PBE 相對于多主體信念庫語義的可靠性和完全性。同時(shí)，本文將兩種個(gè)體信念更新方案做比較，它們分別是：基于信念庫語義的個(gè)體信念更新、基于克里普克語義的個(gè)體箭頭更新。通過模型轉(zhuǎn)換的方法，我們證明了這兩種方案形成的模型具有互模擬關(guān)系。其中，前一種方案只會使模型的規(guī)模發(fā)生線性增加，而后一種方案在每次個(gè)體信念更新時(shí)都必須復(fù)制模型，從而在一系列更新之后會使模型規(guī)模產(chǎn)生幾何級數(shù)增加。這說明前一種方案在達(dá)到相同目的的同時(shí)，能夠有效保持模型的簡潔性。

在后續(xù)工作中，我們不僅會考慮對原子命題的覺知，也會研究某一主體對其他主體的覺知，嘗試以信念庫語義為基礎(chǔ)建立關(guān)于身份的覺知邏輯，而關(guān)于這一覺知的動(dòng)態(tài)變化也會納入該邏輯的討論范圍。