動(dòng)態(tài)認(rèn)知邏輯的幾個(gè)應(yīng)用

1、動(dòng)態(tài)認(rèn)知邏輯的幾個(gè)應(yīng)用 收稿日期：2006-1-10基金項(xiàng)目：本文得到教育部基地重大項(xiàng)目歸納邏輯及其應(yīng)用（項(xiàng)目編號(hào)05JJD720.40001）和教育部哲學(xué)社會(huì)科學(xué)研究重大課題攻關(guān)項(xiàng)目 (04JZD0006) 的資助。作者簡介：李小五(1955-)，男，河北人，中山大學(xué)教授，北京書生公司書生研究中心客座研究員。電子郵箱：LXW121李小五(中山大學(xué)邏輯與認(rèn)知研究所，廣東 廣州 510275)內(nèi)容提要：我們建立若干邏輯分別刻畫下列概念：做了一個(gè)活動(dòng)、若干主體做了若干活動(dòng)形成合力改變一個(gè)狀態(tài)、知道一個(gè)主體、知道一個(gè)性質(zhì)與知道一個(gè)關(guān)系。關(guān)鍵詞：做了一個(gè)活動(dòng)；合力改變一個(gè)狀態(tài)；知道一個(gè)主體；知道一個(gè)性

2、質(zhì)與知道一個(gè)關(guān)系中圖分類號(hào)：B81 文獻(xiàn)標(biāo)識(shí)碼：A一、正則做活動(dòng)邏輯通常的動(dòng)態(tài)邏輯在語形方面（相對(duì)公理化系統(tǒng)）沒有獨(dú)立刻畫做了一個(gè)活動(dòng)的邏輯性質(zhì)。例如，沒有刻畫像“我吃了”那樣的句子。也就是說，相對(duì)活動(dòng)a，它們只刻畫了形如aj的句子，而這樣的句子只是間接刻畫了活動(dòng)a。至于像“我吃了”那樣的句子（概括為“（某主體）做了活動(dòng)a”，符號(hào)化為Da）有什么邏輯性質(zhì)，這些邏輯沒有揭示。而在我們看來，這是一類很重要的句子。為了簡潔，本節(jié)我們只研究單主體邏輯。我們邏輯的基礎(chǔ)是文獻(xiàn)1提到的PDL和9提到的DA1。1.1公式的形成規(guī)則令A(yù)tp1, pn,是可數(shù)無窮多個(gè)原子公式的集合，令A(yù)cta1, am,是可數(shù)無

3、窮多個(gè)原子活動(dòng)的集合。聯(lián)立歸納定義所有公式j(luò)的集合Form和所有活動(dòng)a的集合Action如下：j:p½Øj½(jÙy)½aj½Da， 其中pÎAt；a:a½(aÈb)½(a;b)½a*， 其中aÎAct。說明：據(jù)1第166頁的解釋，aj的直觀意義是：It is necessary that after executing a, j is true。aÈb的直觀意義是：Choose either a or b nondeterministically and exec

4、ut it。a;b的直觀意義是：Execut a, then execut b。a*的直觀意義是：Execut a a nondeterministically chosen finite number of times (zero or more)。aÈb, a;b和a*統(tǒng)稱為復(fù)合活動(dòng)（運(yùn)算），其中aÈb稱為“復(fù)合a和b的選擇活動(dòng)”，a;b稱為“復(fù)合a和b的相繼活動(dòng)”，a*稱為“a的（有窮）疊加活動(dòng)”。Da的直觀意義是： “（主體）做了活動(dòng)a”（The action a has been executed (by the agent)）。這是我們的邏輯主要要刻畫的公式。1

5、.2規(guī)定與縮寫 聯(lián)結(jié)符Ú，®和«的縮寫定義如通常給出。另外，縮寫定義<a>j:ØaØj。為了敘述方便，我們規(guī)定聯(lián)結(jié)符的結(jié)合力從左到右依次減弱：Ø，a，D，Ù，Ú，®，«。此外，我們規(guī)定同形聯(lián)結(jié)符滿足右向結(jié)合原則。例如，j®y®q表示j®(y®q)。T定義為p1ÚØp1， 定義為ØT。我們常用Û表示“當(dāng)且僅當(dāng)”，用Þ表示“若，則”，用表示“并非”。1.3定義正則系統(tǒng)RDA定義如下：對(duì)所有a, b&

6、#206;Action，j, yÎForm，（TA） 所有重言式的代入特例，（Ka） a(j®y)®aj®ay，（Da） aDa， （活動(dòng)公理）（AÈ） aÈbj«ajÙbj， （選擇公理）（A;） a;bj«abj， （相繼公理）（A*） jÙaa*j«a*j， （疊加公理）（IA*） jÙa*(j®aj)®a*j， （歸納公理）（MP） j, j®yy，（RNa） jaj，（RDa） <a>Da®ajDa®j。

7、（活動(dòng)規(guī)則）說明：公理Da和規(guī)則RDa刻畫了做活動(dòng)概念的基本特性，公理AÈ和A;分別刻畫了復(fù)合活動(dòng)運(yùn)算aÈb和a;b的基本特性，公理IA*和IA*刻畫了復(fù)合活動(dòng)運(yùn)算a*的基本特性。文獻(xiàn)2稱刻畫aÈb，a;b和a*的動(dòng)態(tài)邏輯為正則邏輯，而在1，還要加上刻畫測試運(yùn)算j?的公理j?y«(j®y)才能稱為正則邏輯。這里我們遵從2的稱謂，因?yàn)樵黾訙y試運(yùn)算無法證明下面系統(tǒng)的框架可靠性定理和框架完全性定理，而這是邏輯追求的重要目標(biāo)。另一方面，從測試公理j?y«(j®y)和活動(dòng)公理Da易得j®D(j?)。而后者的直觀意義是：每一真

