动态认知条件句逻辑DEC1

1、动态认知条件句逻辑DEC1李小五(中山大学逻辑与认知研究所，广东 广州 510275)摘要：首先，我们构造动态认知条件句系统DEC1，给出它的一些证明论结果。其次，我们引入有序邻域语义，给出描述DEC1的特征公理和规则的框架条件，证明DEC1相对这些框架条件是框架可靠的。最后，我们证明DEC1相对这些框架条件也是框架完全的。关键词：动态认知条件句系统；有序邻域语义；框架可靠性；框架完全性中国分类号: B81 文献标识码: A主体的一个动态认知全过程至少有4个要素：认知目的、背景知识、认知活动和认知结果。主体根据它的认知目的和背景知识，通过认知活动，最后达到认知结果。本文我们用一种4元条件句AB

2、aC来描述这个过程。在这样的条件句，A表示主体的认知目的，B表示它的背景知识，a表示它的认知活动，C表示由此产生的认知结果。因此ABaC的直观意义是“主体根据它的认知目的A和背景知识B通过认知活动a能得到认知结果C（能认知C）”。所以ABaC应该是模态公式。我们知道，一般情况下，背景知识是一个（可以是无穷的）公式集。但这里为了简单，我们把背景知识看作是有穷集b，从而用B来表示b，即B是b中所有公式的一个合取。我们可以把b很自然地推广到无穷，从而b中所有公式的一个合取bB是无穷逻辑语言中的一个公式。因此我们下面建立的逻辑也可以很自然地推广到相应的无穷逻辑。为了简单，本文我们只研究单主体逻辑，将来

3、我们另外撰文将此推广到多主体逻辑。1 形式系统及其证明论本文提到但未定义的概念和记号，请参见李小五的1。定义1.1形成规则（1）我们总用a和b（加或不加下标）表示认知活动，其形成规则如下：p½a;b½aÅb½aÄb。（2）所有活动的集合记为Action。（3）这里我们规定：aÅaa，aÄaa。（4）我们总用A, B, C和D（加或不加下标）表示公式，其形成规则如下：p½ØA½AÙB½ABaC。（5）所有公式的集合记为Form。Form也称为认知过程语言。（6）ABaC称为有三

4、个前件的条件句，其中A, B和a分别称为ABaC的第一前件，第二前件和第三前件。说明：（2）中的p表示原子认知活动。a;b表示认知活动a和b的复合(composition)：先进行a再进行b。aÅb表示认知活动a和b的选择(choice)：任选a或b 中一个活动进行。aÄb表示认知活动a和b的并行(parallelism)：同时进行活动a和b。（1）联结符Ú，®和«定义如通常。（2）省略括号的法则如通常。为了方便，我们规定联结符的结合力从左到右依次减弱：Ø，Ù，Ú，®，«。（3）若有必要，我们也

5、用圆点“·”隔开ABaC的三个前件。例如，(ABa1C1)Ù(ABa2C2)®AB· a1Äa2C1ÙC2，(A1BaC)Ù(A2BaC)®A1ÚA2·BaC，且(AB· a1;a2C)Ù(ABa1D)®A·BÙD· a2C分别表示(ABa1C1)Ù(ABa2C2)®AB(a1Äa2)C1ÙC2，(A1BaC)Ù(A2BaC)®(A1ÚA2)BaC， 且(AB(a1;

6、a2)C)Ù(ABa1D)®A(BÙD)a2C。（4）和T分别表示某个固定的常假式和常真式。（5）我们常用符号Û表示“当且仅当”，用Þ表示“若，则”。动态认知条件句系统DEC1定义如下：公理（模式）： （TA） 所有重言式的代入特例，（CC） (ABa1C1)Ù(ABa2C2)®AB· a1Äa2C1ÙC2，（AD） (A1BaC)Ù(A2BaC)®A1ÚA2·BaC，（ACH） AB· a1Åa2C«(ABa1C)Ú

