徐京京

南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106

1 引言

認(rèn)知邏輯是模態(tài)邏輯的一個分支，主要研究與知識有關(guān)的推理。公共知識是指“一個群體中，所有agent知道，所有agent知道所有agent知道，所有agent知道所有agent知道所有agent知道……”的知識。分布式知識是指一個群體的綜合知識，即通過把一個群體中各個agent了解的知識綜合在一起所推出的知識。

在經(jīng)典邏輯下對認(rèn)知邏輯的研究已經(jīng)十分豐富，例如Fagin、Halpern和Moses對認(rèn)知邏輯基礎(chǔ)的介紹[1]；Vanderschraaf和 Sillari對公共知識的研究[2]；Hakli和Negri對分布式知識的研究[3]。近年來很多學(xué)者開始在直覺主義邏輯下對認(rèn)知邏輯展開研究，例如Marti和J?ger在直覺主義下分別處理了公共知識和分布式知識[4-5]；Hirai研究了有關(guān)異步通信的直覺主義認(rèn)知邏輯[6]；Suzuki研究了有關(guān)博弈論的直覺主義認(rèn)知邏輯[7]；Artemov和Protopopescu以及Proietti研究了對直覺主義認(rèn)知邏輯不同的定義方法[8-9]；Krupski和Yatmanov給出了直覺主義認(rèn)知邏輯的矢列演算系統(tǒng)[10]；Williamson對一般的直覺主義認(rèn)知邏輯做出了總結(jié)[11]。在直覺主義下對模態(tài)邏輯的研究、認(rèn)知邏輯的研究也有所幫助，例如Gisèle[12]、Ono[13]。

本文主要借鑒了Marti和J?ger對公共知識和分布式知識的處理方法以及給出了含分布式知識和公共知識的直覺主義認(rèn)知邏輯公理系統(tǒng)以及相應(yīng)的完備可靠性證明。

本文組織結(jié)構(gòu)如下：第2章介紹語言模型及語義解釋；第3章介紹公理系統(tǒng)；第4章介紹偽滿足性；第5章給出完備可靠性證明；第6章總結(jié)全文。

2 語言LCDK和語義解釋

本文主要處理多個agent的場景下出現(xiàn)的知識、公共知識以及分布式知識。假設(shè)agent的總數(shù)為l(l≥2)，分別記為ag1,ag2,…,agl。本文所用的語言LCDK包含以下的基本符號：

（1）可數(shù)多個原子命題p,q,r,…（可能帶有下標(biāo)），記原子命題的集合為PROP；

（2）邏輯常量⊥，邏輯連接詞∨、∧、→；

（3）模態(tài)詞K1,K2,…,Kl,C,D。

LCDK中的公式由下面的BNF范式產(chǎn)生：

直觀上Ki(α)表示agi了解知識α，C(α)表示α是公共知識，D(α)表示α是傳遞知識。本文使用一些縮寫形式，?α:=α→⊥，α?β:=(α→β)∧(β→α)，E(α):=K1(α)∧K2(α)∧…∧Kl(α)；若P是一個有限的公式集合，那么∧P,∨P分別表示P中所有公式的和合取和析??；用wff表示LCDK中所有公式組成的集合。

下文使用如下記號，若R是一個定義在非空集合W上的二元關(guān)系，則r(R)表示R的自反閉包，對任意v∈W，R[v]表示集合{w∈W|vRw}。

本文采用Marti和J?ger定義公式語義解釋的方法，將語義解釋定義在Kripke結(jié)構(gòu)上，記為EK-structure，并為定義公式C(α)的語義解釋引入3個集合，其定義如下。

定義1[4]EK-structure是一個l+3元組M=(W,? ,R1,R2,…,Rl,V)，其中：

（1）W是一個非空集合，?是一個定義在W上的前序關(guān)系；