8、命題都被（主體）測試過。在我們看來這似乎不自然。由TA和MP構(gòu)成的系統(tǒng)稱為經(jīng)典句子系統(tǒng)，記為PC。我們也用PC0表示用不含模態(tài)算子a的語言表述的PC。1.4定義我們用 j 表示j是RDA的內(nèi)定理：j在RDA中有一個(gè)形式證明。RDA的全體內(nèi)定理的集合記為Th(RDA)。我們也用 j 表示jÏTh(RDA)。1.5引理下面是RDA的導(dǎo)出規(guī)則和內(nèi)定理：（1）j®yaj®ay，j®y<a>j®<a>y；（2）aj«Ø<a>Øj； （3）j1ÙÙjn®jaj1

9、ÙÙajn®aj；（4）<a>(j1ÙÙjn)®<a>j1ÙÙ<a>jn；（5）ajDa®j；（6）D(aÈb)«DaÚDb，D(aÈa)«Da；（7）D(a;b)®Db，D(a;a)®Da；（8）Da«a*Da，（9）Da*。證明：（1）（4）據(jù)Ka和RNa如通常所證。（5） aj 假設(shè) <a>Da®aj Da®j。 ，RDa（6） a(DaÚDb

10、)，b(DaÚDb) TA，（1），Da，MP aÈb(DaÚDb)，AÈ D(aÈb)®DaÚDb ，（5）aD(aÈb)，bD(aÈb) Da，AÈDa®D(aÈb)，Db®D(aÈb) ，（5）DaÚDb®D(aÈb)。 （7） abDb Da，RNa a;bDb ，A; D(a;b)®Db。 ，（5）因此我們有D(a;a)®Da。（8） Da®aDa Da，TA a*(Da®aD

11、a) ，RNa Da®a*Da。 ，歸納公理 a*Da®Da。 疊加公理 （9）據(jù)疊加公理，有a*Da*®Da*，再據(jù)活動(dòng)公理Da，易得要證結(jié)果。說明：初看到（9）令人驚訝，但仔細(xì)一想還是很自然的。對(duì)當(dāng)下主體來說，它在任何情況下總是做了若干次活動(dòng)a（因?yàn)槠渲幸舶?次）。1.6定義定義從Form到不含模態(tài)算子的子語言Form0ÍForm的翻譯映射t如下：t(p)p，對(duì)所有原子公式pÎAt；t(Øj)Øt(j)；t(jÙy)t(j)Ùt(y)；t(aj)t(j)；t(Da)T。對(duì)每一公式j(luò)ÎFor

12、m，我們稱t(j)是j的t-翻譯。1.7定義令S1和S2是任意兩個(gè)公理化系統(tǒng)。我們稱S1能t-退化為S2，當(dāng)且僅當(dāng)，S1的所有內(nèi)定理的t-翻譯是S2的內(nèi)定理。1.8翻譯定理RDA能t-退化為PC0。證明：據(jù)上面的定義，證明顯然。1.9定義稱系統(tǒng)S是協(xié)調(diào)系統(tǒng)，當(dāng)且僅當(dāng)，不存在j使得j和Øj都是S的內(nèi)定理。1.10定理RDA是協(xié)調(diào)的。證明：假設(shè)RDA不協(xié)調(diào)，則存在j使得j和Øj都是RDA的內(nèi)定理。據(jù)上面的翻譯定理，t(j)和Øt(j)都是PC0的內(nèi)定理，矛盾于PC0的協(xié)調(diào)性。1.11定義（1）稱<W, R>是（正則）框架，當(dāng)且僅當(dāng)，W是非空狀態(tài)集，R是定義

13、域?yàn)锳ction的映射：對(duì)每一aÎAction，Ra是W上的二元通達(dá)關(guān)系使得下列框架條件滿足： 其中Ra是R(a)的縮寫。（CH）RaÈb:RaÈRb。（CO）Ra;b:Ra o Rb:<w, u>ÎW2：$vÎW(<w, v>ÎRa且<v, u>ÎRb)。（IT）Ra*:<w, u>ÎW2：$n³0$v0, vnÎW(wv0, uvn且對(duì)0£ i £n1, <vi, v i+1>ÎRa)。本節(jié)把所有（正則

14、）框架的類記作Frame。（2）稱<W, R, >是模型，當(dāng)且僅當(dāng)，<W, R>是框架且 是從At到W的冪集P(W)中的指派映射。這里， 也稱為框架<W, R>上的指派映射。說明：CH是choice的縮寫，CO是composition的縮寫，IT是iteration的縮寫。IT等號(hào)右邊的集合通常記作Ra*，即(Ra)*。它也稱為Ra的自返傳遞閉包。以后我們用wRau表示<w, u>ÎRa。1.12定義與約定令<W, R>是框架。任給wÎW和aÎAction，Ra(w) :uÎW：wRau。以后我

15、們用$uRaw表示$uÎW(uRaw)。若$uRaw，則稱w是a-左持續(xù)的。1.13真值集定義令M<W, R, >是模型。定義j相對(duì)M的真值集j如下：任給wÎW和aÎAction，（1）wÎØj Û wÏj，（2）wÎjÙy Û wÎj且wÎy，（3）wÎaj Û Ra(w)Íj， （4）wÎDa Û $uRaw。說明：$uRaw表示：存在初始狀態(tài)u使得（主體）在其中做了a從而把u改變?yōu)闋顟B(tài)w，這正是我們說在w中（