7、; (ABa2C)，（AW） AB· a1Åa2C®AB· a1Äa2C，（CTR） (ABa1C)Ù(ACa2D)®AB· a1;a2D，（CMP） (ABaC)ÙAÙB®C。推理规则：（MP） A, A®CC，（RAE） A0«AA0BaC«ABaC，（RBM） B®B0AB0aC®ABaC，（RCM） C0®CABaC0®ABaC。说明：（1）由TA和MP构成的系统称为经典句子系统，记为PC。我们也用PC0表示

8、用不含的语言表述的PC。（2）CC称为结果合取公理。CC的直观意义是：若某个主体根据它的认知目的A和背景知识B分别通过认知活动a1和a2能认知C1和C2，则它根据A和B通过并行认知活动a1Äa2能认知C1ÙC2。这个公理的合理性建立在认知活动a1和a2在并行时不会互相干扰的前提下。（3）AD称为目的析取公理。（4）ACH称为活动选择公理。（5）AW称为弱化公理。（6）CTR称为传递公理，又称为活动复合公理。CRT的直观意义是：若主体根据它的认知目的A和背景知识B通过第一个认知活动a1能认知中间结果C，又把C作为它的背景知识通过第二个认知活动a2能认知D，则该主体根据A和原来

9、的背景知识B通过复合认知活动a1;a2能认知D。这个公理刻画了一种认知活动连续的过程。（7）CMP称为认知结果分离律。CMP的直观意义是：若主体根据它的认知目的A和背景知识B通过认知活动a能认知结果C，并且A和B又成立，则该主体认知的C也成立。这个公理说明，当主体的目的为真时认知结果也为真。（8）RAE称为目的等价置换规则。（9）RBM称为背景知识蕴涵规则。它表示主体能用蕴涵其背景知识的结果作为新的背景知识，所以RBM是反单调性的。据RBM易得ABaC®A·BÙD· aC，而此公式刻画了一种背景知识增长过程。（10）RCM称为结果蕴涵规则。它表示主体总能

10、认知其认知结果的逻辑后承，所以RCM是单调的。（11）上述除TA以外的公理都称为DEC1的特征公理，除MP和RAE以外的规则都称为DEC1的特征规则。定义1.4（1）我们用 A表示A是DEC1的内定理，即A在DEC1中有一个形式证明。（2）DEC1的全体内定理的集合记为Th(DEC1)。（3）我们也用 A表示AÏTh(DEC1)。引理1.5下面是DEC1的内定理：（1）(ABa1C)Ù(ABa2C)®AB· a1Äa2C，（2）(ABaC1)Ù(ABaC2)®ABaC1ÙC2，（3）(ABa1C)Ú (A

11、Ba2C)®AB· a1Äa2C。证明：我们只给出证明的主要步骤和主要根据。请读者自行补充细节。（1）据CC和RCM。（2）据CC和定义1.1（3）。（3）据ACH和AW。下面我们研究DEC1与PC0的关系。我们要证明前者是后者的协调概括，或者说前者可以协调地退化为后者。定义1.6 （1）定义从语言Form到不含的子语言Form0ÍForm的翻译映射t如下：t(p)p，对所有句符p；t(ØA)Øt(A)；t(AÙB)t(A)Ùt(B)；t(ABaC)t(C)。（2）对每一公式AÎForm，我们称t(A)是

12、A的t-翻译。说明：据上面的定义，易证t(AÚB)t(A)Ú t(B)，t(A®B)t(A)®t(B)，t(A«B)t(A)«t(B)。定义1.7令S和T是任意两个公理化系统。我们称S能t-退化为T，当且仅当S的所有内定理都能t-翻译为T的内定理。定理1.8DEC1能t-退化为PC0。证明：据上一定义，证明显然。定义1.9称公理化系统S是协调系统，当且仅当不存在A使得A和ØA都是S的内定理。定理1.10DEC1是协调的。证明：假设DEC1不协调，则存在A使得A和ØA都是DEC1的内定理。据上面的定理，t(A)和&#

