覺知邏輯的個體信念更新

宋鵬飛 熊衛

1 引言

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

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

圖1 是兩個單主體模型。左邊的模型表示小張得到信息之前的認知狀態，其中只包含一個原子命題p，實心點是p為真的可能世界，空心點是p為假的可能世界，有下劃線的可能世界是當前的可能世界，模型中的箭頭表示主體的可通達關系，顯然它是等價關系；右邊的模型表示小張得到信息之后的認知狀態，其中包含兩個原子命題p和q，每個可能世界有兩個點，左邊的點表示p的真值，右邊的點表示q的真值，實心為真，空心為假，與左側模型一樣，有下劃線的可能世界為當前可能世界，箭頭表示主體的可通達關系，它也是等價關系。

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

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

由于上述兩種方案都是在克里普克語義上加以擴展，因此，在處理個體信念更新的問題時，都會產生同樣的問題，即，當某一主體接收到某一條信息，原本的認知模型需要被復制成兩個副本，一個副本用來刻畫接收到信息的主體的認知狀態，另一個副本用來刻畫未接收到信息的主體的認知狀態。這樣做的結果是，在一系列個體信念更新之后，認知模型會發生幾何級數的增長。

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

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

2 邏輯語言

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

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

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

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

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

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

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

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

φ∈ΓAtm(φ)。

3 形式語義

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

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

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

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

?V ?Atm是該狀態中那些為真的原子命題集。

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

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

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

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

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

在定義了可通達關系的基礎上，可以給出LLDAA公式的語義解釋。其中，布爾公式與標準的定義保持一致，此處省略。

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

下面兩個定義給出了MABA 的屬性，它們分別對應克里普克模型的自返性和持續性。

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

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

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

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

4 公理化

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

基本的LDAA 邏輯是在經典命題邏輯的基礎上增加以下公理和推理規則的擴充（[18]）：

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

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

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

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

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

5 LDAA 的個體信念更新

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

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

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

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

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

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

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

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

定義9.函數redLDAA-PBE遞歸定義如下：

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

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

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

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

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

證明.只需要逐項驗證這些不等式成立即可。

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

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

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

當φ是原子命題p時，?LDAA-PBEp ?p顯然成立。

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

當φ的形式如?ψ、ψ1∧ψ2、△iα、□iψ、○iψ時，結論可從歸納假設和引理1 的第一項得證。

當φ是[+iα]p時，結論可從公理AI、歸納假設、定義10 得證。

當φ是[+iα]?φ時，結論可從公理PE&N、歸納假設、引理1 的第2 項得證。

當φ是[+iα](φ1∧φ2)時，結論可從公理PE&C、歸納假設、引理1 的第3項得證。

當φ是[+iα]□jφ時，其中ij，結論可從公理PE&IB、歸納假設、引理1 的第4 項得證。

當φ是[+iα]□iφ時，結論可從公理PE&IB、歸納假設、定義10 得證。

當φ是[+iα]△jβ時，結論可從公理PE&EB、歸納假設、定義10 得證。

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

當φ是[+iα]○jφ且并非是前一種情況時，結論可從公理PE&A、歸納假設、引理1 的第5 項得證。

當φ是[+iα][+jβ]φ時，由redLDAA-PBE的定義，可轉化為上述情況。

下面的命題說明歸約函數redLDAA-PBE確實可以將LLDAA-PBE公式轉化為LLDAA公式。

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

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

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

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

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

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

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

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

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

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

??:Agt×Ω?→2Ω是信念可通達函數，

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

?π:Atm ?→2Ω是賦值函數。

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

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

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

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

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

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

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

信念庫模型的個體信念更新

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

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

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

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

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

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

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

很容易驗證，對于每一個S ∈Cxt，(S,Cxt)是MABA，對每一個φ ∈Σ′和每一個s ∈Ω，(M,s)當且僅當(σ(s),Cxt)(φ)。

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

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

? 對每一個i ∈Agt和每一個sS′ ∈Ω′：

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

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

PAM 的個體信念更新

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

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

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

?τ:Agt×O×O→LLPA×LLPA是一個偏函數，

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

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

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

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

箭頭更新模型以|O|為倍數增大了初始模型。具體來說，對每一個輸出o′ ∈O和PAM 的每一個可能世界s′，會產生s′的一個增加了下標o′的復制(s′,o′)。而且，對每一個i ∈Agt和每一個輸出對(o′,o′′)，箭頭更新模型指定了起始條件τ1(i,o′,o′′)和目標條件τ2(i,o′,o′′)，它們分別被s′和s′′滿足，進而保證在乘積模型中，(s′,o′)和(s′′,o′′)具有i-可通達關系。這樣規定使得，可通達關系在乘積模型中被保留的充分必要條件為相應的兩個初始可能世界對應于該輸出分別滿足起始條件和目標條件。A函數的功能是擴大主體的覺知集合。具體來說，它將每一個主體和每一個輸出對應一個原子命題集，在乘積模型中，這一原子命題集將是該主體在被該輸出下標的可能世界的覺知集合的子集。直觀上講，這意味著在乘積模型中，主體的覺知集合因為增加了一些原子命題作為元素而被擴大。

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

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

? 對于每一個k,h ∈{1,2}和每一個j ∈Agt，τ(j,ok,oh) 有定義當且僅當（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←(α)、覺知擴張集合Atm(α)的個體箭頭更新模型。給定PAM 點模型(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。

互模擬

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

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

? 原子命題：s ∈π(p)當且僅當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)。

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

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

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

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

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

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

用常規的方式就可以驗證R(Atm(Σ)) 定義了M′和M′′的標準互模擬關系，因此，具有互模擬關系。

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

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

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

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

圖3：這是用個體箭頭更新過程來展示例1 的模型變化過程。圖中有兩個單主體模型。左邊的模型是信念更新之前小張的認知狀態，右邊的模型信念更新之后的認知狀態。大括號中的原子命題表示小張在該可能世界的覺知集合，模型中其他元素的解釋與圖1 保持一致。

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

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

7 結論與后續工作

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

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