（基础数学专业论文）任务逻辑.pdf

任务逻辑 许文艳 矿6 1 0 0 9 3 摘要自线性逻辑的概念诞生以来，关于线性逻辑及其子结构逻辑的研究已经 引起了广泛关注线性逻辑最初形成时源于把公式看成“资澡，因而从语义上讲又 被称为“资源逻辑然而这种“资源语义一直以来都没有形成严格的形式化体系 1 9 9 8 年g j a p a r i d z e 借鉴g a m e 语义的方法首次提出“任务逻辑”的概念，把 公式( 即资源) 理解为“任务”，给出了线性逻辑的某扩张及其语义理论，但该理论尚 不完善，并未找到相应的语构体系2 0 0 2 年，g j a p a r i d z e 又在一阶谓词逻辑框 架下引入算子n 和n ，建立了严格的任务逻辑语义理论，并得到了完备的形式系统 口，使线性逻辑最初的“资澡语义完全形式化，同时指出该逻辑作为p l a n n i n g 逻 辑应用于人工智能领域时避免了f r a m e 问题和k n o w l e d g ep r e c o n d i t i o n s 问题 然而g j a p a x i d z e 在谓词逻辑框架下的任务逻辑( 简称为谓词任务逻辑) 是不 可判定的，且形式系统中的定理也未得到详细的讨论，这使它的应用受到了很 大的限制本文的目的就是对任务逻辑进行系统的研究，在命题逻辑框架下引入附 加算子n ，建立命题任务逻辑的语义理论，并相应从语构上定义形式系统l ，证f 兜其 可靠性，完备性及可判定性定理，详细考察形式系统l 中的基本定理，为以后研究 更广泛意义的任务逻辑奠定基础与此同时，本文还给出了谓词任务逻辑的语义和 语构理论，得到了界于形式系统l 和p 之间的系统，并证明了系统的可判 定性 本文的主要内容如下： 第一部分：在经典命题逻辑语言中引入附加算子n ，把公式理解为f 壬务，给 出了“任务逻辑的语义理论 第二部分：以经典命题逻辑的所有定理为公理，以a 规则和r _ 规则( 具体定 义见正文) 为两条基本推理规则，建立了形式系统厶并证明了系统l 的可靠性， 完备性及可判定性定理 第三部分：对形式系统l 中的定理进行考察，提出“模仿策略的概念，得到 了系统三中一系列基本定理和一些有趣的结果，为后面研究谓词任务逻辑的基本 定理提供了依据 第四部分：介绍了谓词任务逻辑的语义和语构理论，针对形式系统口，在l 中去掉量词v ，得到新的形式系统，并论证了l 7 的可判定性，从而使任务逻辑的 应用得以推广 关键词：任务逻辑附加算子最终状态可完成的可判定性 2 t h e l o g i co f t a s k s x u w e n y a n a b s t r a c ts i n c et h eb i r t ho fl i n e a rl o g i c ，t h et o p i co fi ta n d s u b s t r u c t u r a ll o g i c s h a sd r a w nt h ea t t e n t i o no fm a n yr e s e a r c h e r s t h ep h i l o s o p h yb e h i n dl i n e a rl o g i ci s t h a tf o r m u l a sa r ev i e w e da sr e s o u r c e s ，t h e r e f o r e ，f r o mt h es e m a n t i cp o i n to fv i e w ， l i n e a rl o g i ci so f t e nc a l l e d “r e s o u r c el o g i c ”b u tt h i sk i n do fr e s o u r c ep h i l o s o p h yh a s n e v e rb e e nf u l l yf o r m a l i z e d m a k i n g u s eo ft h et e c h n i q u eo fg a m es e m a n t i c s ，g j a p a r i d z ef i r s ti n t r o d u c e d “t h el o g i co ft a s k s ”i n1 9 9 8 ，w h e r ef o r m u l a sa r eu n d e r s t o o da st a s k s h eg i y e st h e r e s o u r c es e m a n t i c sf o ral a n g u a g ew h i c he x t e n d st h el a n g u a g eo fl i n e a rl o g i c ，t h o u g h i t st h e o r yi sn o tp e r f e c t i n2 0 0 2 ，g j a p a x i d z ei n t r o d u c e das e m a n t i c sf o rt h el a n g u a g eo f c l a s s i c a lf i r s to r d e rl o g i cs u p p l e m e n t e dw i t ht h ea d d i t i o n a lo p e r a t o r sna n d 兀，a x i o m a t i c a l l yd e f i n e dal o g i cl + i nt h ea b o v el a n g u a g ea n dp r o v e di t ss o u n d i l c 二s a n dc o m p l e t e n e s s ，w h i c hc a nc l a i mt ob eaf o r m a l i z a t i o no ft h er e s o u r c ep h i l o s o p h y a s s o c i a t e dw i t hl i n e a rl o g i c h eb e l i e v e st h ef o r m a l i s mm a yh a v eap o t e n t i a l i t yt o b eu s e di na ia sa na l t e r n a t i v el o g i co fp l a n n i n g b e c a u s e i ti si m m u n et ot h ef r a m e p r o b l e ma n dt h ek n o w l e d g ep r e c o n d i t i o n sp r o b l e m h o w e v e r ，t h el o g i co ft a s k sb a s e do i lc l a s s i c a lf i r s to r d e rl o g i ci n t r o d u c e db y g j a p a r i d z ei s u n d e c i d a b l ea n dt h et h e o r e m si nt h el o g i c 三+ a r en o tg i v e n w h i c h m a k e si t sa p p l i c a t i o nr e s t r i t e d t h ea i mo ft h i sp a p e ri st od e v e l o pt h et h e o r yo ft h e l o g i co ft a s k s i ti n t r o d u c e sa s e m a n t i c sf o rt h el a n g u a g eo fc l a s s i c a lp r o p o s i t i o n a l l o g i cs u p p l e m e n t e dw i t ht h ea d d i t i o n a lo p e r a t o rn ，a x i o m a t i c a l l yd e f i n e sal o g i cl ， p r o v e si t ss o u n d n e s s ，c o m p l e t e n e s sa n dd e c i d a b i l i t y ，a n de x t e n s i v e l yw o r k so u ti t s t h e o r e m s a tt h es a m et i m e ，t h el o g i co ft a s k sb a s e do nt h ec l a s s i c a lf i r s to r d e r l o g i ci si n t r o d u c e da n dan e wl o g i cl ，w h i c hi sb e t w e e nt h el o g i cla n dl + a n di s d e c i d a b l e ，i se s t a b l i s h e d i nt h ef i r s tp a r t ，as e m a n t i c sf o rt h el a n g n l a g eo fc l a s s i c a lp r o p o s i t i o n a ll o g i c s u p p l e m e n t e dw i t ht h ea d d i t i o n a lo p e r a t o rni si n t r o d u c e d ，w h e r ef o r m u l a sa r e u n d e r s t o o da st a s k s i nt h es e c o n dp a r t ，al o g i cli se s t a b l i s e d ，w h o s ea x i o m sa x ea l lt h et h e o r e m s i nc l a s s i c a lp r o p o s i t i o n a ll o g i ca n dr u l e so fi n f e r e n c ea r er u l ea a n dr u l er t h e s o u n d n e s s ，c o m p l e t e n e s sa n dd e c i d a b i l i t yo f i ta r ep r o v e n 3 i nt h et h i r dp a r t as o r to ft h e o r e m si nla n dt h ed e f i n i t i o no fm i m i c k i n g s t r a t e g ya r e 舀y e n l a s t l y , t h ep a p e ri n t r o d u c e st h es e m a n t i c sf o rt h el a n g u a g eb a s e do nc l a s s i c a l f i r s to r d e rl o g i c ，p r o p o s e sa l o g i cl b yo m i t i n gc l a s s i c a lq u a n t i f i e rv ，a n dp r o v e si t s d e c i d a b i l i t y k e y w o r d s ：l o g i c o ft a s k s ；a d d i t i v eo p e r a t o r ；e v e n t u a ls i t u a t i o n ；a c c o m p l i s h a b l e ；d e c i d a b i l i t y 4 引言 自1 9 8 7 年j y g i r a r d 提出线性逻辑 1 1 的概念以来，对其各种子结构逻辑 ( s u b s t r u c t u r a ll o g i c s ) 的研究已经引起国内外著多学者的关注1 2 】这些子结构逻辑 的共同特点是对一个公式中子公式出现个数的敏感性其中最典型的例子是在经典 逻辑中成立的公式a 一aaa 和规则( 若a _ 口且a - a 则a b g ) 在这 些子结构逻辑中不成立 从语义上讲，子结构逻辑通常被称为“资源逻辑( r e s o u r c el o g i c ) 3 | ，其原因在 于如果我们把公式看作资源，算子a 看作对资源的相加，算子“一”看作把前件 资源转变为后件资源，那么公式a 4 一般强于公式a ，公式a 口 g 一般强 于公式( a - b ) a ( a - g ) 例如$ 1 $ 1 应被理解为等价于$ 2 而不是$ l 从而 $ 1 ( $ 1 $ 1 ) 不成立；若一杯牛奶和一块面包各值$ 1 ，则$ 1 _ ( 一杯牛奶) 和 $ 1 斗( 一块面包) 成立，但$ 1 _ ( 一杯牛奶) ( 一块面包) 不成立+ 这种把公式看作资源的方法似乎很自然、合理，但一直以来并未被完全形式 化，还没有形成严格的。完整的语义理论着眼于此，1 9 9 8 年g j a p a r i d z e 将这种 “资源语义进行发展，首次提出“任务逻辑，的概念【3 在那里，公式( 即资源) 被 看作是需要执行的任务文【3 】的主要贡献是建立了线性逻辑语言的一个扩张及其 相应的语义理论，论证了该逻辑体系作为p l a n n i n g 逻辑运用于人工智能领域的优 点是避免了f r a m e 问题 4 - 9 1 ，并且为处理k n o w l e d g ep r e c o n d i t i o n s 同题 1 0 - t 4 1 提供 了有效的方法文【3 】中所提出的语言具有很强的表达力，它包括了经典逻辑和线 性逻辑语言。然而正因为它的一般性，与其语义理论相应的语构体系很难建立 另一方面，早在二十世纪5 0 年代末l o r e n z e n 1 3 】就提出了“g a m es e m a n t i c s ” 的概念他认为：命题应该被看成是两个参赛者( p l a y e r ) 之间进行的一场竞赛( 或游 戏) ( g a m e ) ，其中参赛一方将维护( d e f e n d ) 该命题，另一方将反驳( a t t a c k ) 该命题； 命题的语义值应通过建立一定的竞赛规则而最终确定随后l o r e n z ，h i n t i k k a 1 6 等人也相继研究了g a m e 语义，并取得一定的成果 1 7 - 1 9 】 1 9 9 2 年，b l a s s 1 8 】首先发现g a m e 语义能与线性逻辑最初的“资源语义很好 地统一起来于是在此基础上，又有许多学者开始研究线性逻辑的g a m e 语义例 如文【17 ，【1 9 】和【3 等都对b l a s s 的观点进行了修改和完善但到目前为止人们仍 然没有找到线性逻辑的完备的g a m e 语义和语构体系 2 0 0 2 年，g j a p a r i d z e 2 0 】在经典的一阶谓词逻辑框架下引入附加算子n 和兀， 建立了严格的任务逻辑语义理论，并得到了完备的形式系统f 他认为文2 0 中 所介绍的任务逻辑主义是线性逻辑“资源语义的完全形式化，并且从技术角度看 是一种g a m e 语义，在a j 中有很高的应用价值但遗憾的是该逻辑体系是不可判 定的，且形式系统中的定理并未得到很好的研究这使其应用受到了很大的限 制本文的目的就是对任务逻辑进行系统的研究，分别在命题逻辑和一阶谓词逻辑 框架下建立任务逻辑语义和语构理论，分别定义形式系统l 和，特别是在命题 逻辑框架下证明形式系统l 的可靠性，完备性及可判定性定理，并对l 中的基本 定理进行详细考察，得到了许多有趣的结果，为后面研究任务逻辑的语构理论奠定 基础 本文共分四章第一章为命题逻辑框架下的任务逻辑语义理论，在经典命题逻 辑语言中引入附加算子n ，把公式理解为“任务”，给出了任务逻辑语义的形式化定 义第二章为命题逻辑框架下任务逻辑的语构理论，定义了形式系统l ，证明了该 系统的可靠性，完备性及可判定性定理第三章为形式系统l 中的定理，详细考察 了工中一系列基本定理第四章为谓词逻辑框架下的任务逻辑语义和语构理论，得 到介于命题和谓词任务逻辑形式系统之间的系统l ，并证明了其可判定性 2 第一章命题逻辑框架下任务逻辑的语义理论 1 什么是任务逻辑 在经典的命题逻辑 2 l 】中，命题就是陈述句，如“今天是星期- - , ，“1 6 是偶数， 且1 6 是素数等；它们都可看作是“事实，因而我们称其为“事实逻辑然而在现 实生活中除了这样的事实之外，还有许多这样的命令句( 祈使句) ，如 ( i ) 打扫房间”， ( i i ) “打开电视或打开收音栅， ( i i i ) “整理草坪”， ( i v ) “不要去锄草”， 他们都可看作是“任务”从语义上讲，“事实有4 p 值或“假值，而对于“任 务则应当称其是“被完成的”或“未被完成的” 以任务为基本对象进行研究的逻辑q 任务逻辑如果任务逻辑与经典逻辑的 区别仅在于把“事实”看成“任务”，那么我们介绍任务逻辑也就没多大意义了笔 者认为仅就命题水平而言任务逻辑区别于经典逻辑的显著特点如下： i 引入附加算子n 当我们提到任务时，头脑中会出现两个主体：任务的提 出者和任务的执行者我们形象地称前者为“主人，后者为“仆人当我们把为人 服务的机器、机器人看作“仆人，把操作者、操作环境看作“主人】时，该逻辑就有 了广阔的应用前景本文所提出的逻辑在经典命题逻辑的所有算子中新增加了算子 “门”，从而得到了一个新的逻辑系统 任务a n b 表示“主人i 可以选择提出的两个潜在要求：a 或丑该任务一般 比任务a ab 易完成因为a ab 要求仆人最终完成a 和b 两个任务，而a 几日 只要求仆人完成a 和b 中的一个任务例如，设a 为钉扫教室，曰为“整理草 坪i ，如果我们让一个机器人执行任务，且该机器人有足够的时间和能量完成a 和 b 中的一个，但没有足够的能量完成a 和日两个任务，那么对这个机器人来说，它 能完成任务a n b ，但不能完成任务a a b 进一步，该机器人能完成任务a n 、a ， 但没有哪个机器人髓完成任务a 一a 在引入算子n 后，形如a _ b 的公式也有了新的意义例如有一机器人， 它没有足够的能量无条件执行任务“打扫教室”n “整理草坪”，但如果给它提供一台 吸尘器或一台锄草机。它就能完成上述任务的话，则它能完成任务“给我一台吸尘 器n “给我一台锄草机 “打扫教室”几“整理草坪”由此可以看出在蕴含前件中提 3 出要求的是仆人而不是主人，也就是说主人和仆人的地位在蕴含前件中相互交换 了， 2 引入c c 实现”的概念在具体执行某任务时，可能有不同的实现途径如任 务a 门b ，若主人要求a 且a 被完成，则认为a 几b 被完成；若主人要求5 且 b 被完成，则也认为a nb 被完成再如任务“给我一台吸尘器”几“给我一台锄草 机 ，_ c 打扫教室n “整理草坪 ( 简记为p 1 几仇_ ) 3n p 4 ) ，若p l _ p 3 被完成则认 为p li 1 p 2op 3f i p 4 被完成；若耽- 4 肌被完成则也认为p 1i - 1 ) 2 一p 3n 肌被完 成因此判断某任务是否被完成，就是看该任务的实现过程是否成功在2 我们 将看到不同的任务有不同的实现过程，而同一任务也可能有多种实现过程， 3 引入嘬终状态”的概念经典命题逻辑中每个“事实”的真假是确定的， 而任务逻辑中某任务最初的语义值可能是不确定的，而只有在某个给定的嘬终状 态”下才能确定例如任务“当一名科学家”，对张三来说该任务是否被完成只有结 合一定的最终状态( 如在张三6 0 岁生日时或在本世纪4 0 年代结束时) 才能确定这 样，在某个给定的最终状态下，一任务的语义值就是确定的了当然对同一任务， 在不同的状态下其值也可能不同如上例中。任务“当一名科学家”对张三来说在 状态s ( 在他6 0 岁生日时) 可能是未被完成的，而在状态s 2 ( 在本世纪4 0 年代结束 日寸) 又可能是被完成的 结合2 ，3 两点我们得到：看任务是否被完成就是看该任务的某实现关于某最终 状态是否成功这正是任务逻辑语义的核心 4 定义了形式系统l 相应于命题任务逻辑的语义，本文从语构上形式定义 了系统l 它以经典命题逻辑中的所有定理为公理，以a 一规则和r 一规则为两条 基本推理规则，是不同于经典命题逻辑中形式系统的新系统由于公理和推理 规则不同，所以形式系统l 中定理的形式也不完全等同于经典逻辑中的定理最有 代表性的例子就是公式a _ a a 它在经典逻辑中显然是定理，但在任务逻辑中 却不是定理( 具体原因见第三章) 2 预备知识 1 任务逻辑及其符号化 像1 中所列举的( i ) 、( i i i ) 等这样的任务称为简单任务；而把诸如( i i ) 、( i v ) 这样的任务称为复杂任务 在任务逻辑中，用p ，p 。，来表示简单任务，并称之为原子任务，然后引入 逻辑连接词、，v ，a ，_ 及n ( 其中，v ， ，_ 的意义同经典逻辑中的意义一致几 4 的意义在后文介绍) 这样由原子任务出发借助于上述连接词就可以表达各种复杂 任务了这里我们用上表示经典命题中的任一矛盾式，则、a 就可表示为a 。j _ 了 2 基本概念 定义1 2 1 设s = d l ，i 0 2 ，) ，作f ( s ) 如下： ( i ) p l ，仇，f ( s ) ； ( i i ) 上ef ( s ) ； ( i i i ) 若a ，b f ( s ) ，则a 日，a n b f ( s ) ； ( i v ) f ( s ) 中的元都可以通过( i ) ，( i i ) ，( i i i ) 而得到称s 中的元为原子任务( 原 子公式) ，f ( s ) 中的元为任务( 公式) - 称n 为附加算子 形如a 门b 的公式( 子公式) 叫附加公式( 子公式) 其中a ，b 称为n 的辖 域，称4 ，丑在几的辖域中出现 一个公式中所含附加算子n 的个数叫做该公式的附加度 附加度为o ( 即不含n ) 的公式叫原始公式 若某公式的子公式不在n 的辖域中出现，则称该子公式在公式中表匿出现 例1 2 1 ( 1 ) p l ，p 1 上，p ln p 2 ，p l - p 2n p 3 等都是公式 ( 2 ) 由于经典命题中a v b 是、a - b ，即( a _ 上) _ b 的简写，a ab 是 、( 4 _ 、b ) ，即_ ( b 上) ) - 上的简写，故p lv p 2 ，p 1a p 2 等也是任务 注意，除原子公式和上之外，f ( s ) 中的公式都可化为a 口或4 nb 的 形式，分别视最后一步的连接词是- 或n 而定 例1 2 2 设a = l n p 2 _ p 3 ) _ p 4 ，则子公式p 3 ，p 4 在a 中表面出现，p 1 ，p 2 在几的辖域中出现，特别注意子公式p np 2 作为整体在a 中也为表面出现 下面给出一种方法来表示子公式在公式中表现出现的位置：在公式a - b 中 ( a ，b f ( s ) ) ，a 在蕴含前件( a n t e c e d e n t ) 的位置，用a 表示；日在后件( c o n s e q u e n t ) 的位置，用c 表示这样我们就能用由a ，c 组成的链来表示表面出现的位置 了 ( 如在例1 2 2 中，p 3 的位置为a c ，p 4 的位置为c ，而p 。n p 2 的位置为a a ) 我 们称此a e 链为子公式的出现说明约定空链也为一种出现说明，记为e 对于给 定的某公式而言，并非所有的出现说明都是有效的( 如在例1 2 2 中，a c a ，a a c 等 就是无效的) 设1 1 是公式a 的有效的出现说明( 即某个。一c 链) ，我们用r ( a ) 来表示该 口一e 链所指位置的子公式 ( 如在例1 2 2 中，a c ( a ) = p a ，a a ( a ) = p lu p 2 ) 以下 就给出r ( a ) 的递归定义 2 】= 0 定义1 2 2 设尹为任意的一个a c 链 ( i ) 。节链对a 有效当且仅当a = b 。c 且寸链对b 有效 寸( b ) ； ( i i ) c - 尹链对a 有效当且仅当a = b c 且尹链对c 有效 尹( g ) ； 此时a - 尹( a ) = 此时c - i + ( a ) = ( i i i ) e 对4 总有效，且e ( a ) = a ， 由此定义可知若a = b n c ，则其唯一有效的出现说明为e 若出现说明r 中含有偶数个o ( 可能为0 个) ，则称r 为正的；否则称r 为负 的 - 设a ，b f ( s ) ，f 为a 的有效的出现说明，将a 中的子公式r ( a ) 换为b 而保持a 中其它符号均不变，此过程称为a 的一个变换，记为r b ，变换后的结 果记为a ( r b ) 例如在例1 2 2 中，a a p i ，a c p 4 均为a 的变换，且a ( a a p 1 ) = 扫l - 4 p s ) - 4 p 4 ，a ( a c p 4 ) = ( p ln p 2 - 4 p 4 ) _ p 4 定义1 2 3 设a f ( s ) ，r 为a 的有效的出现说明，r b 为a 的个变换 ( i ) 若f ( a ) = a - n a 。且b = a l 或b = a 2 ，而r 为负的，则称r b 为a 的 一个基本行动； ( i i ) 若r ( a ) = a i 几也且b = a l 或b = a 2 ，而r 为正的，则称r b 为a 的一个基本反应 例1 2 3 设任务a 为“给我钥匙 n “给我抹带o “打开门”n “擦桌子，记为 a = p lf p 2 - p 3 r i p 4 设r l 为a ，则r t ( a ) = p l7 1 p 2r l p 1 ，r l p 2 均为a 的基本行 动且a ( r 1 屈i ) = p i - - 4p 3 ( 3 1 9 4 ( i = 1 或2 ) ；设r 2 为c ，则r 2 ( a ) = p 3 i 3 p 4 ，f 2 p 3 ，r 2 p 4 均为a 的基本反应，且a ( r 2 功) = p i 门p 2 - - 4p j ( j = 3 或4 ) 由此例可看出基本行 动表示仆人的基本要求，基本反应表示主人的基本要求 定义1 2 4 设aef ( s ) ，x = ，其中e 1 是a o = a 的基本行 动，岛是a - = a o ( e t ) 的基本行动，则称x 为a 的行动，记a 的行动的全 体为4 ( a ) 若e t 一，五_ 均为基本反应。则称x 为a 的反应，记a 的反应的全体为 n x ( a ) 我们用a ( x ) = a ( ) 表示对a 进行变换e 1 ，磊后的结 果若x = ，则a ( x ) = a ；若x ，则称x 为a 的真行动( 真反应) 注意，基本行动( 基本反应) 是n = 1 时特殊的行动( 反应) 行动( 反应) 本是一 种变换，在不致于混淆的情况下，也把变换的结果叫做行动( 反应) 如若b = a 伍) ， 则也称且为a 的行动( 反应) 6 由定义1 2 4 容易得到下面的结论： 命题1 2 1 设x 是a 的行动，y 是a 的反应，则x 也是a ( y ) 的行动，y 也是a ( x ) 的反应，且似咩) ) ( y ) = ( a ( y ) ) 旺) ，记为a ( x ，y ) 进步，设b = a ( x ，) ，我们称b 为a 的个进展若该b a ，即x 或y ，则称b 为a 的真进展 定义1 2 5 设a o f ( s ) ，称r = 为a o 的个实现，其中对 任意i ( o i n ) ，a i + 是a 的一个真进展叫r 的最后一个公式特男地约 定冗= 也是a o 的一个实现，只不过这时x = y = ，记实现的全体为冗 注：( i ) 由定义1 2 5 可看出，对于原始公式a ，由于它无行动或反应，即 x = y = ，所以其唯一可能的实现为 ( i i ) 设a = b n c ，则其实现过程有三种： ( a ) ( 此时y = ，相当于主人没提任何要求) ( b ) ( 此时y = , b ，相当于主人提出要求b ) ( c ) ( 此时y = e c ，相当于主人提出要求g ) ( b ) ( c ) 中的“”表示进一步若b ，g 中仍含有附加公式，则可进一步对它们 采取行动或反应或同时采取行动和反应 由此我们就看出公式日ne 的实际意义：主人可能提出的两个潜在要求：或 者b ，或者d ( i i i ) 设a = p tn p 2 ( p 3 上) n p 4 贝0 r 1 = r 2 = r 3 = 等等都是4 的实现 定义1 2 6 设，：冗a 是一个部分函数，它对它已定义的每个实现赋予该 实现的最后一个公式一个行动，我们称，为一个行动策略 当，对某实现r 还未定义时，我们记f ( r ) = 定义1 2 7 设，是一个行动策略，r = 为山的一个实现若 f ( r ) - - - - ，且对v i ( o i 1 ，假设结论对证明长度小于f 的公式成立，则设a ，a ( a o b ) 是 a 的一个基本反应，分两种情况讨论： ( a ) 若a 由a ，a 1 ) 一，a ，昂规则得，则a = a ( 1 i 礼) 由于a 的证明 长度为z l ，故三卜f 一1 ， ( b ) 若a 由a 的一个基本行动4 ”及a 一规则得，则不妨设a ”= a ( f 。c ) 为证明叙述方便，对任意公式p i q ，将a ( f o p , a o q ) 缩写为a l p , 剜设r o ( a ) = g n c i ，a o ( a ) = b o n b l ，则c = g ，b = b ( i ，j 1 0 ，1 ) ) 于是有a = a nq ，岛nb 1 ，a ，_ a c o 几g l ，岛 ，a ”= a a ，b o n b 1 令a = a 盼，b j ， 1 】 则显然a m 是a 的一个基本行动，是a ”的一个基本反应由于a ”的证明长度为 z 一1 ，所以由归纳假设得l 卜- f 一2a 叉a 是a 7 的基本行动，运用a 一规则可得 l 卜l 一1a 综合( i ) ，( i i ) 两步所得引理2 2 1 成立 口 定理2 2 1 ( 可靠性定理) 若l 卜a ，则a 是可完成的 证明：设工卜l a 对f 进行归纳证明 要证a 是可完成的，只须找到一个行动策略，使得，完成a ( i ) 若f = 1 ，a 为公理，即a 为经典逻辑中的定理，由命题1 3 1 有对任意状 态s ，s ( a ) = 1 现定义，设r 为任意实现，定义f ( r ) = 因a 为原始公式， 只有唯一实现 ，所以，策略下a 的任意实现 关于8 成功故，完成 a ，即a 是可完成的 ( i i ) 假设定理对证明长度小于2 时成立( f 1 ) 现设三卜fa ，分两种情况讨 论： ( a ) 若a 由其基本行动运用a 一规则推得，则a 7 的证明长度小于；，由引理 2 2 。l 得的每个反应的证明长度也小于f 。设出，群是川的所有反应，由归 纳假设得，存在一组行动策略，1 ) 一， 分别完成础，越因为a 由a - 规则得 到，不妨设f ( a ) = b o n b l ，a = a ( f b o ) 定义，如下： ( 1 ) ，( ) = r b o 笔x ( 2 ) 对任意实现 1 ) ，其中a 1 = 玛0 1 ，南) ) ，( ) = 1 ) 下证该，完成a 由定义知，策略下a 的每个实现都具有形式 ( m o ) ，其中y 是a 的反应，从而也是a ( x ) 的反应由于a ( x ) = ，因此a ( x ，y ) 也是的一个反应故a ( x ，y ) = a ；，0 l ，七) ) ，于是， 策略下a 的实现具有形式 又 是厶策 略下群的实现，且矗完成群，所以 关于任意状态s 成功 由引理1 3 1 得s ( a 二) = 1 而a ：同时也是 的最后个公 式故由，的定义( 2 ) 得，完成a ( b ) 若a 由万，a l ，a 。用b 规则推得，设b 】j | 一，凤是a 的所有真反应 ( 这样，4 h 一，a 。 b i ，风) ) 由引理2 2 1 知它们的证明长度小于f ，故由 归纳假设知存在行动策略 ， 分别完成它们如下定义，： ( 1 ) ，( ) - - - - ； ( 2 ) 对任意实现 ( n 1 ) q = b i ，( i 1 ，女) ) ，( ) = ( ) 1 2 下证该，完成a 设f 策略下a 的任意实现为 ，对任意状 态s ，下只须证 关于s 成功分两种情况讨论： ( 1 ) 若p2o ， 则 关于s 成功兮5 ( a ) = 1 而事实上，l 卜- 才，五是经典命题中定理，故 5 ( a - - ) = 1 又由命题1 3 2 得s ( a ) = s ( 万) ；1 ；( 2 ) 若p 芝1 ，由于，( ) = ， 则朋必为a 的一个真反应所以不妨设朋= b j ( j 1 ，) ) 则由f 的定义 ( 2 ) 知 是，j 策略下郴的实现因厶完成a ：，故s ( a ；) = 1 而雒 也是 的最后一个公式故，完成a 综合( i ) ( i i ) 两步可得可靠性定理成立 口 引理2 2 2 设，为一个行动策略，a f ( s ) ，( ) = x ，y 是a 的一个 反应，若a ( x ，y ) 不是可完成的，则，不完成a 证明用反证法假设，完成a 对，策略下a 的任意实现 ， 我们定义策略，7 ，使得，7 ( ) = ，( ) 因a ( x ，y ) 不 是可完成的。所以，不完成a ( x ，y ) 故存在某状态s 和，策略下a ( x ，y ) 的某实 现r = ，使得s ( 如) 1 而也是 的最后一个公式，救它关于s 不成功这与假设矛盾 口 引理2 2 3 若l 矿a ，则a 是不可完成的 证明设三矿a ，对a 的附加度进行归纳证明： i ) 设a 的附加度为0