13、216;t(A)都是PC0的内定理，矛盾于PC0的协调性。2 有序邻域语义和可靠性定理任给集合X，我们用P(X)表示X的幂集。（1）称二元组FáW, N ñ是有序邻域框架，简称F是ON-框架，当且仅当W是非空的可能世界集，邻域映射N是从Action×W到P(P(W)×P(W)×P(W)中的映射。（2）称三元组MáW, N, ñ是有序邻域模型，简称M是ON-模型，当且仅当áW, N ñ是ON-框架且 是从全体句符到P(W)的指派映射。（3） 也称为框架áW, N ñ上的指派映射。定义2.

14、2真值集定义令MáW, N, ñ是ON-模型。对每一复合公式A，定义A相对M的真值集A如下：对任意wÎW, aÎAction和公式A, B和C，（1）wÎØA Û wÏA，（2）wÎAÙB Û wÎA且wÎB，（3）wÎABaC Û <A, B, C>ÎN(a, w)。说明：基于框架定义的模型和定义复合公式的真值集，两者合在一起称为语义，因为由此我们可以在任何一个模型的任意可能世界中给任何一个公式赋予一个意义（真值）。上面给

15、出的语义称为有序邻域语义。（1）称ON-框架FáW, Nñ是动态认知条件句框架，简称F是dec1-框架，当且仅当下列框架条件成立：对任意wÎW和a, a1, a2ÎAction和X, Y, Z, U, Z1, Z2, X1, X2, Y0, Z0ÍW，(cc) <X, Y, Z1>ÎN(a1, w)且<X, Y, Z2>ÎN(a2, w) Þ <X, Y, Z1ÇZ2>ÎN(a1Äa2, w)，(ad) <X1, Y, Z>ÎN

16、(a, w)且<X2, Y, Z>ÎN(a, w) Þ <X1ÈX2, Y, Z>ÎN(a, w)，(ach) N(a1Åa2, w)N(a1, w)ÈN(a2, w)，(aw) N(a1Åa2, w)ÍN(a1Äa2, w)，(ctr) <X, Y, Z>ÎN(a1, w)且<X, Z, U>ÎN(a2, w) Þ <X, Y, U>ÎN(a1;a2, w)。(cmp) <X, Y, Z>&#

17、206;N(a, w)且wÎXÇY Þ wÎZ，(rbm) YÍY0且<X, Y0, Z>ÎN(a, w) Þ <X, Y, Z>ÎN(a, w)，(rcm) Z0ÍZ且<X, Y, Z0>ÎN(a, w) Þ <X, Y, Z>ÎN(a, w)。（2）所有的dec1-框架的类记作Frame(dec1)。定义2.4有效性定义令FáW, Nñ是ON-框架，MáW, N, ñ是ON-模型。（1

18、）称A在M中有效，记为M A，当且仅当AW；否则称A在M中不有效，记为M A 。（2）称A在F中有效，记为F A，当且仅当，对F上的任意指派映射 ，有AW；否则称A在F中不有效，记为F A 。（3）称规则A1, AnC相对M保持有效性，当且仅当，若A1AnW，则CW 。引理2.5令MáW, N, ñ是ON-模型。则（1）ØAWA，AÙBAÇB，AÚBAÈB，Æ， T W。（2）AÇA®BÍB。（3）A®BW Û AÍB。（4）A«BW Û

19、; AB。定义（1）称系统S相对框架类C是框架可靠系统，当且仅当，S的内定理在C的所有框架中有效。（2）称系统S相对框架类C是框架完全系统，当且仅当，在C的所有框架中有效的公式是S的内定理。定理框架可靠性定理DEC1相对框架类Frame(dec1)是可靠的。证明：任给dec1-框架F<W, N>和F上赋值 。下面验证DEC1的公理相对M<F, >有效且DEC1的推理规则相对M保持有效性。验证公理TA和规则MP：显然。验证公理CC：任给wÎ(ABa1C1)Ù(ABa2C2)。则<A, B, C1>ÎN(a1, w)，<A,

20、B, C2>ÎN(a2, w)。据定义的(cc)，我们有<A, B, C1ÇC2>ÎN(a1Äa2, w)。据引理，我们有<A, B, C1ÙC2>ÎN(a1Äa2, w)。所以我们有wÎAB· a1Äa2C1ÙC2。所以据2.5（3），我们有wÎ(ABa1C1)Ù(ABa2C2)®AB· a1Äa2C1ÙC2。验证公理AD：任给wÎ(A1BaC)Ù(A2BaC)。则<A

21、1, B, C>ÎN(a, w)，<A2, B, C>ÎN(a, w)。据定义的(ad)，我们有<A1ÈA2, B, C>ÎN(a, w)。据引理，我们有<A1ÚA2, B, C>ÎN(a, w)。所以我们有wÎA1ÚA2·BaC。验证公理ACH：任给wÎW，我们有wÎAB· a1Åa2CÛ <A, B, C>ÎN(a1Åa2, w)。Û <A, B, C>&#

22、206;N(a1, w)ÈN(a2, w) 据定义的(ach)Û wÎ(ABa1C)Ú(ABa2C)。验证公理AW：任给wÎAB· a1Åa2C。则<A, B, C>ÎN(a1Åa2, w)。据定义的(aw)，我们有<A, B, C>ÎN(a1Äa2, w)。所以我们有wÎAB· a1Äa2C。验证公理CTR：任给wÎ(ABa1C)Ù(ACa2D)。则<A, B, C>ÎN(a1, w)，&

23、lt;A, C, D>ÎN(a2, w)。据定义的(ctr)，我们有<A, B, D>ÎN(a1;a2, w)。据2.2（3），我们有wÎAB· a1;a2D。验证公理CMP：任给wÎ(ABaC)ÙAÙB。则<A, B, C>ÎN(a, w)，wÎAÙBAÇB。据定义的(cmp)，我们有wÎC。验证规则RAE：设A0«AW。据2.5，有（）A0A。任给wÎW，我们有wÎA0BaC Û <A0, B,

24、C>ÎN(a, w) Û <A, B, C>ÎN(a, w) 据（）Û wÎABaC 据真值集定义2.2。因此据w的任意性，有A0BaCABaC，据2.5，我们有A0BaC«ABaCW。验证规则RBM：设B®B0W。据2.5，有（）BÍB0。任给wÎW，我们有wÎAB0aC Û <A, B0, C>ÎN(a, w) Þ <A, B, C>ÎN(a, w) 据（）和的(rbm)Û wÎABaC 据

25、真值集定义2.2。因此据w的任意性，有AB0aCÍABaC，据2.5，我们有AB0aC®ABaCW。验证规则RCM：设C0®CW。据2.5，有（）C0ÍC。任给wÎW，我们有wÎABaC0 Û <A, B, C0>ÎN(a, w) Þ <A, B, C>ÎN(a, w) 据（）和的(rcm)Û wÎABaC 据真值集定义2.2。因此据w的任意性，有ABaC0ÍABaC，据2.5，我们有ABaC0®ABaCW。3 完全性定理令w是公式

26、集。（1）称w是一致集，当且仅当对所有有穷序列A1, AnÎw，有 Ø(A1ÙÙAn)。（2）称w是极大集，当且仅当对所有AÎForm，AÎw或ØAÎw。（3）称w是极大一致集，当且仅当w既是一致的又是极大的。（4）称DEC1是一致系统，当且仅当Th(DEC1)是一致的。DEC1是一致的。证明：假设DEC1不一致。则Th(DEC1)不一致，所以存在A1, AnÎTh(DEC1)使得 Ø(A1ÙÙAn)。另一方面，因为A1, AnÎTh(DEC1)，所以易证 A1&#

27、217;ÙAn。据定义1.9，DEC1不协调，矛盾于定理1.10。因为DEC1是PC的扩充，所以如通常证明，我们有下列结果。令w是极大一致集。（1）ØAÎw Û AÏw，AÙBÎw Û AÎw且BÎw，AÚBÎw Û AÎw或BÎw，AÎw且 A®B Þ BÎw，AÎw且A®BÎw Þ BÎw。（2）Th(DEC1)Íw。（3）若 A，则存在极大一

28、致集u使得AÏu。定义 |A|w：w是极大一致集使得AÎw。引理3.5（1）|ØA|W|A|，其中W是所有极大一致集的集合，|AÙB|A|Ç|B|，|AÚB|A|È|B|，| |Æ，| T |W。（2）|A|Ç|A®B|Í|B|。（3）|A®B|W Û |A|Í|B| Û A®B。（4）|A«B|W Û |A|B| Û A«B。证明：据上一引理易证。定义3.6（1）定义DEC1的典范框架N<

29、W, N>如下：Ww：w是极大一致集，N是从Action×W到P(P(W)×P(W)×P(W)中的映射使得<|A|, |B|, |C|>ÎN(a, w) Û ABaCÎw，对任意wÎW, aÎAction和公式A, B和C。（2）定义DEC1的典范模型M<W, N, >如下：<W, N>是DEC1的典范框架，且p|p| ，对每一句符p。说明：据引理3.2，DEC1是一致的，所以W非空。定理3.7典范模型基本定理令M<W, N, >是如上定义的DEC1的典范模型。

30、（1）DÎw Û wÎD，对每一wÎW和公式D。（2）| D|D，对每一公式D。证明：（2）从（1）易得。所以我们只须证（1）。施归纳于D的结构。句符的情况据上一定义的。布尔联结符Ø和Ù的情况如通常所证。令DABaC。所以wÎD Û wÎABaC Û <A, B, C>ÎN(a, w) 据2.2的（3）Û <|A|, |B|, |C|>ÎN(a, w) 据归纳假设Û ABaCÎw 据上一定义的Û DÎw

31、。定理3.8 令M是DEC1的典范模型。则对每一公式A，我们有M A Û A。证明： A Û |A|W 据（2）（3）Û AW 据上一定理Û M A 。（1）定义DEC1的适当结构(proper structure) M<W, N, >如下。（a）Ww：w是极大一致集；（b）对所有aÎAction和wÎW，N(a, w)<|A|, Y, Z>：存在ABaCÎw使得YÍ|B|且|C|ÍZ。（c）p|p|，对每一句符p。（2）F<W, N>称为DEC1的适当框架。引理3.1

32、0 令M<W, N, >是DEC1的适当结构。则M是DEC1的典范模型。证明：据定义3.6，只须证：对任意aÎAction, wÎW和公式A, B和C，（1）<|A|, |B|, |C|>ÎN(a, w) Û ABaCÎw。“Ü”：设ABaCÎw。因为|B|Í|B|且|C|Í|C|，所以据N(a, w)的构造，有<|A|, |B|, |C|>ÎN(a, w)。“Þ”：设<|A|, |B|, |C|>ÎN(a, w)。因为等价类的

33、代表元不是惟一的，所以据N(a, w)的构造，（2）存在A0B0C0Îw使得|A0|A|, |B|Í|B0|且|C0|Í|C|。因为|A0|A|, |B|Í|B0|且|C0|Í|C|，所以据引理3.5，有 A0«A， B®B0， C0®C。 据 A0«A和RAE，有 A0B0aC0«AB0aC0。再据 B®B0和RBM，有 A0B0aC0®ABaC0。再据 C0®C 和RCM，有 A0B0aC0®ABaC。因为A0B0aC0Îw，所以ABaC&#

34、206;w。引理3.11DEC1的适当框架F是dec1-框架。证明： 下面我们来验证F满足定义2.3给出的框架条件。验证(cc)。设<X, Y, Z1>ÎN(a1, w)且<X, Y, Z2>ÎN(a2, w)。则（1）存在A1B1a1C1Îw使得|A1|X, YÍ|B1|且|C1|ÍZ1，且（2）存在A2B2a2C2Îw使得|A2|X, YÍ|B2|且|C2|ÍZ2。因为|A1|A2|，所以据（1）的A1B1a1C1Îw和RAE，有（3）A2B1a1C1Îw。因为 B1

35、ÙB2®B1， B1ÙB2®B2，所以据（3），（2）的A2B2a2C2Îw和RBM，有（4）A2· B1ÙB2· a1C1Îw，A2· B1ÙB2· a2C2Îw。再据公理CC，易得（5）存在A2· B1ÙB2· a1Äa2C1ÙC2Îw使得|A2|X, YÍ|B1ÙB2|且|C1ÙC2|ÍZ1ÇZ2。所以<X, Y, Z1ÇZ2>&

36、#206;N(a, w)。验证(ad)。设<X1, Y, Z>ÎN(a, w)且<X2, Y, Z>ÎN(a, w)。则（1）存在A1B1aC1Îw使得|A1|X1, YÍ|B1|且|C1|ÍZ，且（2）存在A2B2aC2Îw使得|A2|X2, YÍ|B2|且|C2|ÍZ。因为|A1|A2|，所以据（1）的A1B1aC1Îw和RAE，有（3）A2B1aC1Îw。因为 B1ÙB2®B1， B1ÙB2®B2，所以据（3），（2）的A2B

37、2aC2Îw和RBM，有（4）A2· B1ÙB2· aC1Îw，A2· B1ÙB2· aC2Îw。因为 C1®C1ÚC2， C2®C1ÚC2，所以再据（4）和RCM，有A2· B1ÙB2· aC1ÚC2Îw，A2· B1ÙB2· aC1ÚC2Îw。再据公理AD，易得（5）存在A1ÚA2· B1ÙB2· aC1ÚC2&#

38、206;w使得|A1ÚA2|X1ÈX2, YÍ|B1ÙB2|且|C1ÚC2|ÍZ。所以<X1ÈX2, Y, Z>ÎN(a, w)。验证(ach)。任给X, Y, ZÍW，易见下面命题等价：（1）<X, Y, Z>ÎN(a1Åa2, w)。（2）存在AB· a1Åa2CÎw使得|A|X, YÍ|B|且|C|ÍZ。（3）存在(ABa1C)Ú (ABa2C)Îw使得|A|X, YÍ|B|且

39、|C|ÍZ。（据公理ACH）（4）存在ABa1CÎw使得|A|X, YÍ|B|且|C|ÍZ，或存在ABa2CÎw使得|A|X, YÍ|B|且|C|ÍZ。（5）<X, Y, Z>ÎN(a1, w)，或<X, Y, Z>ÎN(a2, w)。（6）<X, Y, Z>ÎN(a1, w)ÈN(a2, w)。因此我们有N(a1Åa2, w)N(a1, w)ÈN(a2, w)。验证(aw)。设<X, Y, Z>ÎN(a1&

40、#197;a2, w)。则（1）存在AB· a1Åa2CÎw使得|A|X, YÍ|B|且|C|ÍZ。再据公理AW，易得（2）存在AB· a1Äa2CÎw使得|A|X, YÍ|B|且|C|ÍZ。所以<X, Y, Z>ÎN(a1Äa2, w)。验证(ctr)。设<X, Y, Z>ÎN(a1, w)且<X, Z, U>ÎN(a2, w)。则（1）存在A1B1a1C1Îw使得|A1|X, YÍ|B1|且|C1

41、|ÍZ，且（2）存在A2B2a2C2Îw使得|A2|X, ZÍ|B2|且|C2|ÍU。因为|A1|A2|，所以据（1）的A1B1a1C1Îw和RAE，有（3）A2B1a1C1Îw。因为|C1|Í|B2|，所以 C1®B2，再据（3）和RCM，有（4）A2B1a1B2Îw。再据（2）的A2B2a2C2Îw和公理CTR，易得（5）存在A2B1· a1;a2C2Îw使得|A2|X, YÍ|B1|且|C2|ÍU。所以<X, Y, U>ÎN(a

42、1;a2, w)。验证(cmp)。设<X, Y, Z>ÎN(a, w)且wÎXÇY。则（1）存在ABaCÎw使得|A|X, YÍ|B|且|C|ÍZ。据ABaCÎw和CMP，易得AÙB®CÎw，所以据3.3，有（2）AÙBÎw Þ CÎw。因此（3）wÎ|AÙB| Þ wÎ|C|。因为|A|X, YÍ|B|，所以XÇY Í|A|Ç|B|AÙB|。据设定，有wÎXÇY，所以wÎ|AÙB|。据（3），有wÎ|C|。因为|C|ÍZ，所以wÎZ。验证(rbm)。设YÍY0且<X, Y0, Z>ÎN(a, w)。则（1）存在ABaCÎw使得|A|X, Y0&