（2）Ri(1≤i≤l)是定義在W上的二元關(guān)系，使得對任意v,w∈W滿足v?w?Ri[w]?Ri[v]；

（3）V是一個從W到PROP的冪集的函數(shù)，滿足對任意v,w∈W滿足v?w?V(w)?V(w)。

定義2[4]給定EK-structureM=(W,? ,R1,R2,…,Rl,V)，v,w∈W及n>0：

（1）PathM(v,w,n):={(u0,u1,…,un)|u0=v,un=w,ui+1∈?{Rj[ui]:1≤j≤l}(1≤i≤n+1)

（2）ReachM(v,n):={w∈W|PathM(v,w,n)≠ ?}

（3）ReachM(v):=∪n>0ReachM(v,n)

定義3給定EK-structureM=(W,?,R1,R2,…,Rl,V)及α∈wff，||α||M表示滿足α的可能世界的集合，歸納定義如下：

通過簡單的歸納證明可得集合||α||M滿足直覺主義邏輯中的單調(diào)性。

引理1對任意EK-structureM=(W,?,R1,R2,…,Rl,V)，v,w∈W及α∈wff，若v?w且v∈||α||M則有w∈||α||M。

證明關(guān)于α的公式復(fù)雜度歸納易證。

給定EK-structureM=(W,? ,R1,R2,…,Rl,V)，v∈W，α∈wff及P?wff，M,v╞α表示v∈||α||M，M╞α表示||α||M=W，╞α表示任意EK-structureM均滿足M╞α，M,v╞P表示對任意的α∈P滿足M,v╞α，同理可定義M╞P，╞P。

3 希爾伯特風(fēng)格公理系統(tǒng)ICDK、ICDT

本文定義希爾伯特風(fēng)格的公理系統(tǒng)，ICDK所包含的公理及規(guī)則陳列如下，其中α,β,γ∈wff，1≤i≤l。

ICDT在ICDK的基礎(chǔ)上添加了公理（T）D(α)→α。

本文使用（1）表示形如α→(α→β)的所有公式的集合，其他公理同理。ICDK?α表示α在ICDK中可推出。如果P?wff，那么P?ICDKα當(dāng)且僅當(dāng)存在有限多個 公 式γ1,γ2,…,γn∈P(n>0) 滿 足ICDK?(γ1∧γ2∧…∧γn)→α。同理可定義ICDT?α，P?ICDTα。

4 偽滿足性

為方便下一章構(gòu)造典范模型及證明完備性，參考Marti和J?ger處理直覺主義分布式知識的方法，引入偽滿足性及EK-structure的兩種變換，擴(kuò)張模型和關(guān)聯(lián)模型。

定義4給定EK-structureM=(W,?,R1,R2,…,Rl+1,V)，||α||pMs表示滿足α的可能世界的集合，歸納定義如下：

（1）～（7）同定義3；

（8）替換為||D(α)||pMs:={v∈W:Rl+1[v]? ||α||M}。

引理2對任意EK-structureM=(W,?,R1,R2,…,Rl+1,V)，v,w∈W及α∈wff，若v?w且v∈||α||pMs則有w∈ ||α||pMs。

證明關(guān)于α的公式復(fù)雜度歸納易證。

給定EK-structureM=(W,? ,R1,R2,…,Rl+1,V),v∈W，α∈wff及P∈wff，同理可定義M,v╞psα，M╞psα，M,v╞psP及M╞psP。

定義5給定EK-structureM=(W,?,R1,R2,…,Rl+1,V)，它的擴(kuò)張模型定義為M#=(W#,?#,R1#,R#2,…,R#l+1,V#)，其中：

（1）W#:=W×{1,2,…,l+1}

（2）?#:={((v,i)(w,j))|v?w,1≤i,j≤l+1}

（3）Ri#:={((v,j),(w,i))|vRiw,1≤j≤l+1}(1≤i≤l+1)

（4）V#((v,i)):=V(v)，(v,i)∈W#

引理3給定EK-structureM=(W,?,R1,R2,…,Rl+1,V)，對任意 (v,i)∈W#及α∈wff，滿足M,v╞psα?M#,(v,i╞)psα。

證明關(guān)于α的公式復(fù)雜度進(jìn)行歸納證明，當(dāng)α形如 ⊥,p,β∨γ,β∧γ時易證，下面考慮α形如β→γ、Ki(β)、C(β)、D(β)時的情形。

（1）α形如β→γ。

(?)任取 (v,i)∈W#滿足M,v╞psβ→γ，任取(w,j)∈W#滿足(v,i)?(w,j)且M#,(w,j╞)psβ。由?#的定義可知v?w，由歸納假設(shè)可得M,w╞psβ，根據(jù)語義解釋可得M,w╞psγ，根據(jù)歸納假設(shè)可得M#,(w,j╞)psγ，因此M#,(v,i╞)psβ→γ。

(?)任取(v,i)∈W#滿足M#,(v,i╞)psβ→γ，任取w∈W滿足v?w且M,w╞psβ。由?#的定義可知(v,i)?(w,j)(1≤j≤l+1)，由歸納假設(shè)可得M#,(w,j╞)psβ，根據(jù)語義解釋可得M#,(w,j╞)psγ，根據(jù)歸納假設(shè)可得M,w╞psγ，因此M,v╞psβ→γ。

（2）α形如Ki(β)。

(?)任取 (v,j)∈W#滿足M,v╞psKi(β)，任取 (w,i)∈W#滿足(v,j)Ri#(w,i)。由R#i的定義可知vRiw，根據(jù)語義解釋可得M,w╞psβ，根據(jù)歸納假設(shè)可得M#,(w,i╞)psβ，因此M#,(v,j╞)psKi(β)。

(?)任取(v,j)∈W#滿足M#,(v,j╞)psKi(β)，任取w∈W滿足vRiw，由Ri#的定義可知(v,j)R#i(w,i)，根據(jù)語義解釋可得M#,(w,i╞)psβ，根據(jù)歸納假設(shè)可得M,w╞psβ，因此M,v╞psKi(β)。

（3）α形如C(β)。

(?)任取 (v,i)∈W#滿足M,v╞psC(β)，任取 (w,j)∈W#滿足 (w,j)∈ReachM#((v,i))，由R#k(1≤k≤l+1)的定義易證w∈ReachM(v)，根據(jù)語義解釋可得M,w╞psβ，根據(jù)歸納假設(shè)可得M#,(w,j╞)psβ，因此M#,(v,i╞)psC(β)。

(?)任取(v,i)∈W#滿足M#,(v,i╞)psC(β)，任取w∈W滿足w∈ReachM(v)，由R#k(1≤k≤l+1)的定義易證存在1≤j≤l+1滿足(w,j)∈ReachM#((v,i))，根據(jù)語義解釋可得M#,(w,j╞)psβ，根據(jù)歸納假設(shè)可得M,w╞psβ，因此M,v╞psC(β)。

（4）α形如D(β)，處理方法同α形如Ki(β)時。

定義6給定EK-structureM=(W,?,R1,R2,…,Rl+1,V)，它的關(guān)聯(lián)模型定義為其中：

擴(kuò)張模型和關(guān)聯(lián)模型的定義是證明在滿足性保持的前提下，存在對應(yīng)偽滿足性解釋下的模型的一般滿足性解釋下的模型。引理3及下面的引理4、引理5就證明了這個問題。

引理4對任意EK-structureM=(W,?,R1,R2,…,Rl+1,V)，若M╞ps(D2)，那么對任意 (v,i)∈W#及α∈wff，滿足M#,(v,i)╞psα?M*,(v,i)╞α。

證明關(guān)于α的公式復(fù)雜度進(jìn)行歸納證明，當(dāng)α形如 ⊥,p,β∨γ,β∧γ,β→γ時易證，下面考慮α形如Ki(β)、C(β)、D(β)時的情形。

（1）α形如Ki(β)。

(?)任取(v,j)∈W#滿足M#,(v,j╞)psKi(β)，任取(w,k)∈W*滿足 (v,j)R*i(w,k)。由R*i的定義可知k=i或k=l+1。若k=i，則有(v,j)R#i(w,i)，根據(jù)語義解釋可得M#,(w,i╞)psβ，根據(jù)歸納假設(shè)可得M*,(w,i╞)β。若k=l+1，則有(v,j)R#l+1(w,l+1)，又由M╞ps(D2)及引理3可 知M╞#ps(D2)，進(jìn) 而 有M#,(v,j╞)psD(β)，因 此M#,(w,l+1╞)psβ，再根據(jù)歸納假設(shè)可得M*,(w,l+1╞)β。從而M*,(w,k╞)β，故M*,(v,j╞)Ki(β)。

(?)任 取(v,j)∈W*滿 足M*,(v,j╞)Ki(β)，任 取(w,i)∈W#滿足(v,j)R#i(w,i)，由R*i的定義可知(v,j)R*i(w,i)，根據(jù)語義解釋可得M*,(w,i╞)β，根據(jù)歸納假設(shè)可得M#,(w,i╞)psβ，因此M#,(v,j╞)psKi(β)。

（2）α形如C(β)。

(?)任取(v,i)∈W#滿足M#,(v,i╞)psC(β)，任取(w,j)∈W*滿足 (w,j)∈ReachM*((v,i))，由R#k(1≤k≤l+1)的定義易證(w,j)∈ReachM#((v,i))，根據(jù)語義解釋可得M#,(w,j╞)psβ，根據(jù)歸納假設(shè)可得M*,(w,j╞)β，因此M*,(v,i╞)C(β)。

(?)任取(v,i)∈W*滿 足M*,(v,i╞)C(β)，任取(w,j)∈W#滿足 (w,j)∈ReachM#((v,i))，由R*k(1≤k≤l)的定義易證(w,j)∈ReachM*((v,i))，根據(jù)語義解釋可得M*,(w,j╞)β，根據(jù)歸納假設(shè)可得M#,(w,j╞)psβ，因此M#,(v,i╞)psC(β)。

（3）α形如D(β)。

(?)任取(v,i)∈W#滿足M#,(v,i╞)psD(β)，任取(w,j)∈W*滿足，易證n≤l+1,m≠n)，進(jìn)而有，因此j=l+1，(v,i)R#l+1(w,j)，根據(jù)語義解釋可得M#,(w,j╞)psβ，根據(jù)歸納假設(shè)可得M*,(w,j╞)β，因此M*,(v,i╞)D(β)。

(?)任取(v,i)∈W*滿足M*,(v,i╞)D(β)，任取(w,j)∈W#滿足，進(jìn)而有，根據(jù)語義解釋可得M*,(w,j╞)β，根據(jù)歸納假設(shè)可得M#,(w,j╞)psβ，因此M#,(v,i╞)psD(β)。

引理5對任意EK-structureM=(W,?,R1,R2,…,Rl+1,V)，若M╞ps(D2)，那么對任意 (v,i)∈W*及α∈wff，滿足M,v╞psα?M*,(v,i╞)α。

證明根據(jù)引理3，引理4易證。

5 可靠性和完備性

本章結(jié)合Marti和J?ger處理公共知識和分布式知識的方法證明ICDK、ICDT的完備性。

下文使用如下記號，若P?wff，H是K1,K2,…,Kl,D中的一個模態(tài)詞，那么H-1(P)表示集合 {α|H(α)∈P}。

關(guān)于ICDK的可靠性通過驗(yàn)證公理的可靠性和規(guī)則的保真性易證。

定理1（可靠性）ICDK?α?╞α。

證明驗(yàn)證公理的可靠性和規(guī)則的保真性，易證。

關(guān)于ICDK的完備性，本文首先參考Marti和J?ger在直覺主義邏輯下處理公共知識的方法，定義切片，α-prime集合，這個概念類似于模態(tài)邏輯中的極大協(xié)調(diào)集。

定義7切片M(α)?wff，按如下方式歸納生成：

（1）α,⊥∈M(α)；

（2）若β∈M(α)，則β的子公式屬于M(α)；

（3）若C(β)∈M(α)，則E(β),E(C(β))∈M(α)；

（4）若Ki(β)∈M(α)，則D(β)∈M(α)。

定義8對任意P?wff，稱P是α-prime的當(dāng)且僅當(dāng)P滿足：

（1）P?M(α)；

（2）若β∈M(α)且P?ICDKβ則β∈P；

（3）若β∨γ∈P則β∈P或γ∈P；

（4）⊥?P。

下面證明的引理，其作用類似于模態(tài)邏輯中的Lindenbaum引理，證明了滿足一定條件的公式集合可以擴(kuò)張成一個α-prime集合。

引理6若公式集合P?M(α)滿足則存在一個α-prime的公式集合Q滿足P?Q且。

證明易證M(α)中的公式個數(shù)為有限多個，取γ0,γ1,…,γk(k>0)表示M(α)中所有的公式。對n=0,1,…,k歸納定義：

（1）根據(jù)定義可知Q?M(α)。

（2）任取δ∈M(α)滿足Q?ICDKδ?？芍嬖?≤m≤k使得γm=δ。若Pm?{γm}?ICDKβ，則有Pm+1=Pm?{γm}，進(jìn)而δ∈Q。若Pm?{γm}?ICDKβ，則有Pm+1=Pm，進(jìn)而Q?{γm}?ICDKβ，故Q?ICDKβ，與已知矛盾。因此δ∈Q。

（3）任取δ1∨δ2∈Q，假設(shè)δ1?Q且δ2?Q?？芍嬖?0≤i,j≤k使得γi=δ1，γj=δ2，進(jìn)而Pi?{γi}?ICDKβ，Pj?{γj}?ICDKβ，因此Q?ICDKγi→β,Q?ICDKγj→β,Q?ICDK(γi∨γj)→β，又δ1∨δ2∈Q，故Q?ICDKβ，與已知矛盾。因此δ1∈Q或δ2∈Q。

（4）因?yàn)閧⊥}?ICDKβ，易知⊥Q。