16、主體）做了a的意思。注意：$uRaw是點(diǎn)框架條件：Da在w的真值只取決于w是否有a-左持續(xù)性。據(jù)上述語義，特別是（4），易見Da*在任何wÎW中成立（這對(duì)應(yīng)前面Da*是內(nèi)定理），但存在uÎW使得Da在u中不成立，也存在vÎW使得Da在v中成立但D(a;a)在v中不成立。下面的引理據(jù)真值集定義的（1）和（2）就能證明：1.14引理 令<W, R, >是模型。則ØjWj，jÙyjÇy，jÚyjÈy， Æ， T W，jÇj®yÍy，j®yW Û j&

17、#205;y，j«yW Û jy。1.15有效性定義 令F<W, R>是框架，M<W, R, >是模型。稱j在M中有效，記為M j，Û jW；否則稱j在M中不有效，記為M j。稱j在F中有效，記為F j，Û 對(duì)F上的任意指派映射 ，有jW；否則稱j在F中不有效，記為F j。稱規(guī)則j1, jny相對(duì)M保持有效性 Û 若j1jnW，則yW 。1.16框架可靠性定理RDA相對(duì)Frame可靠。證明：任給框架F<W, R>和F上賦值 。下面驗(yàn)證RDA的公理相對(duì)M<F, >有效且RDA的推理規(guī)則相對(duì)M保持有效

18、性。公理TA和Ka，規(guī)則MP和RNa的驗(yàn)證如通常。AÈ, A;, A*和IA*的驗(yàn)證參見1的定理5.8(ii)，5.10(ii)，5.15(ix)和(xi)。驗(yàn)證Da：假設(shè)aDa在M中不有效，則存在wÎW使得wÏaDa。據(jù)真值集定義，我們有Ra(w) Da，所以存在vÎW使得wRav且vÏDa。據(jù)后者和真值集定義，我們有$uRav，矛盾于wRav。驗(yàn)證RDa：設(shè)<a>DaÍaj。需證：DaÍj。任給wÎDa，據(jù)真值集定義，有$uRaw，再據(jù)uRaw 和wÎDa，有uÎ<a>

19、;Da。再據(jù)設(shè)定，有uÎaj，再據(jù)uRaw，有wÎj。因?yàn)镽DA是PDL的擴(kuò)充，所以根據(jù)活動(dòng)和公式的聯(lián)立歸納法（據(jù)1.1）和*-算子的特性（據(jù)公理A*和IA*以及1.11（IT），我們不能用通常的典范模型方法證明RDA的框架完全性定理，而是要用過濾方法，為此我們先要定義FL-閉包作為過濾器。1.17定義聯(lián)立歸納定義函數(shù)FL和FL如下：（1）FL(p)p，對(duì)所有原子公式pÎAt；（2）FL(Øj)ØjÈFL(j)；（3）FL(jÙy)jÙyÈFL(j)ÈFL(y)；（4）FL(Da)Da，對(duì)所有原

