动态认知逻辑的几个应用

1、动态认知逻辑的几个应用 收稿日期：2006-1-10基金项目：本文得到教育部基地重大项目归纳逻辑及其应用（项目编号05JJD720.40001）和教育部哲学社会科学研究重大课题攻关项目 (04JZD0006) 的资助。作者简介：李小五(1955-)，男，河北人，中山大学教授，北京书生公司书生研究中心客座研究员。电子邮箱：LXW121李小五(中山大学逻辑与认知研究所，广东 广州 510275)内容提要：我们建立若干逻辑分别刻画下列概念：做了一个活动、若干主体做了若干活动形成合力改变一个状态、知道一个主体、知道一个性质与知道一个关系。关键词：做了一个活动；合力改变一个状态；知道一个主体；知道一个性

2、质与知道一个关系中图分类号：B81 文献标识码：A一、正则做活动逻辑通常的动态逻辑在语形方面（相对公理化系统）没有独立刻画做了一个活动的逻辑性质。例如，没有刻画像“我吃了”那样的句子。也就是说，相对活动a，它们只刻画了形如aj的句子，而这样的句子只是间接刻画了活动a。至于像“我吃了”那样的句子（概括为“（某主体）做了活动a”，符号化为Da）有什么逻辑性质，这些逻辑没有揭示。而在我们看来，这是一类很重要的句子。为了简洁，本节我们只研究单主体逻辑。我们逻辑的基础是文献1提到的PDL和9提到的DA1。1.1公式的形成规则令Atp1, pn,是可数无穷多个原子公式的集合，令Acta1, am,是可数无

3、穷多个原子活动的集合。联立归纳定义所有公式j的集合Form和所有活动a的集合Action如下：j:p½Øj½(jÙy)½aj½Da， 其中pÎAt；a:a½(aÈb)½(a;b)½a*， 其中aÎAct。说明：据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*统称为复合活动（运算），其中aÈb称为“复合a和b的选择活动”，a;b称为“复合a和b的相继活动”，a*称为“a的（有穷）叠加活动”。Da的直观意义是： “（主体）做了活动a”（The action a has been executed (by the agent)）。这是我们的逻辑主要要刻画的公式。1

5、.2规定与缩写 联结符Ú，®和«的缩写定义如通常给出。另外，缩写定义<a>j:ØaØj。为了叙述方便，我们规定联结符的结合力从左到右依次减弱：Ø，a，D，Ù，Ú，®，«。此外，我们规定同形联结符满足右向结合原则。例如，j®y®q表示j®(y®q)。T定义为p1ÚØp1， 定义为ØT。我们常用Û表示“当且仅当”，用Þ表示“若，则”，用表示“并非”。1.3定义正则系统RDA定义如下：对所有a, b&

6、#206;Action，j, yÎForm，（TA） 所有重言式的代入特例，（Ka） a(j®y)®aj®ay，（Da） aDa， （活动公理）（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、（活动规则）说明：公理Da和规则RDa刻画了做活动概念的基本特性，公理AÈ和A;分别刻画了复合活动运算aÈb和a;b的基本特性，公理IA*和IA*刻画了复合活动运算a*的基本特性。文献2称刻画aÈb，a;b和a*的动态逻辑为正则逻辑，而在1，还要加上刻画测试运算j?的公理j?y«(j®y)才能称为正则逻辑。这里我们遵从2的称谓，因为增加测试运算无法证明下面系统的框架可靠性定理和框架完全性定理，而这是逻辑追求的重要目标。另一方面，从测试公理j?y«(j®y)和活动公理Da易得j®D(j?)。而后者的直观意义是：每一真

8、命题都被（主体）测试过。在我们看来这似乎不自然。由TA和MP构成的系统称为经典句子系统，记为PC。我们也用PC0表示用不含模态算子a的语言表述的PC。1.4定义我们用 j 表示j是RDA的内定理：j在RDA中有一个形式证明。RDA的全体内定理的集合记为Th(RDA)。我们也用 j 表示jÏTh(RDA)。1.5引理下面是RDA的导出规则和内定理：（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）据Ka和RNa如通常所证。（5） aj 假设 <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）据叠加公理，有a*Da*®Da*，再据活动公理Da，易得要证结果。说明：初看到（9）令人惊讶，但仔细一想还是很自然的。对当下主体来说，它在任何情况下总是做了若干次活动a（因为其中也包括0次）。1.6定义定义从Form到不含模态算子的子语言Form0ÍForm的翻译映射t如下：t(p)p，对所有原子公式pÎAt；t(Øj)Øt(j)；t(jÙy)t(j)Ùt(y)；t(aj)t(j)；t(Da)T。对每一公式jÎFor