下文參考Marti和J?ger在直覺主義邏輯下處理分布式知識的方法，結(jié)合其處理公共知識的方法，定義關(guān)于α∈wff的典范模型，并在偽滿足性的語義解釋下證明真值引理。

定義9對于任意α∈wff，構(gòu)造相應(yīng)典范的模型為EK-structureCα=(W,?,R1,R2,…,Rl+1,V)滿足：

（1）W:={P?wff|P是α-prime的}；

（2）Ri:={(P,Q)∈W×W|K-1i(P)?Q}(1≤i≤l)；

（3）Rl+1:={(P,Q)∈W×W|D-1(P)?Q}；

（4）V是一個從W到PROP的冪集的函數(shù)，滿足V(P):={p∈PROP|p∈P}。

引理7若Cα=(W,?,R1,R2,…,Rl+1,V)是關(guān)于公式α的典范模型，則對任意β∈M(α),P∈W滿足β∈P?Cα,P?psβ。

證明定義從wff到自然數(shù)集合的函數(shù)rank如下，其中p∈PROP，γ,γ1,γ2∈wff，1≤i≤l：

下面根據(jù)公式β的rank函數(shù)值大小進(jìn)行歸納證明：

（1）β為⊥或原子命題時，β∈P?Cα,P╞psβ平凡成立。

