直覺主義認知邏輯ICDK*

徐京京

南京航空航天大學 計算機科學與技術學院，南京 211106

1 引言

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

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

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

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

2 語言LCDK和語義解釋

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

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

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

（3）模態詞K1,K2,…,Kl,C,D。

LCDK中的公式由下面的BNF范式產生：

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

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

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

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

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

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

（3）V是一個從W到PROP的冪集的函數，滿足對任意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滿足直覺主義邏輯中的單調性。

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

證明關于α的公式復雜度歸納易證。

給定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 希爾伯特風格公理系統ICDK、ICDT

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

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

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

4 偽滿足性

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

定義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。

證明關于α的公式復雜度歸納易證。

給定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)，它的擴張模型定義為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α。

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

（1）α形如β→γ。

(?)任取 (v,i)∈W#滿足M,v╞psβ→γ，任取(w,j)∈W#滿足(v,i)?(w,j)且M#,(w,j╞)psβ。由?#的定義可知v?w，由歸納假設可得M,w╞psβ，根據語義解釋可得M,w╞psγ，根據歸納假設可得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)，由歸納假設可得M#,(w,j╞)psβ，根據語義解釋可得M#,(w,j╞)psγ，根據歸納假設可得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，根據語義解釋可得M,w╞psβ，根據歸納假設可得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)，根據語義解釋可得M#,(w,i╞)psβ，根據歸納假設可得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)，根據語義解釋可得M,w╞psβ，根據歸納假設可得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))，根據語義解釋可得M#,(w,j╞)psβ，根據歸納假設可得M,w╞psβ，因此M,v╞psC(β)。

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

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

擴張模型和關聯模型的定義是證明在滿足性保持的前提下，存在對應偽滿足性解釋下的模型的一般滿足性解釋下的模型。引理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)╞α。

證明關于α的公式復雜度進行歸納證明，當α形如 ⊥,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)，根據語義解釋可得M#,(w,i╞)psβ，根據歸納假設可得M*,(w,i╞)β。若k=l+1，則有(v,j)R#l+1(w,l+1)，又由M╞ps(D2)及引理3可 知M╞#ps(D2)，進 而 有M#,(v,j╞)psD(β)，因 此M#,(w,l+1╞)psβ，再根據歸納假設可得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)，根據語義解釋可得M*,(w,i╞)β，根據歸納假設可得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))，根據語義解釋可得M#,(w,j╞)psβ，根據歸納假設可得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))，根據語義解釋可得M*,(w,j╞)β，根據歸納假設可得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=l+1，(v,i)R#l+1(w,j)，根據語義解釋可得M#,(w,j╞)psβ，根據歸納假設可得M*,(w,j╞)β，因此M*,(v,i╞)D(β)。

(?)任取(v,i)∈W*滿足M*,(v,i╞)D(β)，任取(w,j)∈W#滿足，進而有，根據語義解釋可得M*,(w,j╞)β，根據歸納假設可得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╞)α。

證明根據引理3，引理4易證。

5 可靠性和完備性

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

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

關于ICDK的可靠性通過驗證公理的可靠性和規則的保真性易證。

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

證明驗證公理的可靠性和規則的保真性，易證。

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

定義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的當且僅當P滿足：

（1）P?M(α)；

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

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

（4）⊥?P。

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

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

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

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

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

（3）任取δ1∨δ2∈Q，假設δ1?Q且δ2?Q。可知存在 0≤i,j≤k使得γi=δ1，γj=δ2，進而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）因為{⊥}?ICDKβ，易知⊥Q。

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

定義9對于任意α∈wff，構造相應典范的模型為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的冪集的函數，滿足V(P):={p∈PROP|p∈P}。

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

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

下面根據公式β的rank函數值大小進行歸納證明：

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

（2）β形如γ1∨γ2，γ1∧γ2時，根據歸納假設和α-prime的性質易證。

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

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

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

（4）β形如Ki(γ)。

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

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

（5）β形如C(γ)。

(?)任取P∈W滿足C(γ)∈P，根據n的大小進行歸納證明易得，對任意n>0，Q∈ReachCα(P,n)滿足γ∈Q,C(γ)∈Q，故對任意Q∈ReachCα(P)，滿足γ∈Q，根據歸納假設可知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′，進而有Cα,Q╞psC(γ)，Cα,Q╞psKi(γ)，又rank(C(γ))>rank(Ki(γ)) ，故 根 據 歸 納 假 設 可 得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′，假設Ki-1(Q)?ICDKδ，根據引理6可得存在S∈W滿足Ki-1(Q)?S，S?ICDKδ，根據②可知S∈W′矛盾于S?ICDKδ，因此Ki-1(Q)?ICDKδ。

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

任取Q∈W′，故根據③可知存在ε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′，根據①④可得，Q?ICDKKi(δ)∧Ki(γ)，進而ICDK?δ→E(δ∧γ)，因此ICDK?δ→C(γ)，故P?ICDKC(γ)，C(γ)∈P。

（6）β形如D(γ)。

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

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

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

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

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

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

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

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

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

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

定義10稱公式集合P是α-T-prime的當且僅當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，構造相應典范的模型為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)是關于公式α的典范模型，則對任意β∈M(α)，P∈W滿足β∈P?Nα,P╞psβ。

證明同引理7。

引理11若Nα=(W,?,R1,R2,…,Rl+1,V)是關于公式α的典范模型，Nα*是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，β根據α-T-prime的定義可知β∈Q，由引理10可得Nα,Q╞psβ，進而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，有。

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

（1）α形如Ki(β)。

(?)任取v∈W滿足M,v╞Ki(β)，任取w∈W滿足。由的定義可知v=w或vRiw。若v=w，因為M╞(T)，所以，易推導β，所以。若，根據語義解釋易知。根據歸納假設可得，故。

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

（2）α形如C(β)。

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

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

（3）α形如D(β)。

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

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

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

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

6 總結

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

在本文的基礎上，可以開展對正向內省性和負向內省性即S4、S5系統的研究，關于正向內省性的研究可以參考Fagin、Halpern和Vardi[14]，關于負向內省性的研究可以參考Do?en[15]。