12、m，我们称t(j)是j的t-翻译。1.7定义令S1和S2是任意两个公理化系统。我们称S1能t-退化为S2，当且仅当，S1的所有内定理的t-翻译是S2的内定理。1.8翻译定理RDA能t-退化为PC0。证明：据上面的定义，证明显然。1.9定义称系统S是协调系统，当且仅当，不存在j使得j和Øj都是S的内定理。1.10定理RDA是协调的。证明：假设RDA不协调，则存在j使得j和Øj都是RDA的内定理。据上面的翻译定理，t(j)和Øt(j)都是PC0的内定理，矛盾于PC0的协调性。1.11定义（1）称<W, R>是（正则）框架，当且仅当，W是非空状态集，R是定义

13、域为Action的映射：对每一aÎAction，Ra是W上的二元通达关系使得下列框架条件满足： 其中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且对0£ i £n1, <vi, v i+1>ÎRa)。本节把所有（正则

14、）框架的类记作Frame。（2）称<W, R, >是模型，当且仅当，<W, R>是框架且 是从At到W的幂集P(W)中的指派映射。这里， 也称为框架<W, R>上的指派映射。说明：CH是choice的缩写，CO是composition的缩写，IT是iteration的缩写。IT等号右边的集合通常记作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-左持续的。1.13真值集定义令M<W, R, >是模型。定义j相对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表示：存在初始状态u使得（主体）在其中做了a从而把u改变为状态w，这正是我们说在w中（

16、主体）做了a的意思。注意：$uRaw是点框架条件：Da在w的真值只取决于w是否有a-左持续性。据上述语义，特别是（4），易见Da*在任何wÎW中成立（这对应前面Da*是内定理），但存在uÎW使得Da在u中不成立，也存在vÎW使得Da在v中成立但D(a;a)在v中不成立。下面的引理据真值集定义的（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，Û 对F上的任意指派映射 ，有jW；否则称j在F中不有效，记为F j。称规则j1, jny相对M保持有效性 Û 若j1jnW，则yW 。1.16框架可靠性定理RDA相对Frame可靠。证明：任给框架F<W, R>和F上赋值 。下面验证RDA的公理相对M<F, >有效且RDA的推理规则相对M保持有效

18、性。公理TA和Ka，规则MP和RNa的验证如通常。AÈ, A;, A*和IA*的验证参见1的定理5.8(ii)，5.10(ii)，5.15(ix)和(xi)。验证Da：假设aDa在M中不有效，则存在wÎW使得wÏaDa。据真值集定义，我们有Ra(w) Da，所以存在vÎW使得wRav且vÏDa。据后者和真值集定义，我们有$uRav，矛盾于wRav。验证RDa：设<a>DaÍaj。需证：DaÍj。任给wÎDa，据真值集定义，有$uRaw，再据uRaw 和wÎDa，有uÎ<a>

19、;Da。再据设定，有uÎaj，再据uRaw，有wÎj。因为RDA是PDL的扩充，所以根据活动和公式的联立归纳法（据1.1）和*-算子的特性（据公理A*和IA*以及1.11（IT），我们不能用通常的典范模型方法证明RDA的框架完全性定理，而是要用过滤方法，为此我们先要定义FL-闭包作为过滤器。1.17定义联立归纳定义函数FL和FL如下：（1）FL(p)p，对所有原子公式pÎAt；（2）FL(Øj)ØjÈFL(j)；（3）FL(jÙy)jÙyÈFL(j)ÈFL(y)；（4）FL(Da)Da，对所有原

20、子活动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，对所有原子活动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-闭包。 严格说，1给出的FL-闭包是没有上述（4）（6）的。 FL(j)中的公式和活动称为j的子表达式(subexpression)。据1第192页的说明，是良定义的。1.18引理（1）若yÎFL(j)，则FL(y)ÍFL(j)。（2）若yÎFL(aj)，则FL(y)ÍFL(aj)ÈFL(j)。证明：本证明施联立归纳于j的良建子表达式关系(well-founded subexpression relation)。在此我们只须补充（1）关