（2）β形如γ1∨γ2，γ1∧γ2時，根據(jù)歸納假設(shè)和α-prime的性質(zhì)易證。

（3）β形如γ1→γ2。

(?)任取P∈W滿足γ1→γ2∈P，任取Q∈W滿足P?Q且Cα,Q╞psγ1。易知γ1→γ2∈Q，根據(jù)歸納假設(shè)可知γ1∈Q，進(jìn)而Q?ICDKγ2，根據(jù)M(α)的定義可知γ2∈M(α)，因此γ2∈Q，根據(jù)歸納假設(shè)可得Cα,Q╞psγ2，Cα,P╞psγ1→γ2。

(?)任取P∈W滿足Cα,P╞psγ1→γ2，假設(shè)γ1→。故，根據(jù)引理 6 可知存在Q∈W，滿足，根據(jù)歸納假設(shè)可知，矛盾于。故。

（4）β形如Ki(γ)。

(?)任取P∈W滿足Ki(γ)∈P，任取Q∈W滿足Ki-1(P)?Q，故γ∈Q，根據(jù)歸納假設(shè)可知Cα,Q╞psγ，因此Cα,P╞psKi(γ)。

(?)任取P∈W滿足，假設(shè)。根據(jù)引理6可知存在滿足α-prime的公式集合Q，且，根據(jù)歸納假設(shè)可得，矛盾于。故，因此Ki(γ)∈P。

