（计算机软件与理论专业论文）关于占先结构的相似性研究.pdf

南京航空航天人学硕士学位论文 摘要 本文对占先结构的m 一相似性丌展了研究，主要讨论了卅荆1 似性与等价性之 间的关系，在此基础上讨论了条件断言布尔组合的语言表达能力。获得的主要成 果包括： ( i ) 提出了一种弱化的互模拟概念一m 相似，应用一阶转化技术，基于模型沦 方法和结果，揭示了m 相似性和占先结构等价性之间的密切联系，给出 了判定d i 先结构等价性的充要条件。 f 2 ) 研究了条件断言布尔组合的语言表达能力，给日 了一阶语句等价于条件断 言( 正) 布尔组合的模型论特征。 ( 3 ) 建立了占先结构类可以由条件断言( 正) 布尔组合刻岫的充要条件以及：有 限刻画的充要条件。 关键词： 占先结构m 相似性条f f f 一断言等价性模型论 荚于占先结构的相似性研究 a b s t r a c t m - b i s i m i l a f i t yo ft h ep r e f e r e n t i a ls t r u c t n r ea n dt h ee q u i v a l e n c eo fp r e f e r e n t i a l m o d e l sh a v eb e e ns t u d i e di nt h i st h e s i s 1 1 1 ee x p r e s s i o na b i l i t yo fb o o l e a n c o m b i n a l i o n so fc o n d i t i o n a la s s e r t i o n sa l s oh a sb e e nd i s c u s s e d t h em a i n a c h i e v e m e n to f t h i st h e s i si n c l u d e s ： ( 1 ) t h i st h e s i sh a si n t r o d u c e dan o t i o no fm - b i s i m i l a r i t y ，a n de s t a b l i s h e dt h e r e l a t i o nb e t w e e nm - b i s i m i l a r i t ya n dt h ee q u i v a l e n c eo f p r e f e r e n t i a lm o d e l sa p p l y i n g t h et e c h n o l o g yo fs t a n d a r dt r a n s l a t i o n ，a n dh a sp r o v i d e dt h ec h a r a c t e r i z a t i o nf o rt h e e q u i v a l e n c eo f p r e f e r e n t i a lm o d e l si nt e r m so f m b i s i m i l a r i t y ( 2 ) w eh a v es t u d i e dt h ee x p r e s s i o na b i l i t yo fb o o l e a nc o m b i n a t i o n so fc o n d i t i o n a l a s s e r l i o n s ，a n dp r o v i d e dt h ec h a r a c t e r i z a t i o nf o rt h ef r a g m e n to ff i r s l o r d e rs e n t e n c e ， w h i c ha l ee q u a l i e n tt os o m eb o o l e a nc o m b i n a t i o n so f c o n d i t i o n a la s s e r t i o n s ( 3 ) w eh a v ee s t a b l i s h e dt h ec h a r a c t e r i z a t i o nf o rt h ec l a s s e so f p r e f i j r e n t i a ls t r u c t t t r e c a l lh ee x p r e s s e do rl i m i t e de x p r e s s e db a s e do nb o o l e a nc o m b i n a t i o n so fc o n d i t i o n a l a s s e r l i o l i s k e y w o r d s ：p r e t b r e n t i a ls t r u c t u r e ，m b i s i m i l a r i t y ，c o n d i t i t - n a l a s s e r t i o n s e , l u i x ，a l e n c e ，m o d e lt h e o r y 承诺书 本人郑重声明：所呈交的学位论文，是本人在- t 乎t i | ：i j 旨导一r ，独矗： 进行研究工作所取得的成果。尽我所知，除文中已经注明一川1 川j 内容 外，本学位论文的研究成果不包含任何他人亭有著作牛义的内；亭。列4 i 沦文所涉及的研究工作做出贡献的其他个人和集体，均已在史q 以l 扪 确方式标明。 本人授权南京航空航天大学可以有权保留送交论文的复印件，允 许论文被查阅和借阅，可以将学位论文的全部或部分内容编入有关数 据库进行检索，可以采用影印、缩印或其他复制手段保存论文。 ( 保密的学位论文在解密后适用本承诺书) 箐者签翥i 窒屹2 形 日期： 翅坦世：罗2 彩 南京航空航天大学硕士学位论文 第一章绪论 人l ：智能的发展，迫使人们面对人的常识如何形式化的问题，面对入的常识 推理的形式化问题，即所谓的知识表示和知识推理问题。这里所说的常识以及常 识推理跟通常所说的科学知识以及逻辑推理有本质的区别。首先，常淤具有不确 定性。一个常识可能有例外，一个常识可能是一种尚没有理论根据的或者缺乏充 分验证的经验。其次，常识往往对环境有很强的依赖性。出f 常t 的这种不确定 性，决定了常识推理的非单调性，即依据常识进行通常的逻辑推理，但是保留对 常识的一i 确定性以及环境变迁造成的推理失误的修正权。 尽管早期的大逻辑学家a r cs t o t l e ，l e i h n ：i z ， b o o l e 以及f i e g e 讨论形 式逻辑时均包含常识在其中，但二十世纪的数理逻辑强调的是数学的形式化， w i t t g e n s t e i n 指出经典数理逻辑不适合常识的形式化。如何对常识及其推理进 行形式化已成为人工智能研究领域晟重要和活跃的研究方向之一，开发具备常识 行为能力的系统是人工智能研究的中心目标。 自从图灵奖得主j m c c a r t h y 提倡对常识进行形式化研究以来，常识推理研 究取得了一定的进展，形成了如下几个相对稳定的研究方向：非单调逻辑与信念 变化( n o a m o n o t o n i ci o g i ca n dh e l i e fc h a n g e ) 、关于知识的逻辑( 1 0 9 i c so f k n o w l e d g e ) 、时序摊理( t e m p o r a lr e a s o n i n g ) 、空删推理( s p a t a lr e a s o n i n g ) 以 及关于信念、期望和意图的理论( t h e o r i e so fb e “e f ，d e s i r ea n di n t e n t i o n ) 。 从八十年代以来，非单调逻辑与信念变化的研究获得了广泛的注意，它不但 已成为人工智能研究的重要研究领域之一，而且扩展了经典逻辑的研究范围并在 其中引入了新的观点，近二、三年更多现代数学方法和概念( 拓扑， l l i l b e 】1 t 窀问，l o m mn 理论，代数) 被逐步引入其中。该领域多年的研究取得了一系列 的成果，研究人员从不同直观背景出发提出了多种形式推型l ! 系统，按照构建系统 基本途径的石同，以色列学者a 。b ”c b m a n 将这砦系统大体上分两个范畴 2 0 3 ： 种被称为“解释型非单调推理系统”( e x p l a n a t o r yn o n m o n o t o t i j cr e t s e n i n g ) ， 它包括m c d e f i m o t t 与d o y e 的模态逻辑系统，r e i t e r 的缺省推理( d e f a u i 【 i ( , g ic ) ，逻辑程序设计( 1 0 9 i cp r o g r a m m i n g ) 及m o u r e 的白认i i j 逻辑 ( a u t o e p is t e m i cl o g i c ) 这些早期的非单调推理系统及其变利。近几年由于行动 抑：理研究的需要提出的一些基于因果关系的推理系统亦属f 该范畴。另一种被称 为“占先型非单调推理系统”( p r e f 。e r e n t i a ln o n m o n o t o n i cr e a s o n i n g ) ，它包 挢m c c a r t h y | ，由限定论( c i r c u m s c r i p t i o n ) ，各种非单调后承关系( n o n m o n o t o n i c c o n s e q u e n c er e l a t i o n ，n o n m o n o t o n i ci n f e r e n c er e l a t i o n ) 和信念变化理论。 关于占先结构的相似性研究 陔范畴的形式系统的个重要特征在于：以一种占先结构( 占优结 构) ( p r e f e r e n t i a is t r u c t u r e ) 作为语义结构。例如，非单调后承研究【f i 的极小 型j 吁先模型f 1 0 ，极限型占先模型 2 1 ，e s 结构( e p i s t e m i cs t a t e s s t r u c t u r e ) 3 ，4 ，5 以及信念修正中的部分交模型、球模型、e e 序模型 2 2 以及鹰于距离概念的模型 2 3 等都是一些占先结构。值得一提的足，b o c h m a n 最 近以f s 结构作为语义模型对占先型非单调推理系统的逻辑基础进行了较深入f 门 研究f 5 ，他认为e s 结构为研究这类非单调推理系统提供了统一的语义模型 5 。j 。 这种分类方法反映j 逻辑系统破际为非单调逻辑的两种可能的含义，洋细的讨沦 见 2 i 。本文跨在对择优型非单调推理系统的占先语义结构的若干模型论性质展 丌研究，卜面简要介绍相关的研究背景和现状。 八十年代术期，一批学者) 下始认识到尽管各种具体的非单调推理系统具有自 身研究的价值，但缺少一种刻域非单调推理的一般框架用以对各种系统进行比较 与分类。1 9 8 5 年，g a b b a y 第个提出应当关注于研究非单调逻辑的后承关系 9 。在( kl b l ) a y1 ：作的带动下，m a k i n s o n ，k r a u s ，l e h m a n n ，f r e m l d ，s c h l e c h t a ， b m ：h m a n ，r ，p i n o p e r e z ，c u z c a t e g u i 及m a g i d o r 等批人 钭能j 逻辑学 领域的学者对非单调后承作过深入而广泛的研究。另外值得提及的是，通过 g e n t z e n 型规则刻画非单调后承这种研究方法在人 _ ：智能的其它关于推理的研究 领域也开始采用，例如，c s e h w i n d 用这种方法对因果推理的刻硒 2 7 l ，g o d o 与r 0 r o d r i g u e z 用这种观点考察不确定信息的推理 2 8 ，融p p e r e z 与 c u z c a t e g u i 用这种方法对溯因推理的研究 2 9 ，3 0 ，3 1 非单调后承的研究不但为具体的非单调推理系统提供了一；仲抽象的比较平 台，对于条件知识库而占其本身又是一种推理机制 1 1 。该方向主要的研究内容 包括：非单调后承的证明论性质研究、择优结构的各种形式及相互关系研究、各 种非单凋后承表示定理的研究、如何由有限型后承定义合理的一般后承的研究。 首卅。非单调后承证明论研究的是g a b b a y 本人。他一般化了经典逻辑的后承 关系去掉经典逻辑后承关系中的单调性用以刻画非单调后承，并提出任意非单 调后承关系应满足的三条性质：自反性、切割律及弱单调律( 即m a k i n s o n 的谨单 调律) 。( ；a b b a y 对这三条性质的证明论基础做了研究，但未能提出相应的语义。 m a k i n s o n 对g a h h a y 的： 作做了发展，给出了g a b b a y 系统的语义模型并对一种 贫乏语苦下的系统证明了完备性。除了g a b b a y 提出的三条基本性质外，文献中 还提出了其它各种g e n t z e n 型规则用以约束和刻画非单调后承( 1 2 q 关于这些规 则之间的相互关系，研究人员已做了系统的研究并取得了丰富的成果 1 ，1 0 ，1 l ， 1 2 。 与一。般形式系统的研究类似，在对非单调后承证明沧研究的同时，交织着对 南京航空航天大学硕士学位论文 其语义结构的研究。在该领域主要采用的语义是占先语义，它有极小和极限两种 形式，它是六f 年代逻辑学家h a n s s o n 研究道义逻辑( ( 1 e o n l i c 1 0 9 i c ) 时捉出| 向 语义，最早由b o s s u ，s i e g e 及s h o h a m 引入到非单调后承研究中。目前，l 与 先语义不但成为非难调后承和信念变化研究中的主要语义衙h 计! 知i _ 袭示与推 理的逻辑基础研究中发挥着重要作用，诸多形式系统采纳它为语义结构 2 1 。法 i 司学者1 ( s c h e c h t a 教授日前在其专著中认为，大量的常识推理逻辑系统可以建 构在【i i 先语义基础上 2 1 。 占先语义最显著的特点在于其结构中存在着选择机制，选择机制在数学上川 以通过选择函数或关系加以刻画。由于在择优型非簟凋逻辑研究中，人们 遍接 受法国学者1 1 r o t t 教授提出的一种观点一合理的选择应该是基于( 占先) 关系的 选择 2 5 ，所以，基于关系的占先结构是占先语义叶t 的主要语义结构，下文提到 的占先结构均指该类型的占先结构。 占先结构之所以成为择优型非单调逻辑研究中的主流语义结构，除了它结构 简洁、符合直观外，它具有的高度灵活性也是重要原因，其灵活性至少表现在如 f 两方面： 首先，占先结构中的占先关系可以定义在不同对象上，反映不同对象的优先 顺序，例如，定义在模型集合上反映模型之间优先顺序( 例如，s h o h a m 模型) 、 定义在模型集合的类上反映理论之间的优先顺序( 例如，k l m 的累积模型， m a k i n s o n 的占先模型) 、定义在模型拷贝之间( 例如，k l m 的占先模型) 以及定义 在理沦( 模型集合) 的拷贝之间( 例如，b o c h m a n 的e s 结构) ，y m o i n a r d 对这四 种可能的占先序定义方式进行了较系统的研究 3 2 。 其次，占先结构的占先关系与相应的非单调后承的逻辑性质之间具有高度的 对应性，换言之，在一定程度上，对占先关系性质的约束就会影响所诱导出的非 单凋后承的逻辑性质。在文献中，这种对应性以表示定理形式反映出来，它是非 单调后承与信念变化理论研究最核心的研究内容。在非单凋后承研究领域，第 个涉及此方向研究的是著名学者m a k i n s o n ，但他的工作是基于一种比较甲乏的 语言进行的，一年以后s k r a u s ，d l e h m a n n 及m m a g i d o t 在一般命题逻辑语 言下分别为累积后承及占先后承建立了表示定理 1 0 ，这是非单调后承研究中第 一个建立的蓐要表示定理。白此以后各种类型后承的表示定理被建立起来。另外， 近三年中已有三部择优型非单调逻辑方面的专著用很大的篇幅从不同角度阐述 了占先关系与相应的非单调后承的逻辑性质之间的对应性 4 ，2 l ，2 5 ，该方向 研究受到研究人员的重视程度由此可见一斑。但是，我们认为该方向的研究仍然 属于起步阶段，主要理由有如下几方面： 其一，存在较多占先结构类的表示定理没有得到建立 3 ，8 ，1 5 1 7 ，1 8 ， 关于d - 先结构的相似性研究 1 9 。其中，最著名的也是公认最困难的问题是如何建立单射占先结构类的表示 定理。谚问题自从1 9 9 3 年法国学者m f r e u n d 提出以来 8 ，多位研究人员刈其 进干r 了硼究，但只解决了它的一些特例c 儿，15 ，1 8 ，0 3 年文献 1 9 词：明所有 已出现在相关文献中的逻辑规9 蛐都不足以刻画单射占先结构类。类似的问题在另 一种择优型非单调逻辑一信念变化理论研究中亦存在 4 。 其_ - l ，研究工具和方法甚少。目前，在表示定理的证明中最普遍采用的方法 是建构某种占先结构，对于不同的后承关系，建构的占先结构需要满足不同的性 质。建构合适的模型在表示定理的证明中是关键也是最困难的步骤，目前占先结 构的建私j 并无通用的方法，般而言只能是“因后承而异”。占先结构与模态逻 辑的k r ip k e 结构是类似的，而逻辑学家对k r i p k e 结构的研究则较深入。众所周 知，在模态逻辑的完备性证明中有些通用性的方法，例如，典范模型方法 ( c a n o n i c a lm o d e l ) ，证明有限模型性质有过滤方法( f i l t e r ) ，模型的转换技术 有生成予模型法、超积及直积等方法，判定模型逻辑等价则有互模拟 ( b is i m u l a e i o n ) 及受限互模拟( b o u n d e db i s i m u l a t i o n ) 等理论与方法 2 。而这 些对占先结构而吉除了极少的零散结果基本是空白一个自然的问题是，能否把 k r i p k e 结构的这些结果平移到占先结构中? 答案是否定的，因为从泛代数的角 度看，d i 先结构对应的代数与模态代数差异极大 3 3 ，不但如此，它和h e y t i n g 代数、c y l i n d r i c 代数差异也极大，这就说明一阶逻辑、直觉主义逻辑以及模念 逻辑的 型论性质对占先结构均不适用。 其：，研究视野只见树木不见森林。迄今为止，学术界对占先关系性质与l i ： j _ i ；l 惆后7 f 5 ：的逻辑性质之间对应性的研究局限在对一个个孤立的表示定理的研究， f l q 否i 人这些结录本身对我们了解择优型非华调推理是具有重銎意义的，征i 是我 1 f ：j 缺乏j 、卜一些更深层次的性质的把握，例如，j j 先关系性质与非单调后承的逻 j 性质艺川的刘廊性片不足普遍存在的，那么，这种对应性存在的充要性条件是什 么? 我们i 二经知道一些特殊的单射卣先结构予类i 叮以由l l o r n 型和非l i o l n 型逻辑 舰则加i 奠刻，橱迂献 9 i i f 明所f i - 已i l i 现在相关文献中的逻辑觇则鄙不足以刻 厕褴个r 仁划古先结构类，那么，一个自然的问题是：- f i r 以出h o r l i 型和非t l o i ，鹕 逻辑规则加以刻画的昂射r 耳先结构予类的特征如何? 对该问题， 1 9 获得了“i 田步结仑，似总体而苦，对于这些问题学术界目河尚缺少深入研究。 总 l 勺来说，黔弘调后承的研究技术性成果颇为丰富，但鲜驯的对比是，该领 域具有普遍性的方法和工具较少，缺少具有方法论指导意义的成果。所以，我们 认为非单凋后承的研究还处于初级阶段，些模型论的基础理论研究十分欠缺甚 至空白，对占先结构的研究还仅仅停留在把它作为择优型非单调逻辑的语义结构 用1 j 建立表示定理这。层面上，对占先结构本身的性质缺少深入研究，这一方而 南京航空航天大学硕士学位论文 导致在研究择优型非单调逻辑时缺少可用的技术与理论，另一方面，这也影响到 其它相关领域的研究，例如，最近有文献提出用公式集上的占先关系来刻画a g e n t 的“偏好”进而为a g e n t 的理性行为建模并致力于研究a g e n t 的内逻辑( j n t e r n a l 】o g ic ) 的修正( r e v is i o n ) 问题 2 6 3 ，这无疑对智能a g e n t 理沦模型珂f 究是有益旧 探索，然而目前他们的工作只能处理有限语言f 的最简单的情形一链式修l 卜 ( t h a i nr e v i s i o n ) ，其中的原因在于，它们提出的关键概念一逻辑链( 1 0 9 i c c h a i n ) 实际上等价于l e h m a n n 等人提出的分层( r a n k e d ) 占先结构，学术界对这种 t 吁先结构的性质已有较透彻的研究 1 1 ，而列于一一般偏序f 的f 与先结构，我们甚 至连两个占先结构等价的非平凡充要性条件都不清楚。所以，对占先结构基本性 质展开深入研究不但对择优型非单调逻辑的研究具有重要意义，而且也：卣助于人 工智能其它相关领域的研究。 本文旨在研究占先结构的相似性与等价性之间的关系。互模拟 ( b i s i m u l a t i o n ) 是现代模态逻辑与并发语义 2 ，1 3 ，1 4 巾的核心概念。以色列 学者a b o c h m a n 最近在e s 结构中引入了一种互模拟概念一相似性 5 ，并以此为 工具研究了非荦调逻辑与信念变化的若干问题，正如b o c h m a n 指出的，相似性 很大程度上决定了e s 结构的推理行为 5 ，但遗憾的是，b o c h m a n 本人并没有对 相似性概念进行深入系统的研究。本文将对该概念开展研究。主要讨论占先结构 相似性与等价性之间的关系，在此基础上讨论条件断言布尔组合的语言表达能 力。 全文安排如下：第二章回顾阶模型论相关概念和结果，第三章引入占先逻 辑的一阶转换并讨论其基本性质，第四章讨沦b - 丰目似性，第五章讨论m 相似性 与等价性之问的关系及条件断言布尔组合的语言表达能力，最后是全文总结。 关于i i 先结构的千h 似性研究 第二_ 章预备知识 本文将用刮有关命题逻辑语言，一阶语言及其模型论的一些相关知t i ，弱外， 有关超滤的一些基本知识电将涉及。因此。我们将一些相关的定义以及相关的重 要结果在此做简单陈述。详细介绍参考 1 0 】 7 】 3 3 】。 2 1 占先模型 首先，我们介绍有关命题逻辑语言的相关定义以及其语义解释，在此基础_ j ： 给出本文将着重讨论的占先模型的相关概念。 一个命题逻辑的形式语占，为一集合，由命题变元符号构成。为了定义，中 的( 命题逻辑) 合式公式，我们引入下列逻辑符号： ( 1 ) 括号( ，) ； ( 2 ) 连接词 ( 与) ，、( 非) 。 山f 逻辎符号是每个语吉，中都有的符号，因而我们约定，逻辑符号不记入 ，中。为方便起见，我们将命题语言的全部命题变元组成的集合也记为， ，= 只，b ) 。山命题变元符号和逻辑符号组成符号串，满足一定条件的有限符 号串可以称为命题逻辑的公式，我们有以下定义； 定义2 1 1 。，t 扣的公式归纳定义如下： ( 1 ) 单个命题变元是公式； ( 2 ) 若妒和吵是公式，则( 妒 y ) 和( ，妒) 是公式。 下文中我们将合式公式集记为f o r m ( 1 ) 。 以上归纳定义中的公式疑满足以j ：条件的最小集合，也就是说不足【b 以f ：条 件! l 二成的字符串都不是公式。以下的归纳定义类同，不再特别指出。 由于f 、，一 已经构成了命题逻辑联结词的完全集，因此存以i 二逻辑符号中 没有包含斗，h ，v 等逻辑符号。如果一个公式中出现了o ，h ，v 样逻辑符号，可以 看作上述公式的简记，即 伊 l ；f ，= 肼 ( 妒 1 矿) 南京航空航天大学硕士学位论文 妒h y = 村( 矿。妒) a ( y o 妒) 妒v 矿= 耐1 ( 伊a 1 i f ，) 一个命题逻辑语言的模型a 是若干命题变元组成的一个集合，即 a ，= e ，尸2 ) 。命题逻辑语言，的任意公式在某个模型下都有一个赋值：“真” 或者“假”，一般称之为语义，我们有以下的严格定义。 定义2 1 2 公式a 如果在某个模型爿中取值为真，记为爿卜a 。设4 是命题逻 辑语言f 的一个模型，f 中的公式在模型一中的取值归纳定义如下： ( 1 ) a 是某个命题变元p ，4 卜岱当且仪当只a ； ( 2 ) 口是一声，a 卜岱尚且仪当a | ，即在ar p 驭值不为真； ( 3 ) 甜是伊i 仍，彳卜口当且仅当爿卜缈i 并且名卜纯。 设1 ，是模型a 对应的赋值，若有a 卜口i 乜- i f f 以u 作v 卜( ) j ，显然赋值函数v 叮 以看作，u 仃，f j 斗 0 ，l 的一个映射，( 其中，分别为命题逻辑语言，j 1 的永 粪和永假公式) ，显然v ( t ) = i ，v ( ，1 ) = 0 。以y t l ( i ) 标记所有赋值函数的集合。 划于语言f 的赋值v ，记集合 口e b b r m ( o ：v 卜口 为t 1 1 ( v ) 。 有了上面的准备知识，我们将在此基础上给出占先模型的定义及其语义。为 了后面介绍的方便起见，先对定义中出现的所谓的光滑性作简单介绍。 设s 为一集合，- 为s 上的，2 格偏序( 满足传递性和反自反性) ，对任意 矿s ，矿满足所谓的光滑性是指满足下列条件：任意，ev ，f 或者本身是v 的 极小点或者存在s 矿，5 一 f 并且s 是矿的极小点。所谓f 是y 的极小点是指不存 在，矿，使得r r 。 定义2 1 3 一个命题逻辑语言，的占先模型是一个三元组 s ， ，其中， ( 1 )s 是一个非空集合，其元素称为状态。 ( 2 ) ，是一个函数：s 寸v a l ( o ，给缚个状态指派一个赋值。 ( 3 ) 是s 上的一个严格偏序，并且满足下列所谓的光滑条件：对任意a 而朋，( 黟，集合蚓f ，= s ：ses ，( s ) i - 口) 是光滑的。( 在不引起歧义的情况 下，简记忙b 为i l a l l ) 。 差王直盛绝塑煎塑! 堕堡婴塞 j 面介绍个命题逻辑语言f 的占先模型的语义后承的概念，为了区别于命 题逻辑语言的语意后承( 用符号卜表示) ，本文使用i 作为非单调语意后承的符 号，并且将口i 称为条件断青h - 。 定义2 1 4 设矽是语言z 上的一个占先模型，由形生成的占先关系记为- w 并 且定义如下：l 。是一个f o r m ( o 上的二元关系，对于任意公式“和f o r m ( o ， a i 。当且仅当对恻i 中的任意极小元s ，( s ) 卜。我们以标记c w ( 口) 记集 合 声：a f 。声 。 对于同一个语言? 上的任意两个占先模型彤和，如果i 。i _ 卜w 2 我们称 它们是等价的，记为w 。一w 2 。 2 2 一阶逻辑的形式语言及其模型 下而我们介绍有关一阶逻辑的形式语言相笑定义以及其语义解释，并且埘后 而将要用的的一阶语言的模型沦的相关概念和性质也做简单介绍，其详细的概念 和命题证明在馍型论的相关教材中都可以找到，例如文献【7 】等。 一个一阶逻辑的形式语苦l ( 以下在本节中简称为形式语言) 为一。集禽， 由关系符号，函数钳：号以及常量符号构成。每。一个关系符号p 有一个确定的兀数 n 1 ，称p 为门元关系符弓。每一个函数符号f 有一个确定的元数m 1 ，称f 只j m 冗晒数符号。 ，为一形式语茜。为了定义 中的( 一阶) 合式公式，我们引入1 - 列逻辑符 号： 括号( ，) ： ( 个体) 变量i ，o ，v l ，v 。，( 以为自然数) ； 连接词a ( 与) ，( 非) ； 量词v ( 任意) ； 2 元关系符号；( 等号) 。 b 于逻辑符号是每个语言中都有的符号，因而我们约定，逻辑符号不记入 l 中。我们称中的关系符号，函数符号和常量符号为非逻辑符号，出以上约定 我们知道语言只包含非逻辑符号。 定义2 2 1 中的项归纳定义如下： 南京航空航天大学硕 学位论文 ( 1 ) 变量是项。 ( 2 ) 常量符号是项。 ( 3 ) 若f 1 ，f 。是项，而f 是一个m 元函数符号，则f ( t l t 。) 是项。 定义2 2 2 中的原子公式归纳定义如下： ( 1 ) 若，t ：是项，则f 。；r ：是原子公式。 ( 2 ) 若f 1 ，t 。是项，而p 是一个玎元关系符号，则p ( f 。t 。) 是原子 定义2 2 3 中的公式归纳定义如下： ( 1 ) 原子公式是公式。 ( 2 ) 若妒和妒是公式，则( p a ) 和( ，妒) 是公式。 ( 3 ) 若妒是公式，而x 是变量，则( v x ) 9 是公式。 由于 a ，、，v ) 已经构成了一阶逻辑联结同的完全集，因此在以上逻辑符 号中没有包含寸，付，v ，j 等逻辑符号。如果个公式中出现了斗，付，v ，j 等逻辑符 号，可以看作上述公式的简记。其中，3 x 1 9 0 = 。，( v x ) _ 1 p ；其他有关叶，+ ，v 等 逻辑符号的说明参见2 1 节中有关命题逻辑部分的相差内容，此处不再赘述。 如果一个项f 中出现的自由变量都属于集合 ，j 。 ( 但是x 。，x 。 未必都在f 中出现) ，则，也可以记作f ( ，x 。) 。如果一个公式妒中出现的 自i b 变量都属于集合 ，x 。) ( 但是x 。，x 。未必都在妒中出现) ，则妒 也可以记作妒( ，x 。) 。特殊地，不包含自出变量的公式称为甸子。 设a 为一个非空集合。如果对于三中每一个, 元关系符号j d 都有彳上一个指 定的 元关系r 来解释它；对于三中每一个m 元函数符号f 都有a 上一个指定的 月f 元函数g 来解释它；对于三巾每一个常量符号c 都有a 上一个指定的元素口来 解释它；这样就构成了a 中对于的一个解释 ( 可以看作足由上中符号到a 上的一些关系，函数以及一中的一些元素的映射，毒称为指派函数) 。这样我们 有如下定义：， 定义2 2 4 一个语言的模型是一个二二元组 ，其中彳是一个非空集合 称为的论域，善是如上所述的指派函数。般的亭( d 和善( c ) 记作p 一和c 一。 定义2 2 。5 f 0 一个语言l 的两个模型一= 和从= ，如果a ，9 4 并且适合下列条件，则称m 2 是：，= 中的解释为g ，则 ，【a o d 。】2 g ( f l 【a o “。】，。【“o 订。】) 。 定义2 2 8 设2 ( 一，舌 是一个语言l 的模型，妒( x 。，x 。) 是l 的公式， p 中m t l i 。”v 。“h j 自由变量都属于集合( ，r 。 ，对于爿中的任”+ 1 元组吼， a ，f 而我们将归纳定义，口。在模型，r 中是否“满足公式妒 ( j 。，x ，) ”( 赶作，fp 。伊f d 。】) 这一概念如下： 南京航空航天人学顾：卜学位论文 ( 1 ) 若妒为f l ( 善。) ；，2 ( x 。) ，则五卜伊 。 _ - 与j 1 i x 5 t l 口o a 。 = ， a o a 。 。 ( 2 ) 嵩伊为p ( ( x o x 。) ，。( x o x 。) ) ，p 在2 1 1 的解 释为月，则卜妒 。口。】当且仅当r ( f f 口。d 。 f ，【日。口。】) 为真n ( 3 ) 若譬 为妒l ( x o ，工。) a 孽如( x o ，x 。) ，贝4 卜妒l 口o 口。 当且仪当t 卜妒l 【a o 口。】并且f - t p 2 l a o a 。j ( 4 ) 若妒为- 1 口( ，工。) ，则t 卜_ 伊【a 。a 。】当且仅当 _ 口 a 。 a 。】不成立。 ( 5 ) ) ：普妒为( v x ，) 0 ( x 。x 。) ，( f s 胛) ，则 - 伊【盯。a 。】当且汉 当列任一。a 爿都有卜妒 o e l i _ i a a ，+ l 日。】。 特殊地，当妒为l 的句子时，( 即妒为不包含自由变量的公式) ，若存在a 中的元素序列，a ，能使得卜- 伊 a 。q 1 成立，则称满足妒，记作 卜_ p 。 定义2 2 9 对于一阶语言的两个模型朋= j 1 1 i t ：= c 彳：，岛 ，u l 称为t 2 的初等予模型( 记为2 _ ：) 是指满足f 列条件： ( 1 ) “是：的子模型。 ( 2 ) 对的任意公式妒( x 。x 。) ，对爿i 中每一n 屈组口l ，f t 。，我 们有。 i 妒【a o a 0 当f ；l 仅警, i t 2 卜矿 “o 。】。 定义2 2 1 0 f 日一个语言三的两个模型i = 和，2 = ，如果对于甬 r = 。i 中每一语句( 不含有自出变量的公式) 盯都有触卜盯当且仪当，f ： - 叮，则 称， = 和2 = 是初等等价的，记作“一。 设为上中的一个句子集合，盯为l 中的一个句子。如果对于的每一模 型都有卜_ 盯，则称盯为的一个语义后承，记作卜盯。所有在模型中成 立的句子的集合称为该模型的理论，记为t h ( t 0 。显然若两个模型的理论相刷， 那么这两个模型是初等等价的。 2 3 超滤以及超积基本命题 下面我们来回忆有关超滤的一一些相关重要概念和结论。 关于占先结构的相似性研究 定义2 3 1 ，是一个非窑的集合，p ( h 是，的幂集，上的一个超滤口是尸( d 的一个子集并且满足下列条件： ( 1 )i d 。 ( 2 ) 如果x ，】7 d ，那么n y d 。 ( 3 ) 如果x d ，并且x y j ，那么y d 。 ( 4 ) j d 当且仅当，一z 譬d 。 设，是个非空的集合，对任意j ，a ，是一个非空集合，d 是j 上的一个 趣滤。，我们? 垮爿。( i ，) 豹卡氏积配做兀4 ；，即 1 1 爿。= 删 卅厂：- , u a ，并且v f ，( - 厂( f ) a j l 对任意两个函数，1 ，g 1 1 爿，厂和g 被称为d 等价( 记为，= 。g ) 当且仅当 ，：l ，( f j = g ( m d 。显见二元关系= d 是一一个兀a i 上的等价关系c i e ， 超襁兀爿，是个关二j ：= 。的等价类的集合，即， 几a 。= 局f 兀a ，) ，其中厶 g 丌爿。：= ng ) 。 本文的工作所涉及的一阶语言将不含函数符号，为简洁性起见，下面超积模 ? 型介绍将不涉及函数符号，更完全的定义参见 7 ，3 4 。 ；色义2 3 2 设，是一一个非空集合，d 是，上的一一个超滤，对任意，有“是一阶 语言三的一个模型。则其超积1 - i ，# 。也是一阶语言的一个模型。其中： ( 1 ) v i 。的论域是1 - i a ，对任意f ，其巾爿。是相应模型，t 的论域。 ( 2 ) 设p 是中一个门元关系符号，p 存n 肛中的解释是关系_ p 毋，对任意 咒， 誓兀彳 户玎，( 以 ：) 当且仅当( f ，：尸。7 ( ，( f ) ”( ) ) 】j ! _ ) 。 南京航空航天大学硕十学1 1 i ) = 论文 ( 3 ) 对语言l 中的任意常量符号c ，c 的解释是厶兀a ，其中，对们。意f ， n f f ，( f ) = c 。7 。 如果所有 掣“都是相同的，即“2 ，( i ，) 超积也可以写作1 1 ，r ，称 ， d 作以d 为模的超幂。关于超积兀“与原来的模型，l ，问：有如下基本命题成立： 命翘2 3 1 ，是一个非空集合，d 是，上的一个超滤，对f 醯支i i ，f ，魁一。阶 讲吉l 的一个模型。那么 ( 1 ) 设以，片1 1 4 ，对语言的任意公式口( j x ，) ， d n ，卜口 ：彤 当且仅当 i i ：，卜口f ，。1 ( ，) l ，”( f 1 ) ) d d ( 2 ) 对于语青l 上句子tn 卜卢当且仅当 ie l ：2 ，卜 d 。 ，) 证明见f 7 】中的定理4 1 9 。 关于占先结构的相似性研究 笫三章一阶转换 模态逻悔的基j 峰理沦中f i - 一种重要方法称为标准转换，它是建赢现代梭怠 站! 辑核心理沦( 对应性理论) 的主要工具【2 1 。所谓标准转化就魁将模态逻辑的 订浩转化为一阶语苦，这样就可以将一阶逻辑丰富的模型论性质厦硎到模念语南 i t 。本文将借用这一一技术，对占先逻辑引入相似的转换。 茸先我们介绍相应的语占。z 是经典命题逻辑语言，是带等号的一阶语言 并且对f 中的原于命题符号，p 包含相应的一元关系符号b ，鼻，除此以 外三还有一个二元关系符号肌下面我们给出一阶转换的具体定义： 定义3 1 。若工是阶变元，转换函数7 t ( 。) 将，中的命题逻辑公式按如下方式转 化为中的一阶逻辑公式： ( 1 ) t t ；( ，) ) = a ，- p ( x ) ，其中p ， ( 2 ) 玑( 一) = 。，一玑( ) ， ( 3 ) t r x ( d ) = “2 k ( 口) a 玩( 尸) ， ( 4 ) t r ( 口v ) = “巩( d ) v 玑( ) ， ( 5 ) 玑( 口 卢) = c l e f 玑( 口) _ 玑( ) ， ( 6 ) t r ( 丁) = x = x ， ( 7 ) 玑( ，) = 。一“= x ) 、发m 为命题语言7 的1 1 i 先模型，由于在m 中提供了相应于，的一阶语言l 的所有符号的解释，这样自然有如f 定义： 定义3 2 给定语苦f 上的占先模型m = ，f ， ，相应的一阶语言l 的模型，l 。， ：二 p ，定义直下： ( 1 ) r “m2 ( 2 ) 对任意p f ，啊= 恻i 吖= n s ：，( 5 ) p 。 命题3 i 给定语言f 上的占先模型m = 心，_ ，对任意公式。z 和s s ，下列 性质成立： ( 1 ) f ( s ) 卜a 当且仅当，f 。卜，t ( 甜) i s 】。 ( 2 ) l | 盘i l = ：i l 卢0 当且仅当。卜vx ( 玑( a ) 玑( 户) ) ( 3 ) x m 胁( i f 口6 ) 当月仅当盯卜r a i n ( d ， s ，其c 扣 m i n ( 口，x ) = 以，t r x ( 口) vz ( t r ( d ) 一r ( z ，工) ) 。 证明( 1 ) 对公代甜的结构复杂性进行归纳证明如下： 南京航空航天人学硕士学位论文 1 1 若5 为原子公式p 。 由定义3 t 可知玑( p )