22、于Da的证明，其余证明参见1的引理6.1的证明。设yÎFL(Da)。要证：FL(y)ÍFL(Da)。情况1aa是原子活动：据上一定义（4），有FL(Da)Da，所以据设定，yDa，所以FL(y)ÍFL(Da)，从而成立。情况2abÈg：据上一定义（5），有FL(D(bÈg)D(bÈg)ÈFL(Db)ÈFL(Dg)，所以据设定，下列情况之一成立：(a) yD(bÈg)，(b) yÎFL(Db)，(c) yÎFL(Dg)。若(a)成立，则易见FL(y)ÍFL(D(bÈg

23、)。若(b)成立，则据关于（1）的归纳假设，有FL(y)ÍFL(Db)。再据，有FL(y)ÍFL(D(bÈg)。若(c)成立，则据关于（1）的归纳假设，有FL(y)ÍFL(Dg)。再据，仍有FL(y)ÍFL(D(bÈg)。因此我们有。情况3ab;g：据上一定义（6），有FL(D(b;g)D(b;g)ÈFL(Db)ÈFL(Dg)，所以据设定，下列情况之一成立：(a) yD(b;g)，(b) yÎFL(Db)，(c) yÎFL(Dg)。若(a)成立，则易见FL(y)ÍFL(D(b;g)。若

24、(b)成立，则据关于（1）的归纳假设，有FL(y)ÍFL(Db)。再据，有FL(y)ÍFL(D(b;g)。若(c)成立，则据关于（1）的归纳假设，有FL(y)ÍFL(Dg)。再据，仍有FL(y)ÍFL(D(b;g)。因此我们有。情况4ab*：据上一定义（7），有FL(Db*)Db*ÈFL(Db)，所以据设定，下列情况之一成立：(a) yDb*，(b) yÎFL(Db)，若(a)成立，则易见FL(y)ÍFL(Db*)。若(b)成立，则据关于（1）的归纳假设，有FL(y)ÍFL(Db)。再据，有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)。证明：（据FL(j)的定义显然有0）。如1的引理6.2的证明，我们有（1）（4）。（5）设D(aÈb)ÎFL(j)。据上一引理（1），则FL(D(aÈb)ÍFL(j)。再据1.17（5），有FL(Da), FL(Db)ÍFL(j)。再据（0），易见Da, DbÎFL(j)。（6）设D(a;b)ÎFL(j)。据上一引理（1），则FL(D(a;b)ÍFL(j)。再据1.17（6），有FL(Da), FL(Db)ÍFL(j)。再据（0），易见Da, DbÎFL(j)。（7）设Da*&#

27、206;FL(j)。据上一引理（1），则FL(Da*)ÍFL(j)。再据1.17（7），有FL(Da)ÍFL(j)。再据（0），易见DaÎFL(j)。1.20定义任给集合X，我们用Card(X)表示X的基数。任给公式j和活动a，我们用Leng(j)和Leng(a)分别表示j和a的长度，即构成j和a的符号的个数。1.21引理（1）对每一公式j，有Card(FL(j) £ Leng(j)。（2）对每一公式aj，有Card(FL(aj) £ Leng(a)。证明：参见1的引理6.3的证明。在此我们只补充关于Da的证明。我们只须证：（%）Card(FL

28、(Da) £ Leng(Da)。情况1aa是原子活动：据1.17（4）显然。情况2abÈg：我们有Card(FL(D(bÈg)Card(D(bÈg)ÈFL(Db)ÈFL(Dg) 据1.17（5）1+Card(FL(Db)+Card(FL(Dg) £ 1+ Leng(FL(Db)+Leng(FL(Dg) 据归纳假设 £ Leng(D(bÈg)。情况3ab;g：我们有Card(FL(D(b;g)Card(D(b;g)ÈFL(Db)ÈFL(Dg) 据1.17（6）1+Card(FL(Db)+

29、Card(FL(Dg) £ 1+ Leng(FL(Db)+Leng(FL(Dg) 据归纳假设 £ Leng(D(b;g)。情况4ab*：我们有Card(FL(Db*)Card(Db*ÈFL(Db) 据1.17（7）1+Card(FL(Db) £ 1+ Leng(FL(Db) 据归纳假设 £ Leng(Db*)。1.22过滤定义任给模型M<W, R, >和公式j。 （1）定义W上的等价关系j 如下：任给w, uÎW，wj u Û "yÎFL(j)(wÎy Û uÎy

30、)。（2）任给wÎW，定义w相对j 的等价类为：wj uÎW：wj u。（3）定义M相对FL(j)的过滤Mj áWj, Rj, jñ如下：Wj wj ：wÎW。Raj <wj ,uj >：wRau，对每一原子活动a；对应复合活动a的关系Raj 如1.11定义。pj wj ：wÎp，对每一原子公式p。说明：为了简洁，以后在不致混淆之处，我们省略wj 的上标j。1.23真值集定义令Mj 如上规定。定义j相对Mj 的真值集jj 如1.13。1.24过滤基本定理令<Wj , Rj , j >是模型<W, R, &

31、gt;相对FL(j)的过滤。任给w, uÎW，我们有：（0）对每一DaÎFL(j)，有wRau Ûw Raju。（1）对每一yÎFL(j)，有wÎy ÛwÎyj 。（2）对每一ayÎFL(j)，极小条件：若wRau，则w Raju。极大条件：若w Raju且wÎay，则uÎy。证明：本证明施联立归纳于j的良建子表达式关系。在此我们只须证明（0）且补充（1）中关于Da的证明，其余证明参见1的引理6.4的证明。（0）任给DaÎFL(j)。下证：wRau Ûw Raju。施归纳于a

32、的结构。情况1aa是原子活动：据过滤定义1.23。情况2abÈg：据和1.19（5），有DbÎFL(j)，且DgÎFL(j)。所以我们有 wRbÈgu Û wRbu或wRgu 据1.11的（CH）Ûw Rbju 或w Rgju 据和归纳假设 Ûw RbÈgju。 据1.22的（CH）情况3ab;g：据和1.19（6），有上述和。所以我们有 wRb;gu Û $vÎW(wRbv且vRgu) 据1.11的（CO）Û $vÎW(w Rbjv 且v Rgju) 据和归纳假设 

33、9;w Rb;gju。 据1.22的（CO）情况4ab*：据和1.19（7），有。所以我们有 wRb*uÛ $n³0$v0, vnÎW(wv0, uvn且对0£ i £n1, viRbv i+1) 据1.11的（IT）Û $n³0$v0, vnÎW(wv0, uvn且对0£ i £n1,v i Rbjv i+1) 据和归纳假设 这里的表述还可以参见文献1第198页情况5的证明。 Ûw Rb*ju。 据1.22的（IT）（1）任给。下证：wÎDa ÛwÎDa

34、j。施归纳于a的结构。情况1aa是原子活动：我们有 wÎDa Û $uÎW(uRaw ) 据真值集定义Û $uÎW(u Rajw ) 据和（0）ÛwÎDaj。 据真值集定义情况2abÈg：我们有 wÎD(bÈg) Û $uÎW(uRbÈgw ) 据真值集定义Û $uÎW(u RbÈgjw ) 据和（0）ÛwÎD(bÈg)j。 据真值集定义本情况也可以如下证明： wÎD(bÈg) 

35、9; wÎDb或wÎDg 据1.5（6）和可靠性定理ÛwÎDbj 或wÎDgj 据和归纳假设ÛwÎD(bÈg)j 。 据1.5（6）和可靠性定理（因为过滤也是模型）情况3ab;g：我们有 wÎD(b;g) Û $uÎW(uRb;gw ) 据真值集定义Û $uÎW(u Rb;gjw ) 据和（0）ÛwÎD(b;g)j 。 据真值集定义情况4ab*：我们有 wÎDb* Û $uÎW(uRb*w ) 据真值集定义Û

36、; $uÎW(u Rb*jw ) 据和（0）ÛwÎDb*j 。 据真值集定义 1.25定义（1）称<W, R, >是（正则）非标准模型，当且仅当，W是非空状态集， 是从At到P(W)中的指派映射，R是定义域为Action的映射：对每一aÎAction，Ra是W上的二元通达关系使得下列语义条件满足：（CH）RaÈbRaÈRb。（CO）Ra;bRa o Rb<w, u>ÎW2：$vÎW(wRav且vRau)。（IT*）Ra*是包含Ra的自返传递二元关系使得下列条件满足：a*jjÙa;a

37、*j，a*jjÙa*(j®aj)。（2）定义非标准模型M<W, R, >相对FL(j)的过滤Mj <Wj , Rj , j >如1.22。定义j相对Mj 的真值集jj 如1.13。说明：IT*是模型条件，而不是框架条件。另外，要注意，非标准模型的过滤仍满足框架条件IT，所以非标准模型的过滤是标准模型。易证RDA的内定理集Th(RDA)相对非标准模型仍有效。1.26非标准模型的过滤基本定理令<Wj , Rj , j >是模型<W, R, >相对FL(j)的过滤。任给w, uÎW，我们有：（0）对每一DaÎFL

38、(j)，有wRau Ûw Raju。（1）对每一yÎFL(j)，有wÎy ÛwÎyj 。（2）对每一ayÎFL(j)，极小条件：若wRau，则w Raju。极大条件：若w Raju且wÎay，则uÎy。证明：证明（0）和（1）关于Da的部分恰如1.24，其余证明参见1的引理6.6的证明。1.27定义令w是公式集。（1）称w是一致集，当且仅当，对所有有穷公式序列j1, jnÎw，有 Ø(j1ÙÙjn)。（2）称w是极大集，当且仅当，对所有jÎForm，有jÎ

39、w或ØjÎw。（3）称w是极大一致集，当且仅当，w既是一致的又是极大的。（4）称RDA是一致系统，当且仅当，Th(RDA)一致。1.28引理RDA一致。证明：假设RDA不一致。则Th(RDA)不一致，所以存在公式序列j1, jnÎTh(RDA)使得 Ø(j1ÙÙjn)。因为j1, jnÎTh(RDA)，所以 j1ÙÙjn。据定义1.9，RDA不协调，矛盾于1.10。因为RDA是PC的扩充，所以如通常证明，我们可以得到下面两个引理（包括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|，对每一原子公式p。1.34典范框架主引理 令<W, R>是RDA的典范框架，且令wÎW。则（1）ajÎw Û "uÎW(wRau Þ jÎu)。（2）waÍu Û u<a>Íw，对所有uÎW。（3）DaÎw Û $uRaw。（4）RaÈbRaÈRb。（5）Ra;bRa o Rb。证明：（1）“Þ”：设ajÎw。任给uÎW使得wRau。因为ajÎw且waÍu，故j&

44、#206;u。“Ü”：设：任给uÎW，若waÍu，则jÎu。这意味j属于每一以wa为子集的极大一致集。据1.29（3），存在j1, jnÎwa使得 j1ÙÙjn®j。据1.5（3），我们有 aj1ÙÙajn®aj。 因为aj1, ajnÎw，所以据上式和1.29（1），有ajÎw。（2）“Þ”：任给uÎW 使得waÍu。任给<a>jÎu<a>，则jÎu，所以ØjÏu。再据给

45、定waÍu，有ØjÏwa，所以aØjÏw，所以ØaØjÎw，因此据缩写定义，有<a>jÎw。“Ü”：任给uÎW 使得u<a>Íw。任给jÎwa，则ajÎw，所以据1.5（2），有Ø<a>ØjÎw，因此<a>ØjÏw。再据u<a>Íw，有<a>ØjÏu<a>，所以ØjÏu，因此

46、jÎu。（3）“Þ”：设DaÎw。先证：w<a>一致。假设不成立，则据1.27（1），存在<a>j1, , <a>jnÎw<a>使得 Ø(<a>j1ÙÙ<a>jn)。所以据TA和MP，有 <a>j1ÙÙ<a>jn®Ø<a>Da。据1.5（4），有 <a>(j1ÙÙjn)®Ø<a>Da。据推理规则RDa，易证 j1&#

47、217;Ùjn®ØDa。易见j1, , jnÎw，因此据，有ØDaÎw，矛盾于设定。所以成立。据和Lindenbaum-引理，有$uÎW(w<a>Íu)，再据（2），有 $uÎW(uaÍw)，因此$uRaw。“Ü”：设DaÏw。只须证：$uRaw。假设$uRaw，即$uÎW(uaÍw)。因为DaÏw，所以DaÏua，因此aDaÏu。矛盾于公理aDa属于u。（4）（5）据公理AÈ和A;。具体证明请参见1的引

48、理7.4的(i)(ii)。1.35定理RDA的典范模型是非标准模型。证明：令M<W, R, >是RDA的典范模型。据1.29（1）和上一主引理，我们看到联结符Ø和Ù，算子a和D的性质如标准模型。下面只须证刻画*-算子的公式a*j«jÙa;a*j和a*j«jÙa*(j®aj)在M中有效。据1的练习5.9，上面两式是RDA的内定理，所以据1.29（1），它们在M中有效。因此1.25的（IT*）成立。1.36框架完全性定理RDA相对Frame完全。证明：只须证：(%) 若 j不是RDA的内定理，则j在Frame中某个框

49、架中不有效。设j不是RDA的内定理。令M<W, R, >是RDA的典范模型。据设定，易证M j。令Mj <Wj , Rj , j >是M相对FL(j)的过滤，则据1.25后面的说明，Mj 是标准模型。据1.19（0），有jÎFL(j)，所以据标准模型的过滤基本定理1.24（1），有Mj j，所以我们有<Wj , Rj > j。易见<Wj , Rj >属于Frame，所以(%)成立。结束语：RDA相对Da是极小系统（参见5第3节关于NAD的部分），所以我们还可以根据实际情况加以扩充。例如，下面的公式和规则可以考虑加入RDA：（1）<

50、b>D(a;b)®Da， （2）ajÚbyD(aÈb)®jÚy。易见（1）对应框架条件：$u(wRbu且$u0Ra;bu) Þ $w0Raw。二、合力改变状态的逻辑本节我们要概括上节（单个主体）做了一个活动这个概念。我们要建立逻辑GDA来刻画下列概念：若干主体做了若干活动形成合力改变一个状态。我们用Aa表示主体A做了活动a（Aa是对前面的Da的相对化）。“Aa在w中成立”的点框架条件相对化为$uRaAw，它直观表示：存在初始状态u，A在其中做了a从而把u改变为状态w。现在我们要考虑的是这种情况（简单但又是本质）的概括（概括到多主

51、体）：2个主体做了2个活动共同把初始状态u改变为状态w。这就是我们所谓合力改变状态的含义。为了节省篇幅，以下我们不考虑复合活动的情况，读者可以按上节内容做相应的推广。另一方面，前面有些定义和结果对PC的每一扩充都适用，而下面（包括以后几节）我们建立的逻辑都是PC的扩充，所以我们省略不提，希望读者阅读时注意。2.1公式的形成规则令At和Act如上节规定。本文我们用Agent表示有穷多个主体的集合。归纳定义所有公式j的集合Form如下：j:p½Øj½(jÙy)½aAj½AaBb， 其中pÎAt，A, BÎAgent和a

52、, bÎAct。说明：aAj的直观意义是：主体A做的活动a使j必然成立。AaBb的直观意义是：主体A和B分别同时做了活动a和b。AaBb可以自然地概括到A1a1Anan，其中A1, , AnÎAgent。因此本节我们得到的结果也可以自然地概括到关于A1a1Anan的结果。注意：A1a1Anan的直观意义是：主体A1, , An分别同时做了活动a1, , an。2.2规定 当AB且ab时，我们用Aa缩写AaBb。2.3定义合力系统GDA定义如下：对所有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和规则RG包含两类模式：（可能不同的）主体和（可能不同的）活动，RG还包含（可能不同的）命题。2.4引理下面是GDA的导出规则和内定理：（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。证明：据Ka A和RNa A易得（1）（4）。据RG和2.2易得（5）。据DIS易得（6）。证（7）：据（6），有 aAAa，所以 aAAaÚbB Aa，故据RG，有 AaBb®Aa。据对称性，同理可证 AaBb®Bb。证（8）：据DIS，我们有 bB(BbAa)ÚaA(BbAa)。因此有 aA(BbAa)ÚbB(BbAa)再据RG，易得 AaBb®BbAa。说明：据后面的2.10，（7）的逆不是内定理，从而联结符不会退化为Ù。2.5定义定义从Form到不含模态算子的子语言Form0ÍForm的翻译映射

56、t如下：t(p)p，对所有pÎAt；t(Øj)Øt(j)；t(jÙy)t(j)Ùt(y)；t(aAj)t(j)；t(AaBb)T。如前定义t-翻译，t-退化和协调概念，易证：2.6定理GDA能t-退化为PC0且GDA是协调的。2.7定义称<W, R>是框架，当且仅当，W是非空状态集，R是定义域为Act´Agent的映射：对每一aÎAct和AÎAgent，RaA是W上的二元通达关系使得下列框架条件满足：对每一wÎW，（*）"vÎW(wRaAv Þ $uÎW

57、(uRaAv且uRbBv)或"vÎW(wRbBv Þ $uÎW(uRaAv且uRbBv)。本节把所有如上定义的框架的类记作Frame。注意：RaA是R(a, A)的缩写。以后我们也用定义：RaA(w) :uÎW：wRaAu。2.8真值集定义定义j相对<W, R, >的真值集j如下：对所有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相对Frame可靠。证明：任给框架F<W, R>和F上赋值 。这里只验证DIS和RG。验证DIS：任给wÎW，据2.7的（*），我们有"vÎW(wRaAv Þ $uÎW(uRaAv且uRbBv)或"vÎW(wRbBv

59、 Þ $uÎW(uRaAv且uRbBv)。据真值集定义（4），我们有"vÎW(wRaAv Þ vÎAaBb)或"vÎW(wRbBv Þ vÎAaBb)。再据真值集定义（3），易见wÎaA(AaBb)ÚbB(AaBb)。验证RG：设aAjÚbByW。只须证：AaBbÍjÚy。任给wÎAaBb，据真值集定义（4），有（）$uÎW(uRaAw且uRbBw)。而据设定，有uÎaAjÚbBy。再据（）和真值集定义（3

60、），易见wÎjÚy。2.10反例AaÙAb®AaAb不是GDA的内定理。证明：因为$uÎW(uRaAw)且$uÎW(uRbBw)一般不蕴涵$uÎW(uRaAw且uRbBw)，所以我们很容易构造一个框架F使得AaÙAb®AaAb在F中不有效。再据框架可靠性定理，易见要证结果成立。令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，对所有uÎW。（3）AaBbÎw Û $uÎW(uRaAw且uRbBw)。证明：（1）和（2）的证明类似1.34的（1）和（2）的证明。（3）“Þ”：

62、设AaBbÎw。据Lindenbaum-引理和（2），只须证w<aA>È w<bB>一致。假设要证结果不成立，则存在<aA>j1, , <aA>jnÎw<aA>和<bB>y1, , <bB>ymÎw<bB>使得 Ø(<aA>j1ÙÙ<aA>jnÙ<bB>y1ÙÙ<bB>ym)。据2.4（4），有 Ø(<aA>(j1Ù

63、17;jn)Ù<bB>(y1ÙÙym)。再据2.4（5），有 j1ÙÙjnÙy1ÙÙym®Ø(AaBb)。易见j1, , jn, y1, , ymÎw，因此据，有Ø(AaBb)Îw，矛盾于设定。“Ü”：设AaBbÏw。只须证：$uÎW(uRaAw且uRbBw)，即要证："uÎW(uRaAw或uRbBw)。任给uÎW使得uRaAw，要证uRbBw，为此只须证：存在公式j使得jÎubB但&

64、#216;jÎw。因为AaBbÏw，因此Ø(AaBb)Îw，故<aA>Ø(AaBb)Îw<aA>。因为uRaAw，故据（2），有w<aA>Íu，因此<aA>Ø(AaBb)Îu，再据公理DIS，易得bB(AaBb)Îu，所以AaBbÎubB，再据，易得。2.13典范模型基本定理令<W, R, >是GDA的典范模型。jÎw Û wÎj，对每一wÎW和公式j。证明：施归纳于j的结构。只考虑下面情况，其余情况易证。情况1jaAy：易见 aAyÎw Û "uÎW(wRaAu Þ yÎu) 据上一引理（1）Û "uÎW(wRaAu Þ uÎ|y|) 据1.30Û "uÎW(wRaAu Þ uÎy) 据归纳假设Û wÎaAy。 据真值集定义情况2jAaBb：我们