（5）β形如C(γ)。

(?)任取P∈W滿足C(γ)∈P，根據(jù)n的大小進(jìn)行歸納證明易得，對任意n>0，Q∈ReachCα(P,n)滿足γ∈Q,C(γ)∈Q，故對任意Q∈ReachCα(P)，滿足γ∈Q，根據(jù)歸納假設(shè)可知Cα,Q╞psγ，故Cα,P╞psC(γ)。

(?)任取P∈W滿足Cα,P╞psC(γ)，定義W′:={Q∈W|Q╞psC(γ)}，δ:=∨{∧Q|Q∈W′}。首先證明 4個命題。

①若Q∈W′，則有ICDK?∧Q→Ki(γ)。

任取Q∈W′，進(jìn)而有Cα,Q╞psC(γ)，Cα,Q╞psKi(γ)，又rank(C(γ))>rank(Ki(γ)) ，故 根 據(jù) 歸 納 假 設(shè) 可 得Ki(γ)∈Q，因此ICDK?∧Q→Ki(γ)。

②若Q∈W′，S∈W且QRiS，則有S∈W′。

任取Q∈W′，任取S∈W且QRiS，又Cα,Q╞psC(γ)，Cα,Q╞psKi(C(γ))，因此Cα,S╞psC(γ)，從而S∈W′。

