有限余代数模态逻辑的可定义性和规范化

135理论计算机科学电子笔记65第1期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 65. html21页s有限余代数模态逻辑的可定义性、规范模型、亚历山大·库尔茨1CWIP.O. Box 94079，1090GBAmsterdam荷兰德克·帕丁森2Lu d wig-M aximili ans-Universit？tMu？nc henOettt i ngenstr. 67，80538MuénchenGermany摘要本文从可以对余代数的行为进行有限观察的角度来研究余代数。基于终端序列，引入了有限行为和有限谓词的概念。定义了一个态射保持有限性态的余代数范畴Beh ω（T）.然后，我们研究了有限余代数模态逻辑的可定义性和紧性，证明了Beh ω（T）中的最终对象推广了模态逻辑中规范模型的概念，并研究了由终结序列的有限部分在余代数上诱导的拓扑。介绍集合上的内函子T的余代数包含许多类型的状态基系统，包括Kripke模型和框架，标记转移系统，Moore和Mealy自动机和确定性系统，例如Rutten [22] 。 关 于 模 态 逻 辑 作 为 余 代 数 的 具 体 化 语 言 的 研 究 始 于Moss[15]，并在E.G.[14，21，20，8，9]。模态逻辑和余代数之间的关系在[12]中已经解释如下。用Z表示最终余代数的载体，我们可以1 电子邮件地址：kurz@cwi.nl2电子邮件：pattinso@informatik.uni-muenchen.de·2002年由ElsevierSc ie nceB出版。 V. 操作访问根据C CB Y-NC-N D许可证进行。库尔兹和帕丁森136⊆考虑作为模态公式的语义，子集[]]Z满足- 是的这里的直觉是：Z的元素是行为，模态公式的含义是行为的属性（即集合），定义如下：- 是的如果我们感兴趣的逻辑在允许定义Z的所有子集的意义上是完全表达的，那么我们可以识别模态公式和Z的子集，从而产生一种代数地研究模态逻辑的方法，参见[12，13]。不幸的是，由有限语法给出的模态逻辑通常不能完全表达。原因很简单，不是所有的属性都可以用有限的语言来描述。本文的主要主题之一是寻求一种模态逻辑的语义，它完全适合于有限模态逻辑，就像前一段中概述的语义适合于完全表达的模态逻辑一样。用来解释有限性的关键概念是内函子T的所谓终结序列（Tn1）。终结序列（Tn 1）可以理解为逼近终结余代数，见[1]。直观地说，第n次近似的元素表示可以在n个步骤中观察到的系统的行为。在[16，17]之后，秩为n的无穷模态公式的语义将是子集[]]<$Tn 1。3在函子T将有限集合映射到有限集合的情况下，这种方法结果是有限模态逻辑和它们的语义之间的完美匹配：对于所有有限序数n和Tn1的所有子集，我们可以假设一个定义这个子集的公式如果T将有限集合映射到无限集合，例如，对于具有无限多个原子命题的逻辑，将存在Tn1的子集，它们不由单个有限公式定义这是在第5节中在逼近Tn1上引入拓扑τn的原因之一，其思想是无穷公式对应于闭子集。这篇论文的主要新颖之处可能是在第2节中引入了范畴Behω（T），它以余代数为对象，以函数为态射，保持有限行为。本文的主张之一是Behω（T）对于有限模态逻辑的作用就像Coalg（T）对于完全表达模态逻辑的作用一样。在第4节中，我们证明了Behω（T）总是有一个最终对象。此外，Behω（T）中的最终对象与模态逻辑中已知的规范模型进行了比较。当我们专注于有限逻辑时出现的另一个问题是紧性。余代数模态逻辑的紧性比标准模态逻辑的紧性复杂.在标准模态逻辑中，紧致性是通过范本特姆将模态逻辑公式转换为一阶公式而继承自一阶逻辑的紧致性。该论点依赖于这样一个事实，因为[3]在本文中，我们只研究具有有限秩的模态公式，也就是说，我们排除了谈论无限数量的过渡步骤的模态，例如动态逻辑的“总是”和时态逻辑的库尔兹和帕丁森137LL∼P ×P⟨ ⟩ → ×∈一个合适的一阶语言，的模型正是Kripke模型。因此，如果我们改变模型的类别，这个论证失败也就不足为奇了。例如，模态逻辑在有限分支的Kripke模型上不是紧凑的。由于Kripke模型和有限分支Kripke模型都自然地表现为余代数的范畴，我们不能期望余代数的有限模态逻辑一般都是紧的。假设T将有限集映射到有限集，并基于第4节和第5节，第6节刻画了T-余代数的有限模态逻辑为紧的函子T1符号和标记考虑了集闭函子T的余代数. T-余代数和余代数态射的范畴记为Coalg（T）. 最后的T-余代数，记为Z=（Z，Z），如果它存在的话，可以通过如下的命题定义为同构：对于所有的A ∈ Coalg（T），存在唯一的A：A→Z。给定A中的一个元素a，我们称（A，a）为一个过程，A.行为。 两个过程（A，a）和（B，b）在行为上等价（记为（A，a）（B，b）），如果它们可以由余代数的态射来标识，即如果存在（C，c）∈ Coalg（T）且f：A → C，g：B → C ∈ Coalg（T）使得f（a）= g（b）。如果最终余代数存在，这显然等价于！A（a）=！B（b）。例1.1 [流]对于集合D，考虑TX = D ×X。 给定一个余代数α = head，tail：A D A，一个元素a A的（完全）行为是无限列表（head（a），head（tail（a）），head（tail（a），. . ）. 因此，最终余代数Z=（DN，N头，N尾）由D上的无限列表给出。例1.2 [Kripke模型]设Prop是可数无限集。函子T（X）=XProp的Coalge- bras是Kripke模型.行为等价的共代数概念与模态逻辑中的双模拟的标准概念一致我们已经看到了最终余代数（如果它存在的话）是如何提供了一个be-conscious的概念的。然而，一般来说，过程的行为代表了无限数量的信息。本文研究了过程的性质，这些性质可以由有限的信息量来指定。因此，最终的近似（包含所有过程的无限行为）必须被无限近似所取代。这些近似由底层内函子T的所谓终结序列的（无穷部分）提供。1.1所述末端序列终结序列可以被认为是终结余代数的近似。以下定义取自[24]。T的末端序列 是一个有序索引的集合序列（Zα）以及一族（pα）β≤α函数pα：Zα→Zβ，对所有序数β ββ≤α，使得库尔兹和帕丁森138β→βn⊆β+1βααγγβ• 对于所有β≤α，Zα+1=TZα和pα+1=Tpα• 当γ≤β≤α时，pα=idZ和pα=pβ<$pα• 当α是极限序数时，锥（Zα，（pα））β< α是极限的.考虑Zα是T对空图极限1的α-折叠应用，我们在下式中写Zα=Tα直觉上，Tn1表示可以在n个步骤中显示的例如，如果TX=D×X，nTn1n= Dn包含长度n的所有列。注意，每个余代数（C，γ）在终端序列上产生一个锥（C，（γα：CTα1））定义1.3给定（C，γ）∈Coalg（T），令γ0=！C：C→ 1表示唯一映射。对于后继序数α=β+1，设γ α：C→T α 1 = Tγ β<$γ。若α是极限序数，则设γα是唯一映射，对于所有β α。我们将经常使用以下简单的命题1.4设n为序数。(i) 设f：（A，α）→（B，β）是余代数态射. 则βn<$f = αn。(ii) 设（A，α）∈ Coalg（T）.则pn+1<$T（αn）<$α= αn.1.2余代数模态逻辑我们解释如何从给定的函子T：Set→Set中提取模态语言。继[16，17]之后，我们考虑由预提升给出的余代数的模态逻辑定义1.5T的谓词提升是自然变换λ：2 → 2 <$T，其中2表示逆变幂集函子。例1.6考虑TX = P（X）× P（A），其中A是一组原子命题。 则T-余代数与原子集A上的Kripke模型是1-1对应的.我们演示了如何捕捉使用谓词提升原子和模态设a∈A，考虑由下式给出的提升λ和λaλ（X）（x）={（x∈，a）∈P（X）×P（A）|xx}λa（X）（x）={（x<$，a）∈P（X）×P（A）|a∈a}。Given（C，γ）∈Coal g（T），我们记c→cifc，c∈C且c∈π1<$γ（c）. 如果c∈C，a∈A，我们写c| = ai <$a∈π2<$γ（c）.对于模态的情况，考虑一个子集cC，我们认为它是模态公式的解释c= [[]。然后γ−1<$λ（C）（c）={c∈C|cc→c<$=<$c<$∈c}对应于对“零”的解释。相同的公式，λ被替换库尔兹和帕丁森139∈∈由λa得出γ−1<$λ a（C）（c）={c∈C|C| = a}。因此，给定任何c∈C，我们可以使用提升λa来捕获满足a的世界的集合。✷定义1.7（L（T，Λ）的语义和语义）给定T的预提升集合Λ，我们考虑语言L（T，Λ），通常缩写为L（Λ），它由文法：：= ff |ϕ→ψ |[λ]（λ∈ Λ）对于结构（C，γ）∈Coalg（T），语义[[]]γ<$C由下式给出：[[ff]] γ=[[→]]γ=（C\[[]]γ）<$[[]]γ[[λ]<$]γ=γ−1<$λ（C）（[[]]γ）记法1.8（模态逻辑ML）在T = P ×PProp，Prop可数无限次的情况下，我们用ML表示L（T，Λ），其中Λ与上面的例子一样。ML是Kripke模型的标准模态逻辑。在本节的剩余部分中，我们证明了每个公式<$N∈ L（Λ）对某个n∈N产生一个谓词t<$Tn 1。给定任意结构（C，γ）Coal g（T），我们知道[]]γ=γn−1（t），其中γn在定义1.3中定义。定义1.9（秩为n的公式）设L0表示命题逻辑的公式集，即L0由文法L03，：：= ff |ϕ →ψ映射d0：L0→ P（1）由d0（n）= 1给出，其中n是重言式，且d0（）=，否则。对于n≥ 0，集合Ln+1由文法给出：L n+13，：：= ff |ϕ→ψ |[λ] Q（λ∈ Λ，Q∈ Ln）映射dn+1：Ln+1→ P（Tn+11）由下式归纳给出：ff→→我们把L n中的公式称为秩为n的公式。 对于n ∈ L n，我们也写[[n]] n或者简单地[[]]而不是d n（）。例1.10在ML的情况下，公式秩的等价定义如下：rank（ff）= 0，rank（ff→n）= max{rank（ff），depth（n）}，rank（p）= 1，对于p∈Prop，rank（n）=rank（n）+ 1。这是模态逻辑（其中rank（p）= 0）中标准定义的轻微变化，但可以用于相同的效果。直觉上，公式Ln描述了考虑n个过渡步骤当把集合Tn1看作是库尔兹和帕丁森140⊆⊆L∈对于可以在n个过渡步骤中表现出的行为，值dn（k）是k的模型独立解释。我们注意到，每个公式都包含在其中一个Ln中命题1.11L（Λ）=n∈NLn.下面的命题支持这样的直觉：dn（n）是n的语义模型无关的表示，对于n∈Ln。命题1.12设（C，γ）∈ Coalg（T）. 然后[[]]γ=γn−1<$dn（）对所有n∈ N和所有n ∈Ln.通过使用谓词提升的自然性对n进行归纳来证明。✷为了获得可定义性结果，我们必须假设所考虑的逻辑是合理表达的。我们处理两个表达性的概念：逻辑，它允许通过公式表示每个t Tn 1，以及允许划分每个谓词t的逻辑 T n 1的一组公式。正式定义如下：定义1.13（公式-（集合-）表达）语言L（T，Λ）称为• 公式表达的，如果每个dn是满射• 公式集表达式，如果每个Dn是满射，其中dn如定义1.9中所述，并且Dn定义为Dn：PL n→ PT n 1， Φ n →{d n（n）：n∈ Φ}。为了使（T，Λ）具有表达性，我们必须在谓词提升的集合上设置一个完备性条件。定义1.14（分离）（i）设C是一个集合，C ∈ P（C）是C的子集系。我们称C是分离的，如果映射s：C→ P（C），s（c）={c∈ C|c∈c}是monic的。(ii)C的谓词提升的集合Λ称为分离，如果{λ（C）（c）|λ∈Λ，c <$C}是TC的子集的分离集，对于所有集合C。分离的思想是C的各个点可以由谓词P∈ C区分。传递到谓词提升，我们可以通过谓词提升来区分各个后继者x TX，假设X的所有点都可以区分。分离性能存在于许多实施例中，特别是实施例1.6中。例1.15设TX=P（X）× P（A），对于某个原子命题集合A.考虑Λ={λ}<${λ a|a∈A}如例1.6所定义。然后，分离。库尔兹和帕丁森141⊆⊆⊆⊆假设T将有限集合映射到有限集合，这对应于在Kripke模型的情况下只有有限多个命题变量的事实，人们很容易建立命题1.16假设T将有限集合映射到有限集合，且Λ是分离的。则L（T，Λ）是公式表达的。给定一个结构（C，γ）∈Coalg（T），上面的命题说，每个谓词ecConC，其中对于somt，实际上可以用公式表示。在Kripke模型的情况下，我们有命题1.17设T=P×PProp，Prop可数无穷大，且L（T，Λ）=ML.则L（T，Λ）是公式集表达的。给定一个结构（C，γ）∈Coalg（P × PProp），上面的命题说，每个预测ConC，其中对于somt，可以用一组公式来表示。2有限谓词与范畴Behω（T）行为谓词，即在观测等价下不变的余代数上的谓词在这里，我们感兴趣的是无穷行为谓词，我们建议将它们视为由终端序列给出的Tn1，n ω首先，回顾定义1.3，我们定义了n步行为等价和秩为n的谓词的概念。定义2.1（n-行为等价）设n为序数。 对两个余代数A=（A，α），B =（B，β）定义（A，a）<$n（B，b）i <$α n（a）= β n（a）.类似地，A<$nBi <$α n（A）= β n（B）且A <$<ωBi <$α n（A）= β n（B）对所有n<ω。在最终余代数存在的假设下，我们认为两个点x和y是行为等价的，如果它们被唯一的态射标识到最终余代数中。如[1]所示，这等价于对所有序数n，αn（x）=αn（y）。我们即将介绍的有限行为谓词的概念，将上述方程的有效性限制在有限序数上。注2.2当（A，a）<$ω（B，b）惠<$n ω.（A，a）n ω。阿肯湾设TX={a，b} ×X，A是带载体{a，b}ω的最终余代数，B是带载体{s·aω：s∈ {a，b}ω}的子余代数.例2.3对于TX = PX×PProp，n-行为等价是[5]中研究的模态逻辑的有界互模拟（稍微变化）。库尔兹和帕丁森142⊆|⇔∈⇔∈⇔∈n定义2.4（秩为n的行为谓词）一个集合S T n1称为秩为n的行为谓词。一个过程（A，α，a）满足S，记作（A，α，a）|= S，通常缩写为a| =S，i <$α n（a）∈S.我们还使用标准符号，如（A，α）|= S惠a∈A。一|= S且[[S]]（A，α）={a∈A：a|=S}和Mod（S）={A∈Coal g（T）：A|=S}。例2.5设λ∈ L（T，Λ）是秩为n的公式。[1][2][3][4][5][5][6][7][7][8][定义1.9）。如果T将有限集合映射到有限集合，并且Λ是分离的，则每个谓词STn1都由公式表示（参见。提案1.16）。在ML的情况下，每个谓词都由一组公式表示（参见。提案1. 17）。注2.6在[12，11]中，有人提出通过把最终余代数的子集看作模态公式的语义来研究模态逻辑。从这个角度来看，这里提出的方法是一个特例。设（Z，Z）为最终代数。 STn1在逻辑上等于n−1（S）<$Z。实际上，（A，a）=Sαn（a）Sn（！A（a））S！A （ a ）n−1（S）这是定义的满足模态公式的子集的最终余代数。这将在下一节中使用。秩为n的谓词和n-行为等价由以下命题联系起来。命题2.7假设L（T，Λ）是公式表达的。则对所有A和A中的a，存在<$（A，a）∈ L（T，Λ）使得（A，a）<$n（B，b）惠（B，b）|A，a）.下面是模态逻辑中一个众所周知的结果（参见：[5]，命题2.8）。命题2.8假设L（T，Λ）是公式集表达的，并考虑A，B∈Coalg（T），a在A中，b在B中. 然后（A，a）n（B，b） ⇐⇒（一个|=优惠 B|对于秩为n的所有L∈ L（T，Λ），我们现在定义余代数范畴Behω（T），它具有那些保持有限行为的函数作为态射。定义2.9（Behω（T））范畴Behω（T）有T-余代数作为对象。态射f：（A，α）→（B，β）是这样的函数f：A→B，使得对于所有n< ω，βn<$f= α n.注2.10对于f：A→B，下列每一个等价于f是Behω（T）中的态射f：（A，α）→（B，β）βωf=αωn< ω。1. a∈A。f（a）|= S优惠a| = S注2.11显然，余代数f：（A，α）→（B，β）∈Coalg（T）的每个态射也是态射f∈Behω（T）。从而得到一个函包含Coalg（T）→Behω（T）.有两个不同的原因，为什么Behω（T）库尔兹和帕丁森143zω（T）包含比Coalg（T）更多的态射。第一个是Behω（T）-态射只考虑有限行为，第二个是Behω（T）-态射只保持不涉及着色的行为性质。注2.12为了解释Behω（T）与Coalg（T）的关系，考虑以下类别c-Beh（T），Beh（T）Jc-Behω （T），J.B.ehJ它们都有余代数作为对象，态射如下。 f：（A，α）→（B，β）是Beh（T）-态射i ∈ α n（a）= β n（f（a））. c-Beh（T）和c-Beh ω（T）的定义遵循相同的思想，但考虑了着色：f：（A，α）→（B，β）是c-Beh ω（T）-态射i <$f是Behω（T ×C）-态射（A，<$α，v <$f<$）→（B，<$β，v<$），对所有C ∈ Set和v：B → C。若Coalg（T）有余自由余代数，则c-Beh（T）=Coalg（T）.如果T是无穷的（即，ω-可达）则Behω（T）=Beh（T）和c-Behω（T）=c-Beh（T）.相反的命题是否成立，即c-Behω（T）=c-Beh（T）是否意味着T是无穷的，这是一个悬而未决的问题。✷本文的主张之一是，研究余代数的有限模态逻辑，将Coalg（T）中已知的技术和思想转移到Behω（T）中是有益的。例如，在第4节中，我们将证明Behω（T）总是有一个最终对象。3可定义性结果为了定义性的目的，我们假设存在一个最终余代数Z=（Z，n）。我们首先注意到下面的简单命题，它将Tn1上的谓词与Z上的谓词联系起来。3.我的朋友1（i）对于一个S，它保持A|=SiA|=n−1（S）。(ii) 对于任何S Z，它持有A|= S仅当A|= n（S）。(iii) 我是说... Sn−1（n（S））和STn1。 n（我们现在可以证明定理3.2B类Coalg（T）可由子集S<$Tn1i <$B定义是封闭的图像，余积，域的态射，和dom。证明对于B：B→Z，B∈ B。我们证明了B= Mod（n（S））.对于B∈ B，我们有，库尔兹和帕丁森144根据S，B的定义|= S，因此B| = n（S）由命题3.1.2。为了证明B<$Mod（<$n（S）），定义eS<$=（S<$，σ<$）为f<$n−1（<$n（S））的大余代数。这是从第三个论点开始的。1 .一、3thatn（S）=n（S<$），henceSnS<$. 辛切湾在图像和余积下是封闭的，B在联合下也是封闭的，因此S∈B。 由于B在rn下是封闭的，所以S′∈B。 我不知道|=n（S）。通过方案3。1 .一、一声，！一个因素通过n−1（（S））和hence ghS，即 有一种变形症是A→S。 由于B是r域上态射的闭域，所以A∈B. ✷下面的推论是一个直接的结果。推论3.3（i）设L（T，Λ）是公式表达的。则类B <$Coalg（T）可由秩为n的公式定义i <$B在像、余积、态射域和n下是闭的。(ii) 如果L（T，Λ）是公式集表达的，则类BCoalg（T）可由秩为n的公式集定义，iB在像、余积、态射域和n下是闭的。一个类似的证明给出了有限公式集合的表达性结果。定理3.4余代数类B可由集合S定义，其中S∈ S ≠<$n（S<$T n 1&n< ω）}i <$B在象、余积、态射域和<$ω下是闭<的。推论3.5如果L（T，Λ）是公式集表达的，则类B可由公式集i定义，且B在象、余积、态射域和ω下是闭<的。关于确保公式表达性和公式集表达性的充分条件，见命题1.16和1.17。4余代数的一个标准模型构造关于行为的推理，最终余代数起着核心作用，因为，给定唯一的余代数态射！A：A→Z从一个余代数A到最终余代数Z，对于A的每个元素a，我们可以考虑！A（a）的行为。类似地，余代数在Behω（T）中是最终的（参见定义2.9）由有限行为组成。我们首先证明了Behω（T）中存在最终余代数，然后证明了它们如何推广模态逻辑中已知的规范模型构造。4.1Behω（T）中终余代数Behω（T）中的余代数尾应该<因此，Behω（T）中的最终对象的载体将是Tω1的子集。回想一下，给定任何结构（C，γ），我们将唯一的中介映射γω：C→Tω1记为γω也就是说，所有的ω-行为都表现为Tω1中的某个γω（c）另一方面，不是每个点t∈Tω1都能通过某种结构（C，γ）和某种c∈C表示为t=γω（c）.例如，考虑有限库尔兹和帕丁森145∈∈∈ωK→ωωn◦nnn+1个幂集函子T=Pω.Worrell[24]证明了对于最终T-余代数（Z，n），态射<$ω：Z→Tω1不是满射的。因此，我们构造Behω（T）中余代数尾的载体为由所有t∈Tω1组成，它可以 其中有（C，γ）Coalg（T）和cC使得γ ω（c）= t。 然后剩下的就是在载体上找到一个合适的余代数结构。自始至终，我们固定“可实现”元素t T ω 1的集合KK={t ∈ T ω 1 |n（C，γ）∈ Coalg（T）. c∈C。 γ ω（c）= t}。对于每个k∈K，我们现在可以选择（Ck，γk）∈Coalg（T）和ck∈Ck，使得γ（ck）=k。注意，K是一个集合，这使我们能够考虑（C，γ）=（Ck，γk）k∈K其中副产物取Coalg（T）。用ink：Ck C表示联产物注入（通过在Coalg（T）中构造联产物，其也是集合范畴中的联产物注入），我们准备注意：引理4.1γ ω∈ k（c）= γ k（c），对所有k∈K和c∈ Ck。自γk的证明是进入极限锥的唯一中介映射，在T ω 1顶点上 ，证明了 对 所 有 n ∈ N ，γ n∈ k（c）= γ k（c）。为n= 0，这是显而易见的。 对于归纳步骤，我们计算k（c）中的γ n+1π =Tγn<$γ<$ink（c）=Tγn<$Tin k<$γk（c）=Tγk<$γk（c）=γk建立索赔✷我们得到以下直接推论：推论4.2对所有k∈K，存在c∈C，且γ ω（c）= k。换句话说，γω通过K因子化为γω=m e，m内射，e满射。现在考虑下图TTω1，Tm，TK，T，eTC，，.，，κ。γ.Tω1，，mK，，eCo其中o是e的任何单侧逆，即e∈o=idK，其存在性由e是满射来保证。我们让κ= Teγ o。注意κ：K→TK使K成为T-余代数.用pω：Tω1→Tn 1表示极限投影，我们得到库尔兹和帕丁森146nn◦→ωωωωωPnωn+1个n+1个n+1个nn+1个nn+1个引理4.3对于所有n∈N，κ n=p ω<$m，因此m= κ ω。证明我们继续通过归纳n，其中情况n=0是明显的。我们计算κn+1=T κn<$κ=T（pω<$m）<$Te <$γ<$o=T pω<$T（m<$e）<$γ <$o=n nTpωTγωγo=Tγnγo=γn+1o=pωγωo=pωmeo=pωm如所 期望的，用于诱导步骤。✷这一节的主要定理的证明现在很简单了。定理4.4Behω（T）有一个最终对象。证明我们证明了上面构造的（K，κ）在Behω（T）中是最终的。取任意对象（D，δ）∈Behω（T）。考虑映射δω：D→Tω1，它是锥（D，（δn）n∈N）和锥（Tω1，（pω）n∈N）之间唯一的中介映射.通过构造，δ ω因子为δ ω= m 其中m：KT ω 1如上所述。引理4.3δω= κωε h，这意味着h是Behω（T）-态射。h是唯一的，因为κω是单射的。注意，Behω（T）中的余代数最终不是唯一确定的，直到Coalg（T）中的同构。 在p ω+1：TT ω 1 →T ω 1是满射4的情况下，Behω（T）中的余代数final正是由右-p ω+1的逆。推论4.5假设pω+1是满射的 一个coalgebra是final，当ω（T）i时，Coalg（T）与某些（T）同构ω1，τ），其中pω+1◦τ=idTω1证明id Tω1。 这可以从τ n=pn，n< ω得出，归纳的情况是τ n+1=T（τ n）<$τ = T（p ω）<$τ = p ω <$p ω+1<$τ= p ω。‘only if’: Let (考虑在定理证明中构造的最终对象（K，κ） 设f：（A，α）→（K，κ）是唯一态射.特别地，f是iso且κ ω∈f=α ω。因为κω是单射的，所以αω也是。因为命题1。4（ii），α ω= p ω+1<$T（α ω）<$α，α ω也是我很抱歉，我是说。 Now定义eτ=T（αω）<$α<$αω−1。✷4.2典范模型设M是函子P ×PProp，Prop是可数无限集.模态逻辑ML的规范模型（例如参见[3，6]）是M-余代数（L，λR，λV<$）L{ΦML：Φ是最大一致的}λR：L→ PLΦ<$→{< $：<$∈ <$$><$$><$}λV：L→ PPropΦ→ΦProp[4]除了T = ω外，本文中所有的例子都是这样。 pω +1成立的一个充分条件是：ω p -cha的两个线性极限是p ω+1的两个线性极限。库尔兹和帕丁森147{}✷ωω2i=03i+1正则模型在范畴Th ML中是最终的，范畴Th ML以M-余代数为对象，态射f：（A，α）→（B，β）是函数f：A→B使得对于所有a∈A，a和f（a）具有相同的模态理论。从余代数的观点来看，无穷公式对应于Tn1的子集。沿着极限投影取逆像，每一组无穷公式都可以理解为Tω1的子集。直觉上，最大一致子集对应于最小（即单例）子集不T ω 1的T ω 1。我们通过证明范畴Behω（M）和ThML实际上是相同的来使这一点精确。命题4.6Behω（M）= ThML。证明我们必须证明对于任何余代数（A，α），（B，β）和任何函数f：A→B，βωf（a）=αω（a）惠Th（a）= Th（f（a）），这是一个相当大的[n]。 β n<$f（a）= α n（a）]惠[<$n <ω. ∀ϕ ∈ ML.rank（n）=nn（a| =优惠f（a）|这是命题2.8的一个推论。由于投影pω+1：MMω 1→Mω 1是满射的，我们知道：推论4.5：Behω（M）中的所有余代数（K，κ）最终都是余代数同构-通过K=Mω 1和pω+1的单侧逆κ.因为我们刚刚证明了正则模型在Behω（M）中是最终的，所以它确实是在前一小节中构造的（K，κ5有限观测研究了由终结序列诱导的余代数上的拓扑，并讨论了余代数的逻辑性质和拓扑性质。定义5.1（康托空间拓扑）设τ n是T n 1上的拓扑，对所有有限序数。若（A，α）∈Coalg（T），则由（τ n）n< ω诱导的拓扑τ A是由基生成的拓扑{αn−1（o）|n∈ω，o∈τn}开放的集合。 如果所有的τn都是离散的，我们称τA为康托空间拓扑。显然，τA使得所有投影αn连续。将康托集看作TX= 2×X的最终余代数，即由离散的τn=P（Tn1）诱导的拓扑，人们恢复了康托不连续。例5.2假设TX=2×X，其中2={ 0， 1}。考虑（最终）T-余代数（A，α），其中A=2N={f：N→ 2}，α（f）=（f（0），λn. f（n+1））。n（A，τA）是能发现最小C_∞的同胚（也称为n（中三分之一组，参见例如[10]）通过映射2N→ C，f ∈ N →∞·f（i）.库尔兹和帕丁森148→MMLL备注5.3(i) 设f：（A，α）（B，β）是余代数的同态。 则f是w.r.t.连续的。A和B上的拓扑结构。因此，从余代数（A，α）到拓扑空间（A，τA）的通路诱导函子Coalg（T）→Top。(ii) 设（A，α）∈ Coalg（T），对a0，a1∈ A，dA（a0，a1）= inf{2−n：k

下载后可阅读完整内容，剩余1页未读，立即下载