（基础数学专业论文）disjunctive命题的模型理论.pdf

摘要 论域理论( d o m a i nt h e o r y ) 是格上拓扑学藏畴的一个重要研究领域，其研究基本 器蔚楚在为纛序设计谣言提供语义撰黧。适甩芎：计算机辩学技术的发展，入翻缭了需 要论域的构遗算子外，还需要论域的逻辑表示，以便更好地服务予高阶炎毅的推理。 近来，旅坟静教授基于p i t t s 的h o r n 命题理论、j o h n s t o n e 静d i s j u n c t i v e 理论以及 g e n t e n 的s e q u e n t 演算引入了d 两u n c t i v e 命题理论，稳定论域的逻辑表示，表明一 类稳定论蠛瓣捧于垂穗容d i s j u n c t i v e 命题理论辩模登缀_ i 麓的稼穿煞 本文的羔作主要研究d i s j u n c t i v e 命题的模掇，首先从理论模糖角度研究d i s j u n c - t i r e 会透理论，吾l 入f 一接象模型、势建立穗关游疆论t ( l ) 与p ( 彩褥翮了一个稳 定的d d - 半格的逻辑袭示；其次我们从模型的角度得到了全抽象模型以及自由模型等 摄念，讨论魏镌的挂璇耧关系，我翡得到了震撰罄秘鑫然模登是抽象秘舀巍魏。我步卜 对于不同的对象和对象问的映射，我们w 以建立相应的藏畴，因此为了考虑理论问的 莛赡我弱弓 入了等子瓣概念势建立了藩令理论瓣懿获瓣耩释，菝簿释静是囊，毒黧两 个重簧结论，即含有等子的理论丁与她的诱导理论是同构的以及禽有等子的理论冀理 论翰懿勰释橡成翦蓬游每玉事疑莛跨警徐。 装键词： 论域。s c o t t 论域，稳定论域，藏畴，d i s j u n c t i v e 命题理论，自由模 型，攘象模鹫，d d - 举撂，壤繇 a b s t r a c t d o m a i nt h e o r yi sa nv e r yi m p o r t a n tr e s e a r c ha s p e c to fl a t t i c et o p o l o g y , t h eb a s i c a i mo fi t sr e a s e a r c hi st op r o v i d es e m a n t i c sm o d e lf o rp r o g r a m m el a n g u a g e t s ot h a ti t c a l lp r o p e rf o rt h ed e v e l o p m e n to fc o m p u t e rs c i e n c et e c h n o l o g y e x c e p tf o rd o m a i n s c m c u j n s ，o n ea l s on e e dt h el o g i cr e p r e s e n to ft h ed o m a i n t h a ti tc a l ls e r v e rf o rt h e h i g h t e rt y p ed e d u c t i o nm o r eb e t t e r i nt h e s ed a y s ，p r o fc h e nb a s eo nt h ew o r ko f p i t t s h o r np r o p e s i t i o n a lt h e r o y , j o h n s t o n e sd i s j u n c t i v et h e r o ya n dg e n t e n ss e q u e n t c a l c u l u s ，d i s j u n c t i v ep r o p o s i t i o ni si n t r o d u c e d ，h eg i v e st h el o g i cr e p r e s e n to ft h es t a r b l ed o m a i na n ds h o w sl d o m a i ni si s o m o r p h i ct ot h es e tc o n s i s t i n go fm o d e l so fa d i s j u n c t i v ep r o p o s i t i o nt h e r o y i n t h i sp a p e r ，w ew i l lf u r t h e rd i s c u s st h ed i s j u n c t i v ep r o p o s i t i o nt h e o r y , f i r s t l y w ed i s c u s st h ed i s j u n c t i v ep r o p o s i t i o nt h e o r yi nt h ee s p e c to fm o d e lt h e o r y , i n t r o d u c e f - a b s t r a c tm o d e la n ds e tu pt h er e l a t e dt h e o r yt ( l ) a n dp ( l ) ，s 0w eg e tt h el o g i c r e p r e s e n to ft h ed d s e m i l a t t i c e s e c o n d l yw ee s t a b l i s ht h ef u l la b s t r a c tm o d e l ，f l e em o d e l a n dd i s c u s st h e q u a l i t ya n dr e l a t i o n s h i pb e t w e e nt h e m w eg e tb o t ht h eg e n e r a lm o d e l a n dn a t r u a lm o d e la r ea b s t r a c ta n df r e e e x c e p tt h a t ，w i t hr e g a r dt ot h ed i f f e r e n to b j e e t a n di n t e r p r e t a t i o n ，w ec 2 nb u i l du pt h ec a t e g o r y s oi no r d e rt oc o n s i d e rt h ec a t e g o r y b e t w e e nt h et h e o r yw ed i s c u s st h en o t a t i o no fe q u a l i t ya n d i n t e r p r e t a t i o n i nt h ee n d ， w eg e tt w oi m p o r t a n tc o n c l u s i o n o n ei se v e r yd i s j u n c t i v et h e o r ytt oh a v ee q u a l i t y i si s o m o r p h i cw i t ht h ei n d u c e dt h e o r y a n o t h e ri st h ec a t e g o r ye t h ro fd i j u n c t i v e t h e o r i e st oh a v ee q u a l i t ya n di n t e r p r e t a t i o n si se q u i v a l e n tt ot h ec a t e g o r yd d s l k e y w o r d s ：d o m a i nt h e o r y , d i s j u n c t i v ep r o p o s i t i o n tf r e ea n da b s t r a c tm o d e l ， d d - s e m i l a t t i c e 论文独创性声明 本论文是我个人在导师指导下进行的研究工作及取得的研究成果。论文中除 了特别加阻标注和致谢的地方外，不包含其他人或机构已经发表或撰写过的研究 成果。其他同志对本研究的启发和所做的贡献均已在论文中做了明确的声明并表 示了谢意。 作者签名：i # - 日期：a 川、奠叶 论文使用授权声明 本人完全了解上海师范大学有关保留、使用学位论文的规定，即：学校有权 保留送交论文的复印件，允许论文被查阅和借阅：学校可以公布论文的全部或部 分内容，可以采用影印、缩印或其它手段保存论文。保密的论文在解密后遵守此 规定。 作者签名：雨也 导师签名：日期：a胡、f 咋 f 垡! 塑堕堡全墨堕堡型垄堡 ! 第一章引言 论域理论( d o m a i nt h e o r y ) 是格上拓扑学范畴的一个重要研究领域，其研究基本 目的是在为程序设计语言提供形式化语义从语义模型来看，由于形式化中侧重面和 使用的数学工具不同，形式语义学可分为四大类；操作语义学、指称语义学，代数语 义学公理语义学指称语义学是公认的标准形式语义学，论域理论是其基础和核心， 它是由d s c o t t 开创的，后经m s m y t h ，g d p l o t k i n 等人工作，论域理论已取得了丰 富成果，为指称语义学奠定了坚实的基础 在论域理论中，语言语法域的指称( d e n o t a t i o n ) 称为论域，一般是指具有一定特 性的定向完备偏序集，其上的s c o t t 连续映射( 即单调保定向并的映射) 作为计算( 程 序) 的指称论域与s c o t t 连续映射组成的范畴( 称为论域范畴) 是计算机语言的指称 语义域，它是论域理论主要研究对象为了更好支持程序设计语言，人们要求这样的 语义域是笛卡几闭范畴然而论域范畴本身不是笛卡几闭范畴，人们就退一步寻找它 的笛卡儿闭子范畴? a j u n g 于1 9 9 0 年表明论域范畴恰好有两个满的极大笛卡儿闭予 范畴一双有限论域范畴和k 论域范畴，这个结果使人们特别关注这两类论域 拓扑学的基本概念在计算机科学中特别在程序设计语言的指称语义中有极好的应 用人们可以把拓扑空问认为数据类型，空间中的点认为计算过程( 程序) 。开集认为 规范( 性质) ，z o 认为程序f 具有规范d ，谓词认为空间x 到布尔代数 0 ，1 ) 保 结构的算子若在 0 ，1 ) 上引入适当的拓扑结构，则它是某种连续型映射，并且s x 是开集当且仅当有连续映射( 谓词) p ：x 一 o ，1 使得s = 矿1 ( 1 ) 因此我们可以认为 谓词与开集是等同的这种观点在理解程序设计语言指称语义和程序逻辑的关系时特 别有用 在论域理论中。首先使用的论域是代数格，然而它太强7 。因为从自然数集到自然 数集的部分函数全体在点式序下不再是代数格( 无最大元) 在1 9 8 2 年s c o t t 引入了 一类论域称为s c o t t 论域，但是s c o t t 论域的幂域未必总是s c o t t 论域，为此p l o t k i n 引入了s f p ( s e q u e n c eo ff i n i t ep r o j e c t i o n s ) 论域【2 7 l ，它是非常好的一类论域，如它 在几乎所有的论域运算下都是保持不变的p l o t k i n 同时猜测s f p 论域范畴是廿论 域范畴的极大笛卡尔闭满子范畴 s m y t h 在1 9 8 3 年证实了p l o t k i n 的猜测【6 】s m y t h 的证实激发了j u n g 去寻找 论域范畴的所有极大笛卡尔闭满子范畴，结果他在1 9 9 0 年表明论域范畴恰有两个极 2 2 0 0 7 上海师范大学硕士学位论文 大笛卡尔闭满子范畴一双有限论域范畴与。论域，其中p 双有限论域就是s f p 论 域【2 4 ，2 8 】陈仪香教授在文献【l 】1 中重点关注j u n g 的l 论域，需要说明的是，o 论域是在连续性论域理论中使用的名称，而在稳定性论域理论中，l 论域称为稳定 i 论域 在计算机科学中，除了需要论域的构造算子外，还需要论域的逻辑表示，以便更好地 服务于高阶类型的推理a b r a m s k y 在文献【9 】中讨论了s f p 论域的逻辑表示，a m a d i o 和c u n e n 在文献【1 0 】中从逻辑角度研究了s c o t t 论域以及双有限论域j u n g ，k e g l m a n 以及m o s h i e r 在文献【5 1 5 中研究了多语s e q u e n t 演算与c o h e r e n t 空间的关系，p i t t e r s 在文献【1 1 】中讨论了命题理论与s c o t t 论域的关系，他表明每个s c o t t 论域都是相容 命题h o r n 理论的模型偏序集z h a n g 在文献1 1 2 j 中为了研究d i 论域在稳定映射下 的推理引入了d 溺u n c t i v e 逻辑 陈仪香教授在文献【1 】中引入了d i s j u n c t i v e 命题理论，简称d 命题，其目的在于 建立稳定论域即j u n g 的代数l - d o m a i n s 以及s c o t t 代数论域的逻辑表示最近他同 j u n g 教授一道对d i s j u n c t i v e 命题理论进行了深入的研究，使其理论更加深刻和完美 【2 1 文( 1 , 2 l 是从逻辑推理角度来研究d i s j u n c t i v e 命题理论，本文将从理论模型角度 研究d i s j u n c t i v e 命题理论，引入f 一抽象模型全抽象模型以及自由模型等概念， i - t i 仑他们的1 生质和关系，并建立两个理论间的映射解释，并得到一系列相关重要结 论 t 这篇论文由以下部分所组成，由于全文是在d 命题理论的基础上展开讨论的，首 先在第二章的内容里我们先介绍d - 命题理论，指称，模型，论域，s c o t t 开集等一系 列基本概念陈教授已经从逻辑角度建立了d 命题间的等价类。在第三章里，我们将 从指称相等的角度来建立等价类，建立了新的概念f 抽象模型，并在此基础上得到了 根据指称相等的等价类也是一个d - 半格在第四章里，我们将先介绍两个重要理论 t ( l ) 与t + ( l ) ，及建立其上的相关理论，得到d - 半格的逻辑表示，并从模型的角度 建立了抽象模型和自由模型，得到了自然模型和属模型都是抽象和自由的同时当l 是论域d 的所有开集所组成的集合组成的集合s n ( d ) 时，我们得到理论t ( s n ( d ) ) 与r ( s ( d ) ) 是相同的在第五章里，引入了d 命题间的等子的概念，表明含有等 子的理论丁与它的诱导理论是同构的；同时。含有等子的理论与理论问的解释可以构 成个范畴，此范畴等价与d 半格范畴 里地璺! 堑翌金星堕垡型垄焦 3 第二章预备知识 基于本篇论文在d i s j u n c t i v e 命题上进行讨论，在这章节内我们将详细地介绍和 d i s j u n c t i v e 命题有关的基本概念，为后面几个章节内容的展开打下基础 2 1 论域 陈仪香教授在文献【1 1 1 中给出了稳定论域的逻辑表示，我们来回忆下论域的有关 概念，在这节里我们从偏序集关系的基本概念a - t - ，介绍经典论域的基本内容 定义2 1 i 4 1 设x 是一集合若x 上的三元关系满足： 自反性t 比x ，茁s 蜀 传递性t ：p ，z x ，若z y ，sz 则z 曼： 则称二元关系s 为拟序关系进一步地，若s 还满足 反对称性，比，x ，若z f ，f z ，则。= 则称为偏序关系，简称序关系或偏序，而，) 称为偏序集一 n x 称为最小元( 最大元) 。若v t x ，都有口sz ( z 口) 一。 带有最小元的偏序集称为| p 偏序集 定义2 1 2 1 4 设p 是一偏序集，p 的子集a 称为上集，若z a 且z y 则有 y 月： 命题2 1 3 设p 是偏序集，a 是其子集，则 集合ta = piz ，孔a ) 是包含a 的最小上集，而符号tz 直接表 示t z ) ； 集合la = 3 ，pi ，z ，j z ，4 是包含月的最小下集，而符号lz 直接表 示l | = 定义2 1 4 1 1 】设a 是偏序集p 的子集，z p ， 若a lz ，即v a a ，o s z ，则z 称为a 的上界；对偶地， 若a t z 。即v a a ，z n ，则z 称为月的下界 符号t b 【a ) ，l b ( a ) 将分别表示一的所有上界之集与下界之集 定义2 1 5 ( 1 】设a 是x 的子集， 若r i b ( a ) 有最小元z ，则称z 是a 的最小上界或并。以后用v a 表示a 的并； 若f 6 ( 一l 有最大元z 。则称，是一的最大下界或交，以后用 月表示一的交 4 2 0 0 7 上海师范大学硕士学位论文 定义2 1 6 1 4 1 设p 是偏序集， p 的非空子集x 称为定向的，若x 的每一对元素在x 中有上界； p 的定向下集称为p 的理想，有最大元的理想称为主理想，其形如iz ； 尸的非空上有界子集称为相容集，以后用符号x t 表示x 是相容集，d tb 表 示 口，6 ) 同样的，当x 是一偏序集时，若x 的每个定向集都有最小上界( 即并) 则称偏序 集x 是定向完备偏序集( 简称d c p o ) ，定义2 1 7 f l l 定向完备的j p 偏序集称为完备偏序集 定义2 1 8 1 4 1 设d 是完备偏序集，a d 若a 满足条件t a 是一上集；且 设是_ d 的任一定向集，若v a a 则有z a 使得z 月； 则称a 是d 的s c o t t 开集 接下来我们介绍代数完备集的定义代数的完备集一般称为论域( d o m a i n s ) 首先在完备集上引入另一种序关系，称为双小于关系，或w a y - b e l o w 关系 定义2 1 9 n 设d 是完备集，则 1 d 上的双小于关系定义为；对于任意的z ，y d ，z y 当且仅当，对于d 的 任意定向集，只要g s v a ，就有6 a ，使得z s6 ； 2 d 的元素。称为有限元或紧元，若o y 用符号【( d ) 表示d 的所有有 限元之集符号j lz = ( d ) ：y z ) ； 3 d 称为代数的，若比d ， l z 是定向的。且0 一v q 4 代数的完备集称为论域， 下面我们来介绍下s c o t t 论域和稳定论域 定义2 1 1 0 1 1 i 满足下面公理的d c p o 称为相容完备d c p o ， 相容完备性：垤，9 ，若。ty 则z v y 存在 相容完备的论域称为s c o t t 论域 定义2 1 1 1 f 1 】设d 是完备偏序集，若v z d ，主理想iz 是完备格，则称d 是局部完备的 ， 局部完备的论域称为稳定论域( 即l 论域) 无论是s c o t t 论域还是稳定论域，他们除了代数性外，还有两种代数运算，一是 定向并，另一是交运算，这是它们不同的特征。s c o t t 论域有非空( 集) 交运算，而稳 定论域却有相容集的交定向并是论域理论的基本运算，而交运算是外加的基于这 堕! ! ! 垡翌金塑塑堡型垄堡立 种思想，我们引入两类论域，都是涉及交的有限情形然而论域本身不构成格，但格 在论域理论中有重要的应用下面来简单介绍格的一些概念 定义2 1 1 2 1 1 】设l 是偏序集， 若l 的每一有限子集都有交，则称l 为交半格； 若工的每一有限子集都有并，则称l 为并半格； 若l 的任意非空有限子集都有交与并，则称l 为格 2 2d i s j u n c t i v e 命题理论 m c o s t e 【3 1 1 引入l i r a - 理论的概念，这个理论要求它的公理仅是由逻辑算子t r u e ， ，j 构造的s e q u e n t ，并且进一步要求存在量词仅可施用于可证唯一的变量，即弘妒( z ) 是个“好的公式仅当s e q u e n t ( 咖( z ) a 砂( z ) 卜z = z 7 ) 是可从公理推出 j o h n s t o n e 在文献f 3 l 】中以类似的方式定义了d i s j u n c t i v e 理论：他的公理可使用 几何逻辑的所有算子( 包括无限析取) ，而存在量词服从于c o s t e 的限制，同时析取 是可证d i s j u n c t i v e ，即v 埘晚是个。好的”公式仅当对于任意不同的指标( i ，j ) 。 渤a 咖卜a l s e ) 是可证的。 在j o h n s t o n e 的d i s j u n c t i v e 理论，存在量词是被使用的，也就是j o h n s t o n e 的 d u n c t i v e 理论不是命题的陈仪香教授在【1 1 中引入仅包含命题的d i s j u n c t i v e 理论 定义2 1 1 1 l 设_ p 是一非空集合，其元索成为原子命题，相应地，p 称为原子命 题集p 上的d i s j u n c t i v e 命题，简称d 命题，归纳定义如下t 1 每个原子命题是山命题； 2 常量了与f 是d - 命题； 3 若曲与妒是d 一命题，则a 妒是小命题； 4 若 也k ，) 是一簇d 命题，且对于每一对不同的指标( i j ) 有，( 也，奶) 成 立，则v 也是d - 命题 谓词p ( 毋，妒) 表示毋 妒卜f 是可以通过公理和表1 的规则推出的符号c ( p ) 表 示p 上的所有d - 命题，如果西c ( p ) ，那么我们说是定义好的 定义2 1 2 1 1 】一个d i s j u n c t i v es e q u e n tr 卜币，简称d - s e q u e n t ，是指一对d - 命题 的有限集r 以及单个d i s j u n c t i v e 命题西f 卜的意义是指r 中的命题一起逻辑上 能推出命题妒所谓逻辑上推出是指在公理基础上，经下面的推理规则推出每个推 理规则都形如器曩 62 0 0 7 上海师范大学硕士学位论文 表l ：d i s j u n c t i v e 命题理论推理规则 定义2 1 3 1 1 l 一个s e q u e n t 集在规则下是封闭的是指，只要规则的前提在这个集 合中那么这个规则的结论就在这个集合中若s 是个仅由原子命题组成的s e q u e n t ( 称为原子s e q u e n t ) 集合，t ( s ) 表示包含s 的最小封闭s e q u e n t 集此时，我们称 s 为公理集，称t ( s ) ( 有时简写为t ) 为由s 生成的d i s j u n c t i v e 命题理论，简记为 d p t ，且称t ( s ) 中的s e q u e n t 为直觉定理，简称定理 陈仪香教授在文献1 1 】1 中为了给出稳定论域的s t o n e 表示定理，引入了一种特殊 半格。称为分离完备半格半格r 简称为n 半格，他以j o h r 埠t o n e 的d i s j u n c t i v e 理论 【3 9 】以及z h a n gg u o - q i a n g 的d i s j u n c t i v e 系统为背景陈教授用这类半格建立了代数 l d o m a i n s 的格表示以及s t o n e 对偶后来，这类半格用来建立d i s j u n c t i v e 命题理 论的模型【1 , 2 】这里简要地介绍这类半格 定义2 1 4 l l 】l 是有最大元1 和最小元0 的交半格，若 1 对v 的z ，l ，如果o y = 0 ，我们称z 和f 是分离的 ，2 对l 的任意子集b ，若b 中的任何两个不同的元素，y 是分离的，则b 叫 分离子集 3 如果对于l 的每一个分离子集都有并，那么二叫做d i s j u n c t i v e 半格，简称m 半格 定义2 1 5 i l 】d 半格l 称为分配的，若它满足下面的条件； ( d ) 对于l 中的每一个元素口以及分离子集b ，有oa ( i i b ) = ( 口a b ) 分配的 d - 半格，简称为d d - 半格 型竺! 堑堡佥墨堕送型! ! 笙 7 第三章f 一抽象模型 陈仪香教授在文吲中，从逻辑推理角度在d i s j u n c t i v e 命题间引入j 等价关系。 在这幸中我们将引入另一个f - 抽象模型，并从模型角度引入另一个等价关系首先 我们先来回忆下模型的基本概念和相关性质 3 1 模型 定义3 1 1 i 1 1 给定d d - 半格l 关于原子命题集p 在l 中的结构是指映射m ： p _ l p 上d i s j u n c t i v e 命题关于结构m 的指称是从c ( p ) 到l 的函数1 1 m ，且满足下 列条件： 1 p ( 妒，妒) 推出i 纠肘a l m = o ； 2 若毋p ，则i 纠m = m 0 ) ； 3 f 7 1 f = 1 ，l 的最大元； 4 1 f 1 m ，罩玑l 中的最小元； 5 a 纠 l l ，= l 纠1 i ，a 【纠，l 中的二元交； 6 i v 洲砌m ；_ r i 妒i m ，l 的分离并 原子命题集p 在d d - 半格l 中的结构m 满足p 上的s e q u e n tr 卜是指在l 中，有 眯r b l u i 纠肘成立 设7 是一个d 两u n c t i v e 命题理论，m 是t 的原子命题集在l 中的一个结构， 若肘满足丁的所有公理，则称结构m 为r 的模型 性质3 1 2 【1 j 假设对于所有的 j j ，那么妒a ( v 叫也) 卜v 列a 也) 定理3 1 3 【1 l 设村是d 两u n c t i v e 命题理论t 到d d 一半格l 的模型若币卜妒 是定理则m 满足妒卜妒，即有i 纠m 冬i 纠成立 设丁是原子命题集a 上的d i s j u n c t i v e 命题理论，在以上的所有d i s j u n c t i v e 命题 集中，定义关系s r 为 毋s ri f ，当且仅当卜妒是丁的直觉定理 由表1 中的规则立即得到，- - t 使得d i s j u n c t i v e 命题集合为个拟序集再定义 等价关系为 8 2 0 0 7 上海师范大学硕士学位论文 咖兰t 妒当且仅当毋卜妒以及妒卜妒是t 的直觉定理 对于等价类【纠以及m ，定义m 当且仅当t 妒由( c u t ) 规则得等价类问 的序关系是定义好的，且这商集a ( t ) 是一偏序集陈教授在文献f 1 】中已经证明 了a ( t ) 是一个d d 一半格在下一节中我们将引入另一个等价关系 3 2f - 抽象模型 我们已经从逻辑推理角度引入了笺t ，即垒t 妒当且仅当毋卜妒以及妒卜妒是 d i s j u n c t i v e 命题理论t 的直觉定理对于等价类以及【纠，定义【纠tm 当且仅 当1 - 妒是t 的定理这样所得到的商集a ( t ) = 1 阱：c ( p ) ) 是一d d 一半格 t 到a ( t ) 有个属模型，用符号g r 来表示，其定义为v c ( 尸) ，【纠曲= 【纠 现在从模型角度建立d 命题间的等价关系型m 设m 是d i s j u n c t i v e 命题理论t 到d d 一半格l 的模型，毋与妒是d - 命题，定 义毋皇m 妒当且仅当【e l m = l 妒l m 【e l m 是其相应的等价类令c ( t ) = 【纠m ：妒 c ( p ) ) 对于等价类m 以及【纠m ，定义【纠 f mi 妒k 当且仅当i ms l ， 则c ( t ) 是一个偏序集 一 定义3 2 1 设m 是d p tt 到d d - 半格l 的个模型，若【4 , 1 m = 0 则卜f 是定理，则称模型m 是只抽象的 注，若模型m 是b 抽象的，则咖型t f 当且仅当妒掣m f 定理3 2 2 设m 是d p t t 到d d 一半格l 的一个f 抽象模型。则c ( t ) 是一 个d _ 半格 证明，首先我们可以看到【叫a 【训= 渺a 训也就是说a 纠是眵】和m 的最 大下界因为 l 妒a 妒j = 【纠 ，a i 叫ms 1 4 , 1 m = 【毋a 妒js 阳q 即 a 妒l = l 毋l m a i 妒l 彳s 如l 吖= 叫f 纠 所以陋a 纠是和【训的一个下界 假设【f ，! s ，0 【训也就是说 f 明”l t f l ”，i o m 砂i m d i j u n c t i v e 命题的模型理论 即 e l m i 纠盯a i 妒l m 因此 i 刎s i a 妒j 所以，a 纠是【纠和的最大下界 且对v ，当i f i m = 0 i 纠村时，【用m ，即【用= 0 ；当i t i = 1 m m 时，口1 【纠所以【明= 1 其次，如果【矧a 【奶】= 0 ，那么f 训= l v 以】 因为1 a 【奶1 = o ，也就是说，a 蚓= 0 = 【用，且m 是抽象的 我们得到 a 奶l m = 【r i m 即 m a 如1 m = 0 净咖a 如卜f 所以v 圣t 是可以被定义的 且对，。 i 以1 村i 也l 村令l a j i v a l f 号慨】【v 咖1 则【v 机】是】的个上界 假设对所有的i ，m l msi 明m ，一也就是说【蚓【0 】，即u m 】m 柳_ l i ，= 【v 硐村i o m 我们得到【v 矧s 阶所以【v 矧是【以】的最小上界 所以【也】= 【v 咖】，因此d ( t ) 是一个d 半格 口 1 0 2 0 0 7 上海师范大学硕士学位论文 第四章全抽象模型与自由模型 如果m 是一个d p t t 到d d - 半格的模型。那么m 满足t 的所以定理：也就是 若妒卜妒是定理则m 满足妒卜妒，即有l 纠ms j 村成立，现在我, f r l - , 特考虑考虑相 反的情况，当两个命题的指称满足一定条件时。建立一个特殊的模型在这章里我们 介绍两个理论及两个特殊的模型- 抽象模型和自由模型，并讨论它们之问的关系 4 1 d p tt ( l ) 和p ( l ) 的构成及其相关性质 在这1 = 部分首先我们先来回忆稳定d d - 半格的含义，和n 半格完全余素元有关 的代数n 半格。然后给出稳定的d d - 半格的理论表示 定义4 1 1 1 1 j 假设l 是个d 半格， 1 l 中的一个元素a 被称为n 完全余素元，如果对于l 的任何分离子集x ， o h x 推得存在着z x ，使得d z c o p l 表示l 的所有完全余索无 2 如果对于l 中的每个元素a ，都存在的一个c o p l 的分离子集x 。使得 口= f i x ，那么我们称l 是一个代数的p 一半格 定义4 1 2 【1 i 稳定的半格是指最大元是n 完全余索元的代数n 半格 定理4 1 3 f l j 设t 是一个d i s j u n c t i v e 命题理论，l 是一个d d - 半格，那么在 d d s l ( a ( t ) ，l ) 与m o d ( t ，l ) 之闻存在着一个同构 这里d d s l 表示的是d d - 半格和n 半格同态所组成的范畴 接下来我们将证明稳定的d d - 半格可以被d i s j u n c t i v e 命胚理论所表示 现在给定一个稳定的d d - 半格l ，我们建立一系列的原子命题p = m i d c o v l ，并建立如下的自然公理，对任意的d l ，如，“，e c o p l ，如果e 0 ，那么 如果d la 如a a 厶e ，那么f d l l ，心1 f 厶1 卜旧是公理 此外 f d l l ，d 2 t f d n l 卜川是公理当且仅当d l a 如a a 厶= 0 那么我们得到了p 上的d i s j u n c t i v e 命题理论，用t ( l ) 表示 基于d p tt ( l ) ，我们定义如下的自然结构 ，工，肌( 同) = d ，v d c o p l 这是 t ( l ) 到l 的一个模型，简称自然模型由定理4 1 3 ，我们得到一个d - 半格同态， 墅! ! ! 堑里金星堕垡型堡垒 1 1 ，：a ( 丁( l ) ) + l 且 f ( g r ( l ) ) = 帆 那么，( f 纠) = l 纠帆，v i e 】a ( r ( l ) ) 另一方面，我们建立一个从l 到月( 丁( l ) ) 的映射9 ，使得g ( d ) = 【v 。xf x l 】 这里d = h ；x x ，x c o p l 这样的分离子集x 是唯一存在的。所以g 的可以 被定义的，且如果z c o p ( l ) ，9 ( z ) = f r z l 】 口 定理4 1 4 假设l 是一个稳定的d d - 半格，那么，o g = 缸，9 ，o ，i d 证明： ，o g = i d ，对任意的d l ，我们有 ，o g ( d ) = ，( v ：。xm 】) = i v ；xm j 帆 = i i 。x i m l l = z x x = d 9o ，墨i d 对任意的i 庐1 月( 丁( l ) ) ，那么存在的一个x c o p ( l ) ，使得m 盹= h x ，且 g o ，( 【叫) = 9 ( 【纠帆) = f v ；。x 旧l 接下去我们证明【v ；。x x l 】【纠，即v 。x 卜庐是t ( l ) 的定理 对于每个z x ：l 纠工= i i x ，我们有z m 帆，现在我们要证明通过对妒的 归纳演绎可以得到r z l 卜咖是t ( l ) 的直觉定理 基始； 情况1 妒是一个原子命题，那么存在一个d c o p l ，使得d l = 妒，然而 z s l 纠帆= l 胡l 肌= d 所以，m 是t ( l ) 的公理 情况2 咖= r 卜t 是一个规则，通过弱关系我们得到m 卜r ( = 纠是t ( l ) 的 直觉定理 2 0 0 7 上海师范大学硕士学位论文 情况3 = f ，从【川n o , = o ，z i 纠帆我们可以得到z = 0 ，所以f 0 1 - f ( = 钟 是t ( l ) 的公理 一归纳z 情况1 妒= 曲l a 如，那么 z l 纠l = z 【妒1 l 帆a l 如l 帆 = z s 【l l 帆，z i 如l 帆 = f 司卜l ，m 卜也是t ( l ) 的直觉定理 令m 卜毋1a 也是t ( l ) 的直觉定理( 由尺a 得) 情况2 妒= v 。x 咖，那么 z s l 妒i 】l = 争工 j i ，h l 辛存在，使得zsi q a , n ( 1 l l 为z c o p ( l ) ) = k 1 卜也是丁( l ) 的直觉定理 兮f z 卜v 州也是丁( l ) 的直觉定理( 由v 得) 号f z 卜咖是丁( l ) 的直觉定理 一 所以，我们证明了如果z i 妒 i n l 那么，司卜是t ( l ) 的直觉定理因此通 过规则，v 。e xf z l 卜毋是t ( l ) 的直觉定理 j 口 到目前为止，我们已经知道了l 在映射f 和g 下是a ( t ( l ) ) 的收缩核，并得到了 一些令人感兴趣的映射，例如映射f 满足，( f 纠) = m 帆，映射g 满足g ( d ) = ：。x 扛1 】，这里的d = h x ，两个指称帆和l - i ，他们在两个方向上使得下列图可换 t ( l ) i 也就是说，我们得到下列两个式子， - i = 9 0 1 1 帆 i l 心= f o l l l r ， 钗小l d i j u n c t i v e 命题的模型理论 1 3 因此 【】= ( g o ，) o 【】 卸 1 1 盹= ( ，o 夕) 【l 】 但是，我们已经知道，o g = i d ，因此我们非常希望go r = i d 也是正确的在 这种情况下，f 和g 是l 和a ( t ( l ) ) 之间的同构，那么我们可以得到稳定的d d - 半 格的逻辑表示也就是说， l 皇 ( 丁( l ) ) 然而我们不得不承认我们现在还不能这样做，我们首先要考虑下当go ，= i d 是正确 的时候下会发生什么情况，也就是说对任意的 ( 丁( 工) ) ，我们应该得到 g o ，( 【纠) = i 纠 我们取一对特殊的m 完全余素元x ，y 来考虑，那么通过假设我们得到 【k 1a 们l = g o ，( 【胡a f 们】) = 9 ( 【f 胡a 们】l ) = g ( 1 z l i - , a 【们l 帆) = g ( x ay ) = 【v 础m 】 这里的z c o p ( l ) ，且$ a f = u z 因此，如果这是正确的话，那么我们得到 m 圳= i v 触川 那么，v ，。z z 1 卜m a m 和i x l a y l 卜v ：。z z 1 都是t ( l ) 的定理我们已经 很容易的得到前者是一个定理了，但是通常来说后者我们不能从t ( l ) 的定理推出 的确，我们可以从下面的例子得到些启示我们用l 来表示稳定的d d 一半格，l 是由稳定论域d 的所有稳定开集所组成的，我们用下图来表示 事实上，o = t3 ，6 = t4 ，c = t1 ，d = t2 ，1 = d 0 = 0 c o p ( l ) = 口，b ，c ，d ，1 ，e 不是d - 完全余素元但是，e = c d = 口vb 现在我们看一下d p tt ( l ) 和格 a ( t ( l ) ) 1 4 2 0 0 7 上海师范大学硬士学位论文 在d p t t ( l ) 中。我们可以得到0 1vf 6 1 卜c l a 4 1 是定理，但是，f c l 问卜 mvf b l 不是公理也不是定理证明如下 1 3 l 上 l - d o m a i nd c a d b 0 s e m i l a t t i c el ( = s n ( d ) ) 我们构造一个d p t 理论t ( l ) ； 原子命题；口1 ，6 1 ，f c l ，f d l ，1 1 公理， 一f o 卜f c l ，f 胡卜- f 硼，口1 卜f 1 1 一f 6 1 卜f c l ，嗍卜问，6 1 _ 1 1 一c 1 卜f 1 1 ，问卜1 1 。 一f n t f 矾卜f f 1 1 ，胁1 卜胡：1 1 ，6 1 卜同等是已知的公理，然而它们也是定理，因为可以被 规则( l w k ) 和前面的公理所推出 我们可以通过下面的证明得到a 1vi b l 卜- i c l f d l d 一公理；d 1 卜c 1 ，嘲卜f c f n lv 6 1 卜c 1 通过v ) 一n 1v 6 1 卜问 一f 口1 v f 6 1 卜i c l 问是一个定理( r ) 接下来我们证明如果i da d 1 卜mvf h 是一个定理，那么我们将会得到矛盾 的确。 假设i c lar d l 卜mv 6 1 是个定理 通过( rv ) 在此之前我们应该得到： c la d l 卜口 或者c 1a 问卜f 6 1 是定 理 因此。自然模型 k 一定满足s e q u e n t f c iam 卜m 或者一a 问卜f 6 旦啦型翌垒整丝堡型里堡 1 5 也就是说，l f 4 d l l n 。= 【c 1 1 帆 【问l 帆= c a d ，这里l 1 】帆= 口，i f 6 1 l 帆= 6 是l 中的元素 因此，我们得到：c ad ( = e ) sn 或6 i 这是矛盾的 那么在a ( t ( l ) ) 中，我们得到 【r a l v f b l l 【r c la f d l 】 然而在l 中，我们有 8 v b = c a d 因此，l 是与a ( t ( l ) ) 不同的，然而我们可以看到如果我们在t ( l ) 中添加公理 f c la d l 卜n 1v 6 1 那么l 与a ( t ( l ) ) 是同构的，但是这个理论已经与前面一个不同了，因此我们通过通 过添加新的公理得到一个新的理论p ( l ) 现在，基于给定个稳定的d d - 半格l ，我们通过对t ( l ) 添加新的公理，得到个 新的d i s j u n c t i v e 命题理论p ( 工) 对于任何l 中的有限序列d l ，d 2 d 。且对于c o