③若Q∈W′，則有Ki-1(Q)?ICDKδ。

任取Q∈W′，假設(shè)Ki-1(Q)?ICDKδ，根據(jù)引理6可得存在S∈W滿足Ki-1(Q)?S，S?ICDKδ，根據(jù)②可知S∈W′矛盾于S?ICDKδ，因此Ki-1(Q)?ICDKδ。

④若Q∈W′，則有ICDK?∧Q→Ki(δ)。

任取Q∈W′，故根據(jù)③可知存在ε1,ε2,…,εn∈Ki-1(Q)滿足ICDK?(ε1∧ε2∧…∧εn)→δ，變換可得ICDK?(Ki(ε1)∧Ki(ε2)∧… ∧Ki(εn))→Ki(δ)，故Q?ICDKKi(δ)，因此ICDK?∧Q→Ki(δ)。

任取Q∈W′，根據(jù)①④可得，Q?ICDKKi(δ)∧Ki(γ)，進(jìn)而ICDK?δ→E(δ∧γ)，因此ICDK?δ→C(γ)，故P?ICDKC(γ)，C(γ)∈P。

（6）β形如D(γ)。

(?)任取P∈W滿足D(γ)∈P，任取Q∈W滿足D-1(P)?Q，故γ∈Q，根據(jù)歸納假設(shè)可知Cα,Q╞psγ，因此Cα,P╞psD(γ)。

