(逻辑学专业论文)基于信念的动态偏好逻辑.pdf_第1页
(逻辑学专业论文)基于信念的动态偏好逻辑.pdf_第2页
(逻辑学专业论文)基于信念的动态偏好逻辑.pdf_第3页
(逻辑学专业论文)基于信念的动态偏好逻辑.pdf_第4页
(逻辑学专业论文)基于信念的动态偏好逻辑.pdf_第5页
已阅读5页,还剩52页未读 继续免费阅读

(逻辑学专业论文)基于信念的动态偏好逻辑.pdf.pdf 免费下载

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

论文原创性声明 本人郑重声明:所呈交的学位论文,是本人在导师的指 导下,独立进行研究工作所取得的成果。除文中已经注明引 用的内容外,本论文不包含任何其他个人或集体已经发表或 撰写过的作品成果。对本文的研究作出重要贡献的个人和集 体,均已在文中以明确方式标明。本人完全意识到本声明的 法律结果由本人承担。 学位论文作者签名:後名l 竿 日期:州年月岁日 学位论文使用授权声明 本人完全了解中山大学有关保留、使用学位论文的规 定,即:学校有权保留学位论文并向国家主管部门或其指定 机构送交论文的电子版和纸质版,有权将学位论文用于非赢 利目的的少量复制并允许论文进入学校图书馆、院系资料室 被查阅,有权将学位论文的内容编入有关数据库进行检索, 可以采用复印、缩印或其他方法保存学位论文。 学位论文作者签名:径铍罕导师签名: 魄俳6m 魄1 1 1 1 年 6 月弓 日 气ji : 论文题目:基壬值金的麴查偏妊逻辑 专业名称:逻塑堂 申请人:筮丛堡 指导老师:奎型二五数拯 摘要 偏好和信念密切相关。我们将在本文中用模态逻辑的方法处理信念和偏好。 在信念偏好静态系统中,我们在信念逻辑k d 4 5 中引入了偏好算子和若干新公 理。在信念偏好动态系统中,我们关注偏好的改变,并且引入新的活动类型。最 后,我们证明文中提到的系统都是可靠的和完全的。 关键词:动态、偏好、信念、可靠性、完全性 i v t i t l e : m a j o r : a p p l i c a n t : s u p e r v i s o r : p r o f e s s o rx i a o w uli a b s t r a c t t h e r e sac l o s ec o n n e c t i o nb e t w e e np r e f e r e n c ea n db e l i e f w ew i l ls h o wh o w b e l i e fa n dp r e f e r e n c ec a nb et r e a t e ds y s t e m a t i c a l l yi nt h ef o r m a to fm o d a ll o g i c i nt h e s t a t i cs y s t e mo fb e l i e fa n dp r e f e r e n c e ,ap r e f e r e n c eo p e r a t o ra n dn e wa x i o m sw i l lb e a d d e di nt h eb e l i e fl o g i ck d 4 5 i nt h ed y n a m i cs y s t e mo fb e l i e fa n dp r e f e r e n c e ,w e w i l lf o c u so nt h ec h a n g e so fp r e f e r e n c e ,a n di n t r o d u c en e wa c t i o nt y p e s f i n a l l y , w e w i l lp r o v et h a ta l lt h es y s t e m si nt h i sa r t i c l ea r es o u n da n d c o m p l e t e k e yw o r d s :d y n a m i c s ,p r e f e r e n c e ,b e l i e f , s o u n d n e s s ,c o m p l e t e n e s s v 目录 弓i言l 第一章信念偏好逻辑的理论基础3 1 1信念逻辑3 1 2 序逻辑6 第二章静态信念偏好逻辑9 2 1 静态信念偏好逻辑的语言9 2 2 静态信念偏好逻辑的语义1 0 2 3 静态信念偏好逻辑的公理化1 2 2 4 可靠性1 4 2 5 完全性1 6 2 6 信念与偏好2 2 第三章动态信念偏好逻辑2 7 3 1 动态信念偏好逻辑的语言、语义和公理化2 7 3 2 可靠性和完全性3 0 结语4 0 参考文献4 2 后记4 4 v i 一、选题意义 引言 偏好的概念在许多学科中都有所涉及,例如:哲学、经济学、决策论、最优 化理论、人工智能和博弈论等。个人的偏好在决定个人决策和行动时起到至关重 要的作用。 v o nw r i g h t 在 1 3 中将偏好分为两类:外在偏好和固有偏好。他详细讨论 了固有偏好,给出了固有偏好的形式系统。v o nw r i g h t 没有详细讨论外在偏好, 而且他将产生偏好的原因和偏好改变的可能性都排除在讨论范围之外。但匙偏 好不是静态的,它是可以改变的。此后逻辑学家对产生偏好的原因和偏好的改变 进行了大量的研究。 在现实生活中,我们经常处于信息不完备的情况。于是,我们的偏好很大程 度上取决于我们的信念。例如:“我相信天要下雨,所以我更愿意带上我的伞。” 所以在同一逻辑系统里同时刻画信念和偏好之间的关系具有十分重要的意义。 二、文献综述 在本文中,静态的信念逻辑我们采用的是经典的k d 4 5 系统。对静态信念逻 辑k d 4 5 系统的详细讨论可以参见 1 2 和 9 。a g m 模型对现代的动态信念逻辑 刻画有重要影响,但是a g m 本身并没有给出信念修正的逻辑系统,只是提出信 念修正过程中应该满足的抽象假设。对a g m 的详细讨论可参见 1 4 。在模态逻 辑框架下讨论信念修正可参见 1 1 和 1 5 。 静态的偏好逻辑我们采用的是序逻辑系统。将此系统作为偏好逻辑的详细讨 论可参见 7 ,关于序逻辑更一般的结论可参见 8 。 8 中给出了静态序逻辑的 。关于外在偏好和固有偏好的区别可参见 1 3 :p 1 4 。 l 语义和公理化系统,并在此基础上引入了公开宣告、字典序更新和偏好更新三种 基本活动类型,并证明了相应的静态和动态系统的可靠性和完全性。 在 6 和 1 0 中,j o h a nv a nb e n t h e m 和刘奋荣给出了同时包含知道算子和偏 好算子的静态公理化系统,并证明了该系统的可靠性和完全性。然后又用公开宣 告和公开建议两类活动对上述系统做了动态扩充。在 6 中,刘奋荣还给出了基 于二元偏好算子且包含信念算子的逻辑系统。在 8 中,p a t r i c kg i r a r d 也用模态 逻辑的方法研究了偏好与信念的关系。 关于偏好逻辑详细的综述类文献可参见 1 6 ,本文中使用到的模态逻辑的基 础知识可以参见 1 和 2 。动态逻辑的基础知识可参见 4 ,动态认知逻辑的基础 知识可参见 9 。 三、论文安排 第一章介绍了信念逻辑k d 4 5 和序逻辑的基本结论,为以后章节的展开奠定 了理论基础。 第二章详细研究静态的信念偏好逻辑。在2 1 节中,我们将信念逻辑k d 4 5 和序逻辑结合在一起,定义了信念偏好逻辑语言l m , ;2 2 节给出了静态信念偏 好逻辑的基本语义概念,定义了信念偏好框架b p f 和信念偏好模型b p m ;2 3 节给出了静态信念偏好逻辑的公理化系统b p s ,并定义了一些基本的句法概念; 2 4 节和2 5 节分别证明了b p s 的可靠性和完全性:最后,在2 6 节中,我们在 b p s 中加入两条直接刻画信念和偏好之间关系的公理,并证明了扩充后的公理化 系统b p s + 也是可靠和完全的。 第三章主要研究偏好的改变。我们用“公开建议 活动扩充了静态信念偏好 逻辑语言三即,在b p s 基础上加入若干归约公理构成动态信念偏好逻辑的公理化 系统d b p s ,证明了d b p s 的可靠性和完全性。 最后,在结语中我们说明了取得的结论和进一步研究的方向。 2 第一章信念偏好逻辑的理论基础 在这一章中,我们简要介绍下文中将使用到的两类逻辑:信念逻辑和序逻辑。 信念逻辑我们采用的是经典的k d 4 5 系统,对此详细的讨论可参见 1 2 和 9 。 关于序逻辑的详细介绍可参见 8 。 1 1 信念逻辑 在这一节里,我们简单介绍基础信念逻辑,给出基础信念逻辑的形式语言、 语义和公理化系统。 定义1 1 1 ( 基础信念逻辑) :令尸是可数原子命题集合,彳是主体符号的有 限集合,基础信念逻辑语言如由下面b n f 构成: 伊:= pi 1 妒i ( e p 咖i 饬驴,其中p p ,a 彳。 这里,基础信念逻辑语言如的构造是在命题逻辑语言基础上对a 中每一个主体 口加入一个信念算子b o ,玩缈被解释为“主体口相信伊 。我们用f o r m l 嚣表示 t 所有如的公式组成的集合。- 定义1 1 2 ( 缩写定义) : ( d r y )( 缈v 咖= d f - - a ( - - a ( p 人1 ; ( d f - - ) ( 缈j 咖= d f _ 1 ( 缈 1 咖; ( d f :叫( 伊h 气f ( ( 缈j ( 妒寸咖) ; ( d r t ) t2 d f p v 刊; ( d 札) 上= d f - a t 。- i 注意: ( 1 ) 为了简洁,我们通常用“j ”表示元语言意义上的“如果那么”, 用“ 表示“当且仅当”,“表示“并非”。 。b n f ( 巴科斯范式) 是b a c k u s n a u rf o r m 的缩写,是由j o h nb a c k u s 和p e t e r n a u r 首次引入一种 形式化符号来描述给定语言的语法。 3 ( 2 ) 为了节省括号,我们约定公式最外面的括号可以省略。公式所含的联 结词相对公式的结合力按下列顺序依次减弱: 1 ,b 口,a ,v , ,h 。 ( 3 ) 同类联结词满足右向结合律。例如,我们用仰_ 一仇表示: 仰j ( 仇专一( 铷一1 一仇) ) 。 ( 4 ) 定义1 1 2 和上述约定( 1 ) 一( 3 ) 在全文中适用。另外,下文中出 现的一元联结词的结合力都强于二元联结词的结合力。 我们用经典的克里普克语义解释基础信念逻辑语言,下面首先给出信念框架 的定义: 定义1 1 3 ( 信念框架b f ) :称f = 是信念框架,当且仅当下列条 件满足: ( 1 ) f 嘿非空集合,其中的元素称为可能世界; ( 2 ) 是一个函数,给爿中每一个主体a 指派一个形上的二元关系( 力, 并且对任意口a ,( 口) 满足: 对任意w 形存在u 肜使得r a w u ;( 持续性) 对任意w ,u ,v 形r a w u 且r 口“vjr a w v ;( 传递性) 对任意w ,u ,暇r 口w u 且r a w v r 口u v 。( 欧性) 我们通常称这种二元关系为信念通达关系。- 在信念框架的基础上,我们给出信念模型的定义: 定义1 1 4 ( 信念模型b m ) :称m = 是信念模型,当且仅当 下列条件满足: ( 1 ) 是信念框架,此时我们称形是m 的论域,记为d ( 蚴; ( 2 ) 旷:pjp ( 即是一个赋值函数:对任意p p 指派一个形的子集矿( p ) 。 直观上,矿0 ) 是p 在其上为真的可能世界的集合。1 有了信念框架和信念模型的概念,我们就可以定义可满足和有效等语义概 念。在定义这些语义概念前,我们先给出信念点模型的定义: 定义1 1 5 ( 信念点模型) :称二元组( 必w ) 为信念点模型,当且仅当下列 条件满足: 国也称为“点”或“状态”。 国我们通常将( 口) 记为心,并且对r , , w u ,m ,心计和( w ,) r , , 7 5 :0 n 分。 4 ( 1 ) m 是信念模型; ( 2 ) w d ( 蚴。 我们通常将( 必w ) 记为必w 。- i 我们在信念点模型上解释什么是一个f o r m l 矗中的公式在模型上的一点可 满足: 定义1 1 6 ( 真值定义) :给定信念模型m = ,归纳定义班( m w ) 上可满足( 或真) ,记为必w 缈: 必w p 营w v p ( p ) ,其中p 尸; 必w 伊a 沙必w 殂mw | 5 f ,; 必w 1 妒营并非必w 缈; 必w 优妒v u w ,w r 口ujmu 缈。- i 我们也将“并非必w 矿记为:mw 乒妒。如果对任意的w d ( 蚴有必w 9 ,我们称征m 上为真,记为m 缈。如果对任意的信念模型m 有m 仍我们 称堤b m 有效的,记为b m 妒。同样,我们用m 皓瘫示“并非m 缈 ,用b m 皓婊示“并非b m 缈”。 在定义了上述语义概念后,我们下面给出基础信念逻辑的公理化系统: 定义1 1 7 ( 公理化) :基础信念逻辑的公理化系统k d 4 5 定义如下: ( 1 ) 公理: ( t a u t ) 所有命题重言式的代入特例; ( k )以妒_ _ 既缈_ 玩沙; ( d ) 1 成j - ; ( 4 ) b a 缈叶既既缈; ( 5 ) 1 玩缈一既1 b a 缈。 ( 2 ) 规则: ( m p ) 仍缈_ 少 f ,; ( r n b ) 缈玩伊。- t 我们对定义1 1 7 中的公理作一些说明: k 公理表明信念算子玩对蕴涵是可分配的。d 公理表明主体的信念是内在 一致的。可以证明加入d 公理和加入既缈一- 1 既- 1 砟为公理得到的公理系统是 等价的,直观意义是主体相信僦不能同时相信1 缈。4 公理和5 公理表明相信是 一种具有反思能力的活动,其中4 称为正反思:主体相信僦相信自己相信伊;5 公理称为负反思:主体不相信械相信自己不相信缈。 有了公理化系统k d 4 5 ,我们就可以定义什么是硅此系统中可证: 定义1 1 8 ( 形式证明) :称公式序列仰,仇是k d 4 5 中的形式证明,当 且仅当对每一f 使得l f 疗,下列条件至少有一个成立: ( 1 ) 仍是k d 4 5 的公理的代入特例; ( 2 ) 存在,k f 使得纺是从纺和仇据m p 得到; ( 3 ) 存在j f 使得纺是从纺据r n b 得到。 称蔽k d 4 5 中有形式证明存在k d 4 5 中的形式证明伊l ,铷使得铷= 缈。 称堤k d 4 5 的定理,记作 - k d 4 5 缈缈在k d 4 5 中有形式证明。1 由模态逻辑的知识,我们可以证明基础信念逻辑的可靠性和完全性: 定理1 1 9 ( 刻画定理) :对任意伊f o r m l b ,i - - k d 4 5 伊b m 印。- i 1 2 序逻辑 在这一节里,我们介绍序逻辑。序逻辑的直观思想我们将在下一章借助信念 逻辑给予说明,在这里我们只给出重要定义和结论。 定义1 2 1 ( 序逻辑) :令p 是可数原子命题集合,序逻辑语言三d 由下面 b n f 构成: 伊:= pl _ 1 伊i ( 缈人i 口s 缈iu 矽,其中p p 。 我们用f o r m l d 表示所有d 的公式组成的集合。我们将口s 和u 的对偶算子分 别记为和e 。_ 定义1 2 2 ( 序框架o f ) :称 ,归纳定义班( w ) 上可满足( 或真) ,记为必w 仍 必w p w 矿p ) ,其中p p ; mw 妒a c ,必w 俎必w 砷; 必w 1 缈营必w 桀仍 a 磊w b a c p v u ,w r s a uj 正u 缈; 必w p r e t 口缈v u w ,w 妄“j 必u 弘 必w u 矽营v u 形,必z , 妒。一 如果在w ) 上亦可满足,我们记为mw 肄缈,此时也称碚( 必w ) 上假。在不 致混淆之处,我们通常省略m ,将必w 徊为w 缈,将必w 壮徊为w 皓伽 有了上面的定义,我们就可以将矿扩充为定义域是f o r m 即的赋值函数n 将坎劝定义为: 坎劝= d f wmw 缈) 。 下面我们给出一些常用的语义术语的定义,在这些定义中出现的框架或模型 不只局限于信念偏好框架或模型。 定义2 2 4 :称公式黼w ) 上可满足,记为必w 三 营v 缈己必u 伊。 一 定义2 2 5 : ( 1 ) 公式征模型m 上真,记为m 伊v w 形,必w 矽: ( 2 ) 公式征模型m 上可满足营3 w 矿,使得mw 仍 ( 3 ) 公式集跪模型m 上真v w 形,尬w 眨; ( 4 ) 公式集脏模型m 上可满足营3 w w ,使得必w 眨; ( 5 ) 公式维模型类m 上有效( 或真) ,记为m 印铮v m m ,肘 缈。- 定义2 2 6 : ( 1 )公式硅框架肚一点w 有效,记为ew 伊v 矿, ,w 仍 ( 2 ) 公式征框架趾有效,记为f # :伊v w 严,ew 驴; ( 3 ) 公式碓框架类f 上有效,记为f 缈营v f f ,f 仍 ( 4 ) 公式缔效,记为 缈疵所有框架上有效。- f 是任意框架类,我们用v 柚( f ) 表示f 上所有有效公式组成的集合,即, v a i ( f ) = d f 伊if 驴) 。 定义2 2 7 ( 局部语义后承) :令s 是一模型类或框架类,腥一公式集,我 们称公式硝配相对于s 的局部语义后承,记为三t = s 缈营v m s ,w m , 必1 4 醪j 必w p 。 一 2 3 静态信念偏好逻辑的公理化 定义2 3 1 ( 公理化) :信念偏好逻辑的公理化系统b p s 定义如下: ( 1 ) 公理: ( t a u t ) 所有命题重言式的代入特例; ( k ) p r e t 口( g o _ _ p r e f 口妒一 p r e f 口y 饬( 妒_ 咖_ 既缈一玩沙 矾缈一们一跏一嘶; ( d ) 1 晚上; ( t ) p r e t 口缈一矽 u g o _ 够; ( 4 ) p r e f 口伊_ p r e f 口 p r e f 口缈 b 0 9 _ b 口b d 9 ; ( 5 ) e g o _ u e g o - 1 b d 9 + b d 、b d 9 ; ( i n c l ) u g o _ b a g o ; ( i n c 2 ) 坳j p r e q 口伊。 。若f = 彬胁,我们用w f 表示,ew ,wem 的用法与此类似。 。若s 是框架类,m s 指基于s 中框架的模型。 1 2 ( 2 ) 规则: ( m p )仍缈_ 】;f ,| ;f ,; ( r n p )缈 p r e q 口仍 ( r n u ) 伊u r p , ( r n b ) q , b a r p 。- i 我们在b p s q b 加入了新公理( i n c l ) 。在从卜述定义我们可以看出,除了公理 ( i n c l ) 夕b ,信念偏好逻辑的公理化系统b p s 的公理是由我们在第一章中介绍的信 念逻辑和序逻辑的公理组成,信念偏好逻辑中的 p r e f 口与序逻辑中的口s 具有相同 的逻辑性质。信念偏好逻辑和信念逻辑相同,都是用经典的k d 4 5 系统解释信念 算子饬。 对于公理u r p - - b a 研口唧一 p r e q 4 缈,我们将它们分别命名为( i n c l ) 和( i n c 2 ) 。 这里i n c 是英文单词i n c l u s i o n 的缩写。在2 5 节中我们将看到这两条公理提供的通 达关系间的包含关系是完全性成立的必要条件。 下面我们给出一些常用的涉及公理化系统的术语定义,在这些定义中出现的 公理化系统不只局限于系统b p s 。 定义2 3 2 ( 形式证明) :令x 是任意的公理化系统,其公理黝x l ,a x n , 推理规则是r 甜i ,r ,其中每一个推理规则尺哆( ,劝形如“仰,纺”( 我 们用肪表示推理规则r 甜,的元数) 。征x 中的形式证明是有穷公式序列仰,铷, 满足: ( 1 ) c p m = 积 ( 2 ) 公式序列中的每一个仍或者是公酌x l ,吒之一的代入特例,或者是 通过对公式序列中出现在纺之前咖矗个公式使用规则月甜,( ,勋得到。 我们用畋瘫示存在疵x 中的形式证明。当x 在上下文中清楚时,我们也简 单记为卜弘此时我们也称堤x 的定理。如果师是x 的定理,我们记为呶妒。我 们将x 的所有定理组成的集合记为t h ( x ) 。- i 定义2 3 3 ( 推演) :令厂u 纠是一公式集,称征x 中有删推演( 记为 ,畋伊) ,如果存在有穷序列肌,臌得: 畋】5 f ,l 人_ 缈。 1 3 如果不存在硭x 中枷推演,我们记为厂呶缈。- i 如果嘿有穷公式集合,其中公式为妒l ,蛳,我f 门用八嘹示la 。 另外,我们约定八f 2 j = t 。 定义2 3 4 ( x - 一致) :公式赧x 一致的,如果厂呶上。否则,称腥x 不一致的。公式碾x 一一致的,如果 纠是x - 一致的。否则,称堤x - 不一致的。 一 引理2 3 5 :厂恢垆营厂u - 1 咖是x 一一致的。 证明:( 1 ) 厂恢妒jf u - 1 纠是x - 一致的。 假设,u - 1 纠不是x - 一致的,则存在有穷子集罗厂u - 1 仍,使得: b 【八罗_ 上 容易看出,必存在有穷公式集西少,使得_ 1 妒萑西且 b 【八西 矽一上 于是有 k 八西_ 即厂呶够。 ( 2 ) 厂u 1 纠是x 一一致的jfb x 伊。 假设,畋妒,由定义2 3 3 易得: 厂u 办k9 ,u 1 办呶 妒 于是 厂u - 1 缈) 畋j i i 口f u 1 谚不是x - 一致的。- 定义2 3 6 ( 正规系统) :如果公理化系统x 包含公理口( 伊_ 们一口伊_ 口 y 和规n q , 口妒,则称x 是正规系统。 由定义2 3 6 ,我们前面提到的公理化系统都是正规系统。 2 4 可靠性 这一节里我们要证明信念偏好逻辑公理化系统b p s 的可靠性。首先我们从一 1 4 般意义上定义什么是可靠性。 定义2 4 1 ( 框架可靠性) : 果v 伊,i - x 伊j 伊v 赳( f ) 。- t 定义2 4 2 ( 模型可靠性) : 如果v 够,t - x 缈jm 缈。- i 令f 是一框架类,正规系统x 相对于f 可靠,如 令m 是一模型类,正规系统x 相对于m 可靠, 通常证明公理化系统的可靠性是容易的,只要我们验证公理化系统的公理是 有效的,推理规则保持有效性即可。 引理2 4 3 :b p s 的公理是c b p f 上的有效式。 证明:我们举例验证定义2 3 1 中的公理。 考虑公理 p r e f 口妒_ p r e t 口 p r e q 口缈。我们要证明:v f c n p v , f # p r e f 口伊_ p r e t 口 p r e f 口缈, 也就是v v , w 只 , w # : p r e f 口缈_ p r e t 4 p r e f 口缈。 假设w 忙 p r e f 口伊一【p r e f 口 p r e f 。缈,于是 w # : p r e f 口矽 且 w # :1 p r e f 口 p r e t 口缈 由,j ,f ,使得:w u ,u v 且,# _ 1 妒。由毛的传递性,有岛w ,与矛 盾。 其它公理可以类似验证。- 引理2 4 4 :b p s 的规则相对于c b p f 保持有效性。 证明:我们验证规则i p 。设妒v a l ( c b p f ) ,往证 p r e f 口缈v a l ( c b p f ) 。由缈 v a i ( c b p f ) ,有v f c b p f ,v v , w e ,w 缈。由w 的任意性,有v kw e ,w p r e t 口伊,i 1 1 p r e t 口驴v a i ( c i l p r ) 。- i 定理2 4 5 :信念偏好逻辑的公理化系统b p s 相对于信念偏好框架类c b p f 是 可靠的。 证明:由引理2 4 3 和引理2 4 4 。_ 用类似的方法我们也可以证明信念偏好逻辑的公理化系统b p s 相对于所有 信念偏好模型组成的类也是可靠的。 下面我们讨论b p s 相对于c b p f 的强可靠性。 定义2 4 6 ( 框架强可靠性) :令f 是一框架类,正规系统x 相对于f 强可靠, 如果对任意公式集厂u 伊) ,f t - x 缈j 厂唧缈。- i 定理2 4 7 :信念偏好逻辑的公理化系统b p s 丰n 对于信念偏好框架类c b p f 是 强可靠的。 证明:设厂i - - b p s 矽,由定义2 3 3 ,有存在有穷序列缈l ,腋得: 卜b p s 沙la 一妒。 如果对v m c b p f ,w m ,有mw 厂,则mw 叩1 a 。 由定义2 2 6 、定义2 4 1 和定理2 4 5 ,我们有: mw 沙la a 一妒。 于是,必w 妒。由定义2 2 7 ,有 i = c b p f 妒。- t 2 5 完全性 在上一节中,我们证明了信念偏好逻辑的公理化系统b p s 相对于信念偏好框 架类c b p f 是可靠的,即v 伊,i - - b p s 伊j 缈v a l ( c b p f ) 。这一节中我们将证明相反 方向也是成立的:v 缈,缈v a l ( c b p f ) j 卜b p s 伊( ) 。这种性质在逻辑中被称 为完全性。实际上,我们证明的是信念偏好逻辑的公理化系统b p s 相对于信念偏 好框架类c b p f 的强完全性,( ) 是此强完全性的一个直接推论。为了书写方便, 我们只考虑单主体情况,所以我们省略了各模态算子的下标“a ”。我们先从一般 意义上定义什么是强完全性和( 弱) 完全性。 定义2 5 1 ( 框架完全性) :令f 是一框架类,正规系统x 相对于f 强完全, 如果对任意公式轲u 磅,厂唧妒jf t x 仍 正规系统x 相对于f ( 弱) 完全,如果对任意公式缈,f 缈jt x 矽。- 定义2 5 2 ( 模型完全性) :令m 是一模型类,正规系统x 相对于m 强完全, 如果对任意公式轲u 辨,厂嘞伊固j ,畋仍 。参见定义2 2 7 。 。参见定义2 2 7 。 。参见定义2 2 7 。 1 6 正规系统x 相对于m ( 弱) 完全,如果对任意公式仍mb 缈j 畋伊。- i 在证明完全性的过程中,我们经常使用下面的引理: 引理2 5 3 ( 完全性引理) :令s 是一框架类或模型类,正规系统x 相对于s 强完全营对于每一个x 一致公式集厂,存在模型m s ,使得脏模型a 七可满 足。 正规系统x 相对于s ( 弱) 完全营对于每一个x 一致公式矽,存在模型m s ,使得蔽模型m 上可满足。 证明:我们只对强完全的情况给予证明。 ( 1 ) “仨 假设x 相对于s 不是强完全的,则存在公式集,u 纠,使得厂心呶伽 由后者和引理2 3 5 ,有厂u - 1 纠是x - 一致的。则据题设,存在模型m s ,使 得厂u - 1 办在模型m 上可满足,但是这与厂帝盾。 ( 2 ) “j ” 假设x 相对于s 强完全且存在x 一致公式集厂,使得对任意模型m s ,v w mmw 乒f o 于是,有v m s ,v w m 必w 厂j 必w 上。 所以厂上,再由强完全定义2 5 1 或2 5 2 ,我们有厂畋_ l ,这与厂是x 一一致公 式集矛盾。- 1。 我们采用典范模型的方法证明完全性,为此先定义极大一致集的概念: 定义2 5 4 ( x 极大一致) :公式集厂是x 极大一致的,如果厂是x 一致的, 并且对任意公式集p 满足厂c - , ,有p 不是x 一致的。_ 引理2 5 5 :令x 是正规系统,胰x 极大一致集,则: ( 1 ) 耐m p 封闭:仍伊_ y 厂j 沙几 ( 2 ) t h ( x ) 厂 ( 3 ) v 伊,妒,或1 缈厂 ( 4 ) v 仍v :伊vy 厂c 缈,或y 厂 ( 5 ) v 仍| ;f ,:缈人j ;f ,厂车缈厂且 f ,f o - t 引理2 5 6 ( l i n d e n b a u m 引理) :如果厂是x 一致集,则存在x 极大一致 证明参见 1 :p p 9 0 9 2 。 。证明参见 1 :p p 8 8 9 0 或 2 :p 1 9 7 。 1 7 集广使得厂互广。_ 1 我们假设正规系统x 中出现的必然化模态算子为 口f ) f ,其中堤某指标 集。它们相应的对偶算子为 ,) ,e ,。例如,信念偏好逻辑的公理化系统b p s 中 出现的b , p r e q 和螂是必然化算子。它们相应的对偶算子分别为:b , 乘q e 。下面我们给出x 的典范模型的定义: 定义2 5 7 ( 典范模型) :正规系统x 的典范模型肝是多元组: fe , 其中: ( 1 ) 矿是所有x 一致公式集的集合; ( 2 ) vf i ,r ;矿矿,且满足:r 。, w u v 妒,妒uj l 伊w ,r ; 也称为f ( 或口,) 的典范通达关系; ( 3 ) 矿p ) = w 旷ip w 。 二元组 矿,r p fe ,称为x 的典范框架。- 1 引理2 5 8 :令x 是j 下规系统, f 。,是x 的典范模型,则r ;w “ v 伊,口f 缈wj 缈甜。- i 引理2 5 9 :令x 是正规系统, fe ,是x 的典范模型,则对于任 意的w 矿: ( 1 ) f 伊w 3 u 旷,使得r ;w “且伊甜; ( 2 ) 口f 妒w 营v u 矿,g 。, w uj 缈u 。1 引理2 5 9 在证明下面的真引理过程中起到关键作用。 引理2 5 1 0 ( 真引理) :令x 是正规系统,膨是x 的典范模型,则对任意 公式缈,肝,w 缈营缈w 。1 我们从定义2 3 1 中可以看出,我们通常将形如口缈一妒,口缈_ 口口妒,1 口上和伊_ 口缈的公理分别称为t 公理、4 公理、d 公理和5 公理。下面我 们给出这些公理的对应定理,对应定理揭示出了含有上述公理的正规系统的典范 我们只考虑一元模态算子,对于多元模态算子的讨论可参见 2 。 罾证明参见 1 :d 9 4 。 母证明参见 1 :p 9 7 。 田证明参见 1 :p p 1 4 0 1 4 l 。 1 8 模型应该具有的性质。 定义2 5 1 1 :令堤模态公式,么 二元组 ,有: 是一阶公式,称卿a 对应对任意的 p a 。 一 注意:我们在 每够 a 中第一次使用 是表示关系 框架,而第二次使用 是表示一阶关系模型。 引理2 5 1 2 ( 对应定理) : ( 1 ) d 公理对应持续性; ( 2 ) t 公理对应自返性; ( 3 ) 4 公理对应传递性; ( 4 ) 5 公理对应欧性。- 对应定理告诉我们:d 公理在其上有效的框架,其通达关系一定满足持续性; t 公理在其上有效的框架,其通达关系一定满足自返性;4 公理在其上有效的框 架,其通达关系一定满足传递性;5 公理在其上有效的框架,其通达关系一定满 足欧性。 我们还将用到典范公式的概念,定义如下: 定义2 5 1 3 ( 典范公式) :称公式堤典范公式对任意的正规系统x , k 缈j 征x 的典范框架上有效。- 1 引理2 5 1 4 :t 公理、d 公理、4 公理和5 公理都是典范公式。 证明:我们只证明4 公理是典范公式,其余公理的证明方法类似。我们的证 明分为两步: ( 1 ) 首先证明含有4 公理的正规系统x 的典范框架都是传递框架; ( 2 ) 然后证明4 公理在传递框架上有效。 注意到由定义2 5 1 1 和引理2 5 1 2 ,( 2 ) 已经成立。于是,我们只需证 明( 1 ) 。 我们设4 公理为口9 _ 口口妒,正规系统x 的典范框架中口对应的通达关 系为r 。 。证明参见 1 :p p 1 1 4 1 1 6 。 1 9 v w ,u ,矿,设w r u 且u r v ,要证w r y 。 对任意公式缈,假设口妒w ,由引理2 5 5 ( 2 ) ,有口妒_ 口口缈w , 再由引理2 5 5 ( 1 ) ,有口口伊w 。因为w r u ,由引理2 5 8 ,有口缈u ,又 因为u r v ,所以缈v 。由引理2 5 8 ,有w r y 。 在证明b p s 的强完全性之前,有必要先作一些说明。通常我们是应用引理 2 5 3 来证明强完全性的,即证明对于每一个x 一致公式集八存在模型m s , 使得厂在模型m 上可满足。而存在的模型m 就是我们广卜面提到的典范模型, l i n d e n b a u m 引理和真引理保证了厂在典范模型上是可满足的。所以,要想证明 强完全性,只需验证典范模型是s 中的模型。但是,当我们在语言中引入全局模 态时,就会出现典范模型可能不是s 中的模型的情况。为了解决这一问题,我们 将使用典范模型的生成子模型。 下面我们给出生成子模型的定义和主要性质: 定义2 5 1 5 ( 生成子模型) :令m = 和m = 是两 个模型,我们称m 是m 的子模型营下列条件满足: ( 1 ) 形形; ( 2 ) r = rn ( 肜,) ; ( 3 ) v p 尸,y = 坳) 厂、。 我们称m 是m 的生成子模型下列条件满足: ( 1 ) m 是m 的子模型; ( 2 ) v w ,w 形且r w vj ,w 。 令m 是一模型,x cd ( 旧,由胜成的子模型定义为m 的论域包绷最小生 成子模型。 由单元集生成的子模型称为点生成子模型。- 1 引理2 5 1 6 :令m 是m 的生成子模型,对任意公式神w m ,有: 必w 缈 m ,w # 妒。 - 定义2 5 1 7 ( 生成子框架) :令f = 和f ,- 是两个框架, 我们称f 是f 的子框架下列条件满足: ( 1 ) 肜形; 毋我们对语言中只含有个一元模态算子的情况给出定义,其余情况与此类似。 西这样的最小生成子模型总是存

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论