20、子活動(dòng)aÎAct；（5）FL(D(aÈb)D(aÈb)ÈFL(Da)ÈFL(Db)；（6）FL(D(a;b)D(a;b)ÈFL(Da)ÈFL(Db)；（7）FL(Da*)Da*ÈFL(Da)；（8）FL(aj)FL(aj)ÈFL(j)；其中FL(aj)如下定義：FL(aj)aj，對(duì)所有原子活動(dòng)aÎAct；FL(aÈbj)aÈbjÈFL(aj)ÈFL(bj)；FL(a;bj)a;bjÈFL(abj)ÈFL(bj)；FL(a*j)a*j&#

21、200;FL(aa*j)。說明：FL(j)稱為j的Fischer-Ladner-closure，簡稱j的FL-閉包。 嚴(yán)格說，1給出的FL-閉包是沒有上述（4）（6）的。 FL(j)中的公式和活動(dòng)稱為j的子表達(dá)式(subexpression)。據(jù)1第192頁的說明，是良定義的。1.18引理（1）若yÎFL(j)，則FL(y)ÍFL(j)。（2）若yÎFL(aj)，則FL(y)ÍFL(aj)ÈFL(j)。證明：本證明施聯(lián)立歸納于j的良建子表達(dá)式關(guān)系(well-founded subexpression relation)。在此我們只須補(bǔ)充（1）關(guān)

22、于Da的證明，其余證明參見1的引理6.1的證明。設(shè)yÎFL(Da)。要證：FL(y)ÍFL(Da)。情況1aa是原子活動(dòng)：據(jù)上一定義（4），有FL(Da)Da，所以據(jù)設(shè)定，yDa，所以FL(y)ÍFL(Da)，從而成立。情況2abÈg：據(jù)上一定義（5），有FL(D(bÈg)D(bÈg)ÈFL(Db)ÈFL(Dg)，所以據(jù)設(shè)定，下列情況之一成立：(a) yD(bÈg)，(b) yÎFL(Db)，(c) yÎFL(Dg)。若(a)成立，則易見FL(y)ÍFL(D(bÈg

23、)。若(b)成立，則據(jù)關(guān)于（1）的歸納假設(shè)，有FL(y)ÍFL(Db)。再據(jù)，有FL(y)ÍFL(D(bÈg)。若(c)成立，則據(jù)關(guān)于（1）的歸納假設(shè)，有FL(y)ÍFL(Dg)。再據(jù)，仍有FL(y)ÍFL(D(bÈg)。因此我們有。情況3ab;g：據(jù)上一定義（6），有FL(D(b;g)D(b;g)ÈFL(Db)ÈFL(Dg)，所以據(jù)設(shè)定，下列情況之一成立：(a) yD(b;g)，(b) yÎFL(Db)，(c) yÎFL(Dg)。若(a)成立，則易見FL(y)ÍFL(D(b;g)。若

24、(b)成立，則據(jù)關(guān)于（1）的歸納假設(shè)，有FL(y)ÍFL(Db)。再據(jù)，有FL(y)ÍFL(D(b;g)。若(c)成立，則據(jù)關(guān)于（1）的歸納假設(shè)，有FL(y)ÍFL(Dg)。再據(jù)，仍有FL(y)ÍFL(D(b;g)。因此我們有。情況4ab*：據(jù)上一定義（7），有FL(Db*)Db*ÈFL(Db)，所以據(jù)設(shè)定，下列情況之一成立：(a) yDb*，(b) yÎFL(Db)，若(a)成立，則易見FL(y)ÍFL(Db*)。若(b)成立，則據(jù)關(guān)于（1）的歸納假設(shè)，有FL(y)ÍFL(Db)。再據(jù)，有FL(y)ÍF

25、L(Db*)。因此我們有。1.19引理（0）jÎFL(j)。（1）若ayÎFL(j)，則yÎFL(j)。（2）若aÈbyÎFL(j)，則ay, byÎFL(j)。（3）若a;byÎFL(j)，則aby, byÎFL(j)。（4）若a*yÎFL(j)，則aa*yÎFL(j)。（5）若D(aÈb)ÎFL(j)，則Da, DbÎFL(j)。（6）若D(a;b)ÎFL(j)，則Da, DbÎFL(j)。（7）若Da*ÎFL(j)，則Da

26、6;FL(j)。證明：（據(jù)FL(j)的定義顯然有0）。如1的引理6.2的證明，我們有（1）（4）。（5）設(shè)D(aÈb)ÎFL(j)。據(jù)上一引理（1），則FL(D(aÈb)ÍFL(j)。再據(jù)1.17（5），有FL(Da), FL(Db)ÍFL(j)。再據(jù)（0），易見Da, DbÎFL(j)。（6）設(shè)D(a;b)ÎFL(j)。據(jù)上一引理（1），則FL(D(a;b)ÍFL(j)。再據(jù)1.17（6），有FL(Da), FL(Db)ÍFL(j)。再據(jù)（0），易見Da, DbÎFL(j)。（7）設(shè)Da*&#

27、206;FL(j)。據(jù)上一引理（1），則FL(Da*)ÍFL(j)。再據(jù)1.17（7），有FL(Da)ÍFL(j)。再據(jù)（0），易見DaÎFL(j)。1.20定義任給集合X，我們用Card(X)表示X的基數(shù)。任給公式j(luò)和活動(dòng)a，我們用Leng(j)和Leng(a)分別表示j和a的長度，即構(gòu)成j和a的符號(hào)的個(gè)數(shù)。1.21引理（1）對(duì)每一公式j(luò)，有Card(FL(j) £ Leng(j)。（2）對(duì)每一公式aj，有Card(FL(aj) £ Leng(a)。證明：參見1的引理6.3的證明。在此我們只補(bǔ)充關(guān)于Da的證明。我們只須證：（%）Card(FL

28、(Da) £ Leng(Da)。情況1aa是原子活動(dòng)：據(jù)1.17（4）顯然。情況2abÈg：我們有Card(FL(D(bÈg)Card(D(bÈg)ÈFL(Db)ÈFL(Dg) 據(jù)1.17（5）1+Card(FL(Db)+Card(FL(Dg) £ 1+ Leng(FL(Db)+Leng(FL(Dg) 據(jù)歸納假設(shè) £ Leng(D(bÈg)。情況3ab;g：我們有Card(FL(D(b;g)Card(D(b;g)ÈFL(Db)ÈFL(Dg) 據(jù)1.17（6）1+Card(FL(Db)+

29、Card(FL(Dg) £ 1+ Leng(FL(Db)+Leng(FL(Dg) 據(jù)歸納假設(shè) £ Leng(D(b;g)。情況4ab*：我們有Card(FL(Db*)Card(Db*ÈFL(Db) 據(jù)1.17（7）1+Card(FL(Db) £ 1+ Leng(FL(Db) 據(jù)歸納假設(shè) £ Leng(Db*)。1.22過濾定義任給模型M<W, R, >和公式j(luò)。 （1）定義W上的等價(jià)關(guān)系j 如下：任給w, uÎW，wj u Û "yÎFL(j)(wÎy Û uÎy

30、)。（2）任給wÎW，定義w相對(duì)j 的等價(jià)類為：wj uÎW：wj u。（3）定義M相對(duì)FL(j)的過濾Mj áWj, Rj, jñ如下：Wj wj ：wÎW。Raj <wj ,uj >：wRau，對(duì)每一原子活動(dòng)a；對(duì)應(yīng)復(fù)合活動(dòng)a的關(guān)系Raj 如1.11定義。pj wj ：wÎp，對(duì)每一原子公式p。說明：為了簡潔，以后在不致混淆之處，我們省略wj 的上標(biāo)j。1.23真值集定義令Mj 如上規(guī)定。定義j相對(duì)Mj 的真值集jj 如1.13。1.24過濾基本定理令<Wj , Rj , j >是模型<W, R, &

31、gt;相對(duì)FL(j)的過濾。任給w, uÎW，我們有：（0）對(duì)每一DaÎFL(j)，有wRau Ûw Raju。（1）對(duì)每一yÎFL(j)，有wÎy ÛwÎyj 。（2）對(duì)每一ayÎFL(j)，極小條件：若wRau，則w Raju。極大條件：若w Raju且wÎay，則uÎy。證明：本證明施聯(lián)立歸納于j的良建子表達(dá)式關(guān)系。在此我們只須證明（0）且補(bǔ)充（1）中關(guān)于Da的證明，其余證明參見1的引理6.4的證明。（0）任給DaÎFL(j)。下證：wRau Ûw Raju。施歸納于a

32、的結(jié)構(gòu)。情況1aa是原子活動(dòng)：據(jù)過濾定義1.23。情況2abÈg：據(jù)和1.19（5），有DbÎFL(j)，且DgÎFL(j)。所以我們有 wRbÈgu Û wRbu或wRgu 據(jù)1.11的（CH）Ûw Rbju 或w Rgju 據(jù)和歸納假設(shè) Ûw RbÈgju。 據(jù)1.22的（CH）情況3ab;g：據(jù)和1.19（6），有上述和。所以我們有 wRb;gu Û $vÎW(wRbv且vRgu) 據(jù)1.11的（CO）Û $vÎW(w Rbjv 且v Rgju) 據(jù)和歸納假設(shè) 

33、9;w Rb;gju。 據(jù)1.22的（CO）情況4ab*：據(jù)和1.19（7），有。所以我們有 wRb*uÛ $n³0$v0, vnÎW(wv0, uvn且對(duì)0£ i £n1, viRbv i+1) 據(jù)1.11的（IT）Û $n³0$v0, vnÎW(wv0, uvn且對(duì)0£ i £n1,v i Rbjv i+1) 據(jù)和歸納假設(shè) 這里的表述還可以參見文獻(xiàn)1第198頁情況5的證明。 Ûw Rb*ju。 據(jù)1.22的（IT）（1）任給。下證：wÎDa ÛwÎDa

34、j。施歸納于a的結(jié)構(gòu)。情況1aa是原子活動(dòng)：我們有 wÎDa Û $uÎW(uRaw ) 據(jù)真值集定義Û $uÎW(u Rajw ) 據(jù)和（0）ÛwÎDaj。 據(jù)真值集定義情況2abÈg：我們有 wÎD(bÈg) Û $uÎW(uRbÈgw ) 據(jù)真值集定義Û $uÎW(u RbÈgjw ) 據(jù)和（0）ÛwÎD(bÈg)j。 據(jù)真值集定義本情況也可以如下證明： wÎD(bÈg) 

35、9; wÎDb或wÎDg 據(jù)1.5（6）和可靠性定理ÛwÎDbj 或wÎDgj 據(jù)和歸納假設(shè)ÛwÎD(bÈg)j 。 據(jù)1.5（6）和可靠性定理（因?yàn)檫^濾也是模型）情況3ab;g：我們有 wÎD(b;g) Û $uÎW(uRb;gw ) 據(jù)真值集定義Û $uÎW(u Rb;gjw ) 據(jù)和（0）ÛwÎD(b;g)j 。 據(jù)真值集定義情況4ab*：我們有 wÎDb* Û $uÎW(uRb*w ) 據(jù)真值集定義Û

36、; $uÎW(u Rb*jw ) 據(jù)和（0）ÛwÎDb*j 。 據(jù)真值集定義 1.25定義（1）稱<W, R, >是（正則）非標(biāo)準(zhǔn)模型，當(dāng)且僅當(dāng)，W是非空狀態(tài)集， 是從At到P(W)中的指派映射，R是定義域?yàn)锳ction的映射：對(duì)每一aÎAction，Ra是W上的二元通達(dá)關(guān)系使得下列語義條件滿足：（CH）RaÈbRaÈRb。（CO）Ra;bRa o Rb<w, u>ÎW2：$vÎW(wRav且vRau)。（IT*）Ra*是包含Ra的自返傳遞二元關(guān)系使得下列條件滿足：a*jjÙa;a

37、*j，a*jjÙa*(j®aj)。（2）定義非標(biāo)準(zhǔn)模型M<W, R, >相對(duì)FL(j)的過濾Mj <Wj , Rj , j >如1.22。定義j相對(duì)Mj 的真值集jj 如1.13。說明：IT*是模型條件，而不是框架條件。另外，要注意，非標(biāo)準(zhǔn)模型的過濾仍滿足框架條件IT，所以非標(biāo)準(zhǔn)模型的過濾是標(biāo)準(zhǔn)模型。易證RDA的內(nèi)定理集Th(RDA)相對(duì)非標(biāo)準(zhǔn)模型仍有效。1.26非標(biāo)準(zhǔn)模型的過濾基本定理令<Wj , Rj , j >是模型<W, R, >相對(duì)FL(j)的過濾。任給w, uÎW，我們有：（0）對(duì)每一DaÎFL

38、(j)，有wRau Ûw Raju。（1）對(duì)每一yÎFL(j)，有wÎy ÛwÎyj 。（2）對(duì)每一ayÎFL(j)，極小條件：若wRau，則w Raju。極大條件：若w Raju且wÎay，則uÎy。證明：證明（0）和（1）關(guān)于Da的部分恰如1.24，其余證明參見1的引理6.6的證明。1.27定義令w是公式集。（1）稱w是一致集，當(dāng)且僅當(dāng)，對(duì)所有有窮公式序列j1, jnÎw，有 Ø(j1ÙÙjn)。（2）稱w是極大集，當(dāng)且僅當(dāng)，對(duì)所有jÎForm，有jÎ

39、w或ØjÎw。（3）稱w是極大一致集，當(dāng)且僅當(dāng)，w既是一致的又是極大的。（4）稱RDA是一致系統(tǒng)，當(dāng)且僅當(dāng)，Th(RDA)一致。1.28引理RDA一致。證明：假設(shè)RDA不一致。則Th(RDA)不一致，所以存在公式序列j1, jnÎTh(RDA)使得 Ø(j1ÙÙjn)。因?yàn)閖1, jnÎTh(RDA)，所以 j1ÙÙjn。據(jù)定義1.9，RDA不協(xié)調(diào)，矛盾于1.10。因?yàn)镽DA是PC的擴(kuò)充，所以如通常證明，我們可以得到下面兩個(gè)引理（包括1.31）。1.29引理令w是公式集。（1）若w極大一致。則Ø

40、jÎw Û jÏw，jÙyÎw Û jÎw且yÎw， jÚyÎw Û jÎw或yÎw，jÎw且 j®y Þ yÎw， jÎw且j®yÎw Þ yÎw，(jÎw Þ yÎw) Û j®yÎw，(jÎw Û yÎw) Û j«yÎw，Th(RDA)Íw。

41、（2）若 j，則存在極大一致集w使得jÏw。（3）j屬于每一以w為子集的極大一致集 Û 存在j1, jnÎw使得 j1ÙÙjn®j。（4）（Lindenbaum-引理）令w一致。則存在極大一致集u使得wÍu。1.30定義|j|:w：w是極大一致集使得jÎw。1.31引理令W是所有極大一致集的集合。（1）|Øj|W|j|，|jÙy|j|Ç|y|，|jÚy|j|È|y|，| |Æ，| T |W。（2）|j|Ç|j®y|Í|y|。（

42、3）|j®y|W Û |j|Í|y| Û j®y。（4）|j«y|W Û |j|y| Û j«y。1.32定義令w是公式集。wa:j：ajÎw，w<a>:<a>j：jÎw。1.33定義RDA的典范框架<W, R>定義為： Ww：w是極大一致集，且RRa：aÎAction，其中每一Ra<w, u>ÎW2：waÍu。RDA的典范模型<W, R, >定義為：<W, R>是RDA的典范框架，且

43、p|p|，對(duì)每一原子公式p。1.34典范框架主引理 令<W, R>是RDA的典范框架，且令wÎW。則（1）ajÎw Û "uÎW(wRau Þ jÎu)。（2）waÍu Û u<a>Íw，對(duì)所有uÎW。（3）DaÎw Û $uRaw。（4）RaÈbRaÈRb。（5）Ra;bRa o Rb。證明：（1）“Þ”：設(shè)ajÎw。任給uÎW使得wRau。因?yàn)閍jÎw且waÍu，故j&

44、#206;u。“Ü”：設(shè)：任給uÎW，若waÍu，則jÎu。這意味j屬于每一以wa為子集的極大一致集。據(jù)1.29（3），存在j1, jnÎwa使得 j1ÙÙjn®j。據(jù)1.5（3），我們有 aj1ÙÙajn®aj。 因?yàn)閍j1, ajnÎw，所以據(jù)上式和1.29（1），有ajÎw。（2）“Þ”：任給uÎW 使得waÍu。任給<a>jÎu<a>，則jÎu，所以ØjÏu。再據(jù)給

45、定waÍu，有ØjÏwa，所以aØjÏw，所以ØaØjÎw，因此據(jù)縮寫定義，有<a>jÎw?！?#220;”：任給uÎW 使得u<a>Íw。任給jÎwa，則ajÎw，所以據(jù)1.5（2），有Ø<a>ØjÎw，因此<a>ØjÏw。再據(jù)u<a>Íw，有<a>ØjÏu<a>，所以ØjÏu，因此

46、jÎu。（3）“Þ”：設(shè)DaÎw。先證：w<a>一致。假設(shè)不成立，則據(jù)1.27（1），存在<a>j1, , <a>jnÎw<a>使得 Ø(<a>j1ÙÙ<a>jn)。所以據(jù)TA和MP，有 <a>j1ÙÙ<a>jn®Ø<a>Da。據(jù)1.5（4），有 <a>(j1ÙÙjn)®Ø<a>Da。據(jù)推理規(guī)則RDa，易證 j1&#

47、217;Ùjn®ØDa。易見j1, , jnÎw，因此據(jù)，有ØDaÎw，矛盾于設(shè)定。所以成立。據(jù)和Lindenbaum-引理，有$uÎW(w<a>Íu)，再據(jù)（2），有 $uÎW(uaÍw)，因此$uRaw。“Ü”：設(shè)DaÏw。只須證：$uRaw。假設(shè)$uRaw，即$uÎW(uaÍw)。因?yàn)镈aÏw，所以DaÏua，因此aDaÏu。矛盾于公理aDa屬于u。（4）（5）據(jù)公理AÈ和A;。具體證明請參見1的引

48、理7.4的(i)(ii)。1.35定理RDA的典范模型是非標(biāo)準(zhǔn)模型。證明：令M<W, R, >是RDA的典范模型。據(jù)1.29（1）和上一主引理，我們看到聯(lián)結(jié)符Ø和Ù，算子a和D的性質(zhì)如標(biāo)準(zhǔn)模型。下面只須證刻畫*-算子的公式a*j«jÙa;a*j和a*j«jÙa*(j®aj)在M中有效。據(jù)1的練習(xí)5.9，上面兩式是RDA的內(nèi)定理，所以據(jù)1.29（1），它們在M中有效。因此1.25的（IT*）成立。1.36框架完全性定理RDA相對(duì)Frame完全。證明：只須證：(%) 若 j不是RDA的內(nèi)定理，則j在Frame中某個(gè)框

49、架中不有效。設(shè)j不是RDA的內(nèi)定理。令M<W, R, >是RDA的典范模型。據(jù)設(shè)定，易證M j。令Mj <Wj , Rj , j >是M相對(duì)FL(j)的過濾，則據(jù)1.25后面的說明，Mj 是標(biāo)準(zhǔn)模型。據(jù)1.19（0），有jÎFL(j)，所以據(jù)標(biāo)準(zhǔn)模型的過濾基本定理1.24（1），有Mj j，所以我們有<Wj , Rj > j。易見<Wj , Rj >屬于Frame，所以(%)成立。結(jié)束語：RDA相對(duì)Da是極小系統(tǒng)（參見5第3節(jié)關(guān)于NAD的部分），所以我們還可以根據(jù)實(shí)際情況加以擴(kuò)充。例如，下面的公式和規(guī)則可以考慮加入RDA：（1）<

50、b>D(a;b)®Da， （2）ajÚbyD(aÈb)®jÚy。易見（1）對(duì)應(yīng)框架條件：$u(wRbu且$u0Ra;bu) Þ $w0Raw。二、合力改變狀態(tài)的邏輯本節(jié)我們要概括上節(jié)（單個(gè)主體）做了一個(gè)活動(dòng)這個(gè)概念。我們要建立邏輯GDA來刻畫下列概念：若干主體做了若干活動(dòng)形成合力改變一個(gè)狀態(tài)。我們用Aa表示主體A做了活動(dòng)a（Aa是對(duì)前面的Da的相對(duì)化）?！癆a在w中成立”的點(diǎn)框架條件相對(duì)化為$uRaAw，它直觀表示：存在初始狀態(tài)u，A在其中做了a從而把u改變?yōu)闋顟B(tài)w。現(xiàn)在我們要考慮的是這種情況（簡單但又是本質(zhì)）的概括（概括到多主

51、體）：2個(gè)主體做了2個(gè)活動(dòng)共同把初始狀態(tài)u改變?yōu)闋顟B(tài)w。這就是我們所謂合力改變狀態(tài)的含義。為了節(jié)省篇幅，以下我們不考慮復(fù)合活動(dòng)的情況，讀者可以按上節(jié)內(nèi)容做相應(yīng)的推廣。另一方面，前面有些定義和結(jié)果對(duì)PC的每一擴(kuò)充都適用，而下面（包括以后幾節(jié)）我們建立的邏輯都是PC的擴(kuò)充，所以我們省略不提，希望讀者閱讀時(shí)注意。2.1公式的形成規(guī)則令A(yù)t和Act如上節(jié)規(guī)定。本文我們用Agent表示有窮多個(gè)主體的集合。歸納定義所有公式j(luò)的集合Form如下：j:p½Øj½(jÙy)½aAj½AaBb， 其中pÎAt，A, BÎAgent和a

52、, bÎAct。說明：aAj的直觀意義是：主體A做的活動(dòng)a使j必然成立。AaBb的直觀意義是：主體A和B分別同時(shí)做了活動(dòng)a和b。AaBb可以自然地概括到A1a1Anan，其中A1, , AnÎAgent。因此本節(jié)我們得到的結(jié)果也可以自然地概括到關(guān)于A1a1Anan的結(jié)果。注意：A1a1Anan的直觀意義是：主體A1, , An分別同時(shí)做了活動(dòng)a1, , an。2.2規(guī)定 當(dāng)AB且ab時(shí)，我們用Aa縮寫AaBb。2.3定義合力系統(tǒng)GDA定義如下：對(duì)所有A, BÎAgent，a, bÎAct和j, yÎForm，TA和MP如前定義，（KaA） aA

53、(j®y)®aAj®aAy，（DIS） aA(AaBb)ÚbB(AaBb)，（RNaA） jaAj，（RG） aAjÚbByAaBb®jÚy。說明：公理DIS和規(guī)則RG包含兩類模式：（可能不同的）主體和（可能不同的）活動(dòng)，RG還包含（可能不同的）命題。2.4引理下面是GDA的導(dǎo)出規(guī)則和內(nèi)定理：（1）j®yaAj®aAy，j®y<aA>j®<aA>y。（2）aAj«Ø<aA>Øj。 （3）j1ÙÙjn&

54、#174;jaAj1ÙÙaAjn®aAj。（4）<aA>(j1ÙÙjn)®<aA>j1ÙÙ<aA>jn。（5）aAjÚaAyAa®jÚy，aAjAa®j， Ø(<aA>jÙ<bB>y)jÙy®Ø(AaBb。（6）aA(AaAb)ÚbA(AaAb)，aAAa。（7）AaAb®AaÙAb。（8）AaBb®BbAa，AaBb«

55、;BbAa。證明：據(jù)Ka A和RNa A易得（1）（4）。據(jù)RG和2.2易得（5）。據(jù)DIS易得（6）。證（7）：據(jù)（6），有 aAAa，所以 aAAaÚbB Aa，故據(jù)RG，有 AaBb®Aa。據(jù)對(duì)稱性，同理可證 AaBb®Bb。證（8）：據(jù)DIS，我們有 bB(BbAa)ÚaA(BbAa)。因此有 aA(BbAa)ÚbB(BbAa)再據(jù)RG，易得 AaBb®BbAa。說明：據(jù)后面的2.10，（7）的逆不是內(nèi)定理，從而聯(lián)結(jié)符不會(huì)退化為Ù。2.5定義定義從Form到不含模態(tài)算子的子語言Form0ÍForm的翻譯映射

56、t如下：t(p)p，對(duì)所有pÎAt；t(Øj)Øt(j)；t(jÙy)t(j)Ùt(y)；t(aAj)t(j)；t(AaBb)T。如前定義t-翻譯，t-退化和協(xié)調(diào)概念，易證：2.6定理GDA能t-退化為PC0且GDA是協(xié)調(diào)的。2.7定義稱<W, R>是框架，當(dāng)且僅當(dāng)，W是非空狀態(tài)集，R是定義域?yàn)锳ct´Agent的映射：對(duì)每一aÎAct和AÎAgent，RaA是W上的二元通達(dá)關(guān)系使得下列框架條件滿足：對(duì)每一wÎW，（*）"vÎW(wRaAv Þ $uÎW

57、(uRaAv且uRbBv)或"vÎW(wRbBv Þ $uÎW(uRaAv且uRbBv)。本節(jié)把所有如上定義的框架的類記作Frame。注意：RaA是R(a, A)的縮寫。以后我們也用定義：RaA(w) :uÎW：wRaAu。2.8真值集定義定義j相對(duì)<W, R, >的真值集j如下：對(duì)所有wÎW，A, BÎAgent，a, bÎAct和j, yÎForm，（1）wÎØj Û wÏj，（2）wÎjÙy Û wÎj且w&

58、#206;y，（3）wÎaAj Û RaA(w)Íj， （4）wÎAaBb Û $uÎW(uRaAw且uRbBw)。說明：（4）還可以簡單表示為：wÎAaBb Û $uRaAÇRbBw。2.9框架可靠性定理GDA相對(duì)Frame可靠。證明：任給框架F<W, R>和F上賦值 。這里只驗(yàn)證DIS和RG。驗(yàn)證DIS：任給wÎW，據(jù)2.7的（*），我們有"vÎW(wRaAv Þ $uÎW(uRaAv且uRbBv)或"vÎW(wRbBv

59、 Þ $uÎW(uRaAv且uRbBv)。據(jù)真值集定義（4），我們有"vÎW(wRaAv Þ vÎAaBb)或"vÎW(wRbBv Þ vÎAaBb)。再據(jù)真值集定義（3），易見wÎaA(AaBb)ÚbB(AaBb)。驗(yàn)證RG：設(shè)aAjÚbByW。只須證：AaBbÍjÚy。任給wÎAaBb，據(jù)真值集定義（4），有（）$uÎW(uRaAw且uRbBw)。而據(jù)設(shè)定，有uÎaAjÚbBy。再據(jù)（）和真值集定義（3

60、），易見wÎjÚy。2.10反例AaÙAb®AaAb不是GDA的內(nèi)定理。證明：因?yàn)?uÎW(uRaAw)且$uÎW(uRbBw)一般不蘊(yùn)涵$uÎW(uRaAw且uRbBw)，所以我們很容易構(gòu)造一個(gè)框架F使得AaÙAb®AaAb在F中不有效。再據(jù)框架可靠性定理，易見要證結(jié)果成立。令w是公式集。waA:j：aAjÎw， w<aA>:<aA>j：jÎw。2.11定義GDA的典范框架F<W, R>定義為： Ww：w是極大一致集，且RRaA：aÎAc

61、t且AÎAgent，其中每一RaA<w, u>ÎW2：waAÍu。2.12典范框架主引理 令<W, R>是GDA的典范框架，且令wÎW。則（1）aAjÎw Û "uÎW(wRaAu Þ jÎu)。（2）waAÍu Û u<aA>Íw，對(duì)所有uÎW。（3）AaBbÎw Û $uÎW(uRaAw且uRbBw)。證明：（1）和（2）的證明類似1.34的（1）和（2）的證明。（3）“Þ”：

62、設(shè)AaBbÎw。據(jù)Lindenbaum-引理和（2），只須證w<aA>È w<bB>一致。假設(shè)要證結(jié)果不成立，則存在<aA>j1, , <aA>jnÎw<aA>和<bB>y1, , <bB>ymÎw<bB>使得 Ø(<aA>j1ÙÙ<aA>jnÙ<bB>y1ÙÙ<bB>ym)。據(jù)2.4（4），有 Ø(<aA>(j1Ù

63、17;jn)Ù<bB>(y1ÙÙym)。再據(jù)2.4（5），有 j1ÙÙjnÙy1ÙÙym®Ø(AaBb)。易見j1, , jn, y1, , ymÎw，因此據(jù)，有Ø(AaBb)Îw，矛盾于設(shè)定。“Ü”：設(shè)AaBbÏw。只須證：$uÎW(uRaAw且uRbBw)，即要證："uÎW(uRaAw或uRbBw)。任給uÎW使得uRaAw，要證uRbBw，為此只須證：存在公式j(luò)使得jÎubB但&

64、#216;jÎw。因?yàn)锳aBbÏw，因此Ø(AaBb)Îw，故<aA>Ø(AaBb)Îw<aA>。因?yàn)閡RaAw，故據(jù)（2），有w<aA>Íu，因此<aA>Ø(AaBb)Îu，再據(jù)公理DIS，易得bB(AaBb)Îu，所以AaBbÎubB，再據(jù)，易得。2.13典范模型基本定理令<W, R, >是GDA的典范模型。jÎw Û wÎj，對(duì)每一wÎW和公式j(luò)。證明：施歸納于j的結(jié)構(gòu)。只考慮下面情況，其余情況易證。情況1jaAy：易見 aAyÎw Û "uÎW(wRaAu Þ yÎu) 據(jù)上一引理（1）Û "uÎW(wRaAu Þ uÎ|y|) 據(jù)1.30Û "uÎW(wRaAu Þ uÎy) 據(jù)歸納假設(shè)Û wÎaAy。 據(jù)真值集定義情況2jAaBb：我們