(?)任取P∈W滿足Cα,P╞psD(γ)，假設(shè)D-1(P)?ICDKγ，根據(jù)引理6可知存在Q∈W，滿足D-1(P)?Q且Q?ICDKγ，根據(jù)歸納假設(shè)可得Cα,Q╞psγ，矛盾于Cα,P╞psD(γ)。故D-1(P)?ICDKγ,P?ICDKD(γ)，因此D(γ)∈P。

下面，通過第4章定義的擴(kuò)張模型和關(guān)聯(lián)模型可以得到一個在一般滿足性的語義解釋下與Cα的滿足性一致的模型。

引理8若Cα=(W,?,R1,R2,…,Rl+1,V)是關(guān)于公式α的典范模型，C*α是Cα的關(guān)聯(lián)模型，則對任意(P,i)∈W*，β∈M(α)，滿足β∈P?C*α,(P,i╞)β。

證明任取P∈W，任取Ki(β)∈wff，Q∈W滿足Cα,Q?psKi(β),P?Q。由引理7可知Ki(β)∈Q，故Ki(β)∈M(α)，根據(jù)M(α)的定義可知D(β)∈M(α)，又ICDK?Ki(β)→D(β)，故Q?ICDKD(β)，根據(jù)α-prime的定義可知D(β)∈Q，又根據(jù)引理 7 可知Cα,Q╞psD(β)，進(jìn)而Cα,P╞psKi(β)→D(β)，故C╞αps(D2)，由引理5可知對任意(P,i)∈W*,β∈M(α)，滿足β∈P?C*α,(P,i╞)β。

定理2（完備性）╞α?ICDK?α。

證明假設(shè)╞α。假設(shè)ICDK?α，根據(jù)引理6可知存在一個α-prime的公式集合P，滿足P?ICDKα，，考慮關(guān)于公式α的典范模型Cα的關(guān)聯(lián)模型，由引理8可得存在 (P,i)∈W*，C*α,(P,i)?α，矛盾于╞α。故ICDK?α。

仿照對ICDK的完備可靠性證明，易得ICDT的完備可靠性證明思路，下文對重復(fù)的步驟簡要帶過。

定理3（可靠性）若ICDT?α，則對任意自反的EK-structureM，滿足M╞α。

證明在ICDK可靠性證明的基礎(chǔ)上驗(yàn)證(T)公理的可靠性，易證。

定義10稱公式集合P是α-T-prime的當(dāng)且僅當(dāng)P滿足：

（1）、（3）、（4）同定義8；

（2）若β∈M(α)且P?ICDTβ則β∈P。

引理9若公式集合P?M(α)滿足P?ICDTβ(β∈wff)，則存在一個α-T-prime的公式集合Q滿足P?Q且Q?ICDTβ。

證明同引理6。

定義11對于任意α∈wff，構(gòu)造相應(yīng)典范的模型為EK-structureNα=(W,?,R1,R2,…,Rl+1,V)滿足：

（1）W:={P?wff|P是α-T-prime的}；

（2）、（3）、（4）同定義9。

引理10若Nα=(W,?,R1,R2,…,Rl+1,V)是關(guān)于公式α的典范模型，則對任意β∈M(α)，P∈W滿足β∈P?Nα,P╞psβ。

證明同引理7。

引理11若Nα=(W,?,R1,R2,…,Rl+1,V)是關(guān)于公式α的典范模型，Nα*是Nα的關(guān)聯(lián)模型，則N╞α*(T)且對任意(P,i)∈W*,β∈M(α)，滿足β∈P?Nα*,(P,i╞)β。

證明同引理8易證對任意(P,i)∈W*，β∈M(α)，滿足β∈P?Nα*,(P,i╞)β。下面證明N╞α*(T)。任取P∈W，任取D(β)∈wff，Q∈W滿足Cα,Q╞psD(β)，P?Q，由引理 10可知D(β)∈Q，故D(β)∈M(α)，又ICDT?D(β)→β，故Q?ICDT，β根據(jù)α-T-prime的定義可知β∈Q，由引理10可得Nα,Q╞psβ，進(jìn)而Nα,P╞psD(β)→β，故N╞αps(T)，因此N╞α*(T)。

上文得到的Nα*并不一定滿足自反性，下面定義EK-structure的自反拓展，并證明在一定條件下通過自反拓展后的模型與原模型滿足性保持一致。

定義12給定EK-structureM=(W,?,R1,R2,…,Rl,V)，定義M的自反拓展，其中。

引理12給定EK-structureM=(W,?,R1,R2,…,Rl,V)，M╞(T)，則滿足自反，且對任意公式α，任意v∈W，有。

證明關(guān)于α的公式復(fù)雜度進(jìn)行歸納證明，當(dāng)α形如 ⊥,p,β∨γ,β∧γ,β→γ時易證，下面考慮α形如Ki(β)、C(β)、D(β)時的情形。

（1）α形如Ki(β)。

(?)任取v∈W滿足M,v╞Ki(β)，任取w∈W滿足。由的定義可知v=w或vRiw。若v=w，因?yàn)镸╞(T)，所以，易推導(dǎo)β，所以。若，根據(jù)語義解釋易知。根據(jù)歸納假設(shè)可得，故。

(?)任取v∈W滿足，任取w∈W滿足，由的定義可知，根據(jù)語義解釋易知，根據(jù)歸納假設(shè)可得，故。

（2）α形如C(β)。

(?)任取v∈W滿足，任取w∈W滿足)。即存在滿足因此1≤j≤l}(1≤i≤n+1)或ui+1=ui，根據(jù)i的大小歸納證明易得。根據(jù)歸納假設(shè)可得，故。

(?)任取v∈W滿足，任取w∈W滿足，由的定義易證，根據(jù)語義解釋易知，根據(jù)歸納假設(shè)可得，故。

（3）α形如D(β)。

(?)任取v∈W滿足M,v╞D(β)，任取w∈W滿足，由的定義可知因此v=w或若v=w，因?yàn)镸╞(T)，所以M,v╞D(β)→β，M,w╞β；若因?yàn)镸,v╞D(β)，所以M,w╞β，根據(jù)歸納假設(shè)可知，所以。

(?)任取v∈W滿足，任取w∈W滿足，由的定義可知，因此，根據(jù)歸納假設(shè)可知M,w╞β，因此M,v╞D(β)。

定理4（完備性）若任意自反的EK-structureM滿足M╞α則ICDT?α。

證明假設(shè)任意自反的EK-structureM均滿足M╞α。假設(shè)ICDT?α，根據(jù)引理9可知存在一個α-T-prime的公式集合P，滿足P?ICDTα，α?P，考慮關(guān)于公式α的典范模型Nα的關(guān)聯(lián)模型Nα*，由引理11可得N╞α*(T)，且對任意(P,i)∈W*，β∈M(α)，滿足，由引理12可得滿足自反性，且任意，滿足，因此矛盾于任一自反的EK-structureM滿足M╞α，從而ICDT?α。

6 總結(jié)

本文給出了直覺主義公共知識和分布式知識的公理系統(tǒng)ICDK、ICDT，以及其相應(yīng)的語義解釋，并建立了其間的可靠完備性。

在本文的基礎(chǔ)上，可以開展對正向內(nèi)省性和負(fù)向內(nèi)省性即S4、S5系統(tǒng)的研究，關(guān)于正向內(nèi)省性的研究可以參考Fagin、Halpern和Vardi[14]，關(guān)于負(fù)向內(nèi)省性的研究可以參考Do?en[15]。