余代数的模态展开与引用代数和Stone空间的推广

SVVSS理论计算机科学电子笔记106（2004）243-259www.elsevier.com/locate/entcs余代数与逻辑的模态展开Alexander Kurza莱斯特大学b巴塞罗那大学摘要在本文中，我们构建了一个设置中，当一个逻辑支持一个经典的模态扩展可以精确的问题。给定一个完全自扩张逻辑，我们找到了Vietoris内函子对- 引用代数可以被定义，我们建议定义的模态扩展作为逻辑，- 余代数 作为一个例子，我们还证明了参照代数上的Vietoris内函子是如何推广Stone空间上的Vietoris内函子的。从另一个角度来看，我们研究了当一个“空间”范畴（X，A），即集合X配备了一个由X的子集组成的代数A时，允许定义幂空间V（以及因此的转移系统（X，A）→ V（X，A））。保留字：模态逻辑，模态展开，Vietoris闭函子，余代数，Stone空间。1介绍本文所研究的问题可以从不同的角度来解释和动机余代数动机我们研究的系统，其状态空间可以描述的一个集合X与代数A的子集X。我们认为A的元素是X上的可接受谓词（或可以对X中的状态进行的观察）。代数的运算反映了使用逻辑连接词从给定的观测值这种解释，以及与拓扑空间的类比，建议将这些结构称为逻辑空间在代数逻辑中，它们被称为引用代数。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.05.010244A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243V一个转移关系可以被认为是一个映射，它为X中的一个状态分配了它的后继者的集合。余代数的观点建议我们应该在逻辑空间范畴上寻找一个函子，它允许我们把系统表示为态射（X，A）-（VX，VA）。VX将是完整幂集PX的子集。为了了解VX上的允许谓词VA应该是什么，我们集中于以下两个基本观察，可以使用允许集对子集v∈ VX进行a∈A：v的所有元素是否都包含在a中，是否存在v的一个元素包含在a中。这使我们得到关于VX的以下基本可容许谓词：Qa ={v∈ VX|v∈ v ∈a}和Qa ={v∈ VX|v a}。这种基本可容许谓词的选择在拓扑学和域理论中是众所周知的，其中（VX，VA）被称为Vietoris空间或Plotkin幂域。看看在什么情况下，这种建设可以推广从拓扑空间是这项工作的目的之一。VX的构造是众所周知的，并在第3节中介绍。 本文的主要贡献在于给出了VA的一个构造。这种构造的动机是引用代数作为自扩张逻辑模型的逻辑解释，并使用自扩张逻辑的对偶理论。自延逻辑哲学逻辑在概念上的主要成就之一是弗雷格对意义和指称的区分，这体现在定义逻辑语言语义学的内涵方法和指称方法之间的正式区分中在指称方法中，公式的语义由它们的真值（指称）给出。指称方法只适用于那些替代性原理成立的逻辑，即那些具有相同真值的任何两个句子可以相互替代而不改变结果的真值的逻辑。替代性原则不适用于内涵逻辑，模态逻辑也许是其中最著名的例子。在任何内涵方法中，语义结构总是基于状态集或可能的世界然后，通过将φ映射到它是真实的可能世界的子集。这个集合通常被称为强度。替代性原理不适用于给定世界中具有相同外延的公式，但适用于具有相同内涵的公式A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243245∧∧联系我们P即在所有可能的世界中具有相同的外延。克里普克结构可能是内涵语义学最著名的例子。组合性是语义学外延和内涵研究的基本要求。众所周知，指称方法通过赋予真值集代数结构来解释组合性：典型的例子是布尔代数2，其中可以计算复合公式的真值和真值的关系。同样地，在任何内涵集合中解释组合语义意味着赋予P（X）（的选定子集）代数结构，以便可以从X和X的内涵计算复合公式X的内涵（并且通常对运算的定义有进一步的要求：例如，ϕ与“”和“”的内涵的交集重合，因此打开）。模态逻辑的一般框架是一个典型的例子：它们被定义为三元组（X，R，A），其中X是一个非空的状态集，R<$X×X，A是布尔代数P（X）的一个子代数。在代数逻辑中，语义的内涵方法是在一般的设置中处理的，该设置从逻辑的特定相似性类型中抽象出来：对于每个代数相似性类型τ，τ-逻辑的语义结构是引用代数，即元组（X，A），使得X=A是τ-代数X的子集（不需要是X的子代数） （X））。Selfex-张力逻辑，其中由Wo′ j cick计算的逻辑是可靠的和完整的。它们对应的参照代数类。它们的特征之一是任何两个公式是可互导的当且仅当它们映射到任何参照代数中的相同子集。因此，对于自外延逻辑，可相互推导性以一种组合的方式捕获了意义的同一性（内涵）。由于作为自扩张逻辑的规范语义结构的参照代数可以被看作一般框架的抽象形式，因此自扩张逻辑可以被松散地认为是广义模态逻辑。另一方面，许多既不是模态的也不是内涵的逻辑，如经典的和直觉主义的命题逻辑，也是自外延的。本文是一个调查线，旨在更好地理解自我扩张逻辑和模态之间的关系的起点。逻辑动机从代数的角度研究模态逻辑的一般方法是将模态算子视为扩展底层逻辑签名。我们采取相反的观点，问246A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243SS−→StnV自我延伸逻辑支持模式？我们的目标是建立一个上下文，在这个上下文中，这个问题可以变得精确，即定义自延拓逻辑的模态展开的一般理论，使得模态展开的算子具有预定的语义和性质。在本文中，我们集中于扩展一个逻辑与模态算子Q和Q，这是正常的和相关的像在模态逻辑K。因此，我们将把逻辑的模态扩展定义为这样一种逻辑，它规范地产生于我们有意构造的语义结构，以强制实现所需的语义和属性。我们构造这些结构作为余代数的Vietoris endofunctorV的范畴上的参考代数与S，S-参考代数。反过来，这样得到的V-余代数可以表示为模态扩张相似型的参照代数：的确，V-余代数是一个集映射ρ：X−→VX使得ρ−1∈Hom（VA， A）。然后ρ将对应于参照代数（X，AJ），其中AJ 是模态与ρ−1∈Hom（VA， A）相关联的A的展开。S的模态展开将被定义为从这类参照代数产生的逻辑。我们建议说，一个自延逻辑支持经典模式如果它的模态展开可以按照上面的草图来构造的话。对偶理论本文的主要贡献是构造了S-参照代数上的Vietoris一个很自然的问题是，这个概念如何与文献中已知的某些拓扑空间类上的Vietoris内函子（如Stone和Priestley空间上的Vietoris内函子）相关联。这种构造有一种自然的方式来扩展已知的构造，它是基于这样一个事实，即那些拓扑空间可以表示为参照代数。实际上，这些拓扑空间的范畴同构于指称代数的全子范畴，以这样一种方式，下面的图可以交换：StnRASK−−V−→RASPriRAS−→初级−−V−→RAS。这些嵌入是一个更普遍的图景的一部分，利用自延拓逻辑的对偶理论，简要地介绍了在2.2.这个理论由两部分组成：第一部分定义了同一个自延逻辑S的模型范畴之间的对偶，即根据抽象Al理论为SA. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243247SVA几何逻辑和-参照代数。这种对偶性是围绕逻辑形成的，因为地图集和参照代数在这种逻辑中相互对应。 一种完整地保存其逻辑内容的方式。这种二重性的关键特征是，它的逻辑意义是内在于它的定义之中的。第二部分是关于这种对偶性如何一致地推广了一大类已知的对偶性，其中包括斯通对偶性和普里斯特利对偶性。所涉及的代数和拓扑空间范畴被证明分别同构于图集和参照代数范畴，以这样一种方式，对偶函子也被提升，并且由于图集和参照代数的对偶的逻辑输入由定义给出，这种嵌入提供了一种方法来使嵌入的对偶的逻辑解释明确和统一。这并不奇怪：对偶的逻辑意义在文献中已经被广泛地认识到，通过展示它们与可靠性和完备性定理的系统联系，对偶在文献中已经被广泛地用于对基于集合的结构给出逻辑解释，拓扑空间和余代数。自延逻辑的对偶理论在我们这里介绍的背景中起着至关重要的作用。新颖之处在于，对独立定义的基于集合的结构给出逻辑解释：它用于从我们想要模态扩展的逻辑，以及从模态扩展的预定语义和属性中定义相关工作这项工作是在抽象代数逻辑（AAL）和对偶理论的背景下进行的。专著[2]提供了AAL基础的详细说明。这本书[4]是对偶理论基础的标准参考。文[7]发展了自扩张逻辑的对偶理论。自扩张逻辑用参照代数的特征化出现在[11]和[12]中。 文[6]和[8]分别证明了Stone和Priestley空间上Vietoris内函子的余代数是模态逻辑K和PML的充分语义结构。在[9]中可以找到一些模态直觉逻辑的类似但部分的结果。 第4节中的描述[15]在许多地方，人们都有自己的看法。在[1]中发展的自然对偶理论和有界格扩张理论[3]将与这项工作的进一步发展有关（也见第6节中的讨论）。确认本文是第二作者在莱斯特大学计算机科学系访问期间写的。的248A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243一A A S A −→ A第二作者要感谢莱斯特大学计算机科学研究小组的热情款待，并为她的逗留提供部分我们要感谢Ramon Jansana阅读了本书的初步版本，并提出了许多有用的意见。2关于自延拓逻辑的几个在这一节中，τ是一个代数相似型，是一个τ-代数，A是它的载体，Fm是一个给定变量集Var上的自由τ-代数（公式），S=（Fm，S）是一个τ-推论关系，H=（W，A）是一个τ-参照代数，X是H的定义域，Q=（A，B）是一个τ-图集。2.1基本概念一个τ-后果关系是一对S=（Fm，<$S），其中Fm是给定变量集上的公式的τ-代数，<$S<$P（Fm）×Fm使得对所有的Γ<${<$}<$ Fm，1. 如果ε∈Γ，则Γ ∈Sε。2. 如果Γ S且Γ则S。3. 若对任意的ε∈ΓSε，则εSε。如果T<$Fm在S下是闭的，即如果T<$S <$，则对每一个<$∈ Fm都有<$∈T，则T是S的理论，或S-理论。 Th（S）是S-理论的集合。 对所有的Γ{}Fm，S是无穷的，如果ΓS，则对某个有限集，好吧S是结构的i ∈ F，对所有的Γ<${<$}<$Fm，对所有的σ∈Hom（Fm，Fm），如果Γ<$S <$，则σ[Γ]<$Sσ（<$）.一个因果逻辑是一个有限的和结构性的结果关系。S的可互导关系是等价关系E <$S={（n，n∈ Fm×Fm|ϕ► Sψ and ψ► Sϕ}. S是自扩张的，如果E是Fm的一个同余。对每个τ-代数A和每个F<$A，F是一个S-滤子i <$，对每个h∈Hom（Fm，A）和每个S-滤Γ <$S<$，如果h[Γ]<$F，则h（<$）∈F. F iS（A）是A的S滤子的集合。FiS（Fm）=Th（S）。S是完全自扩张的，对每个代数A，Frege关系Λ S={εa，bε |a ∈ Fi，i∈F，对任意F∈FiS（A）}，a ∈ Fi，i ∈ b ∈ F是A的同余. Fm上的弗雷格关系式是ES。如果S是完全自扩张的，则A是S-代数i <$Λ S是单位关系。例如，如果S是经典命题逻辑，则布尔代数是S-代数。对于每个完全自扩张逻辑S和每个代数、/ΛS是一个- 代数设q：/ΛS 是 相关的正则投影。注2.1对于每个完全自扩张的逻辑S，且每个h∈Hom（A1，A2），赋值q1（a）<$→q2（h（a））定义一个同态qh∈A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243249Q对于每个h∈Hom（Fm，A），γ∈Γh（γ）<$h（γ）. H是S-参照代数Hom（A1/ΛS，A2/ ΛS）.证据对每个h∈Hom（A1，A2）和每个F ∈FiS（A2），h−1（F）∈FiS（A1）.因此，<$a，b <$∈ Λ S（A1）意味着<$h（a），h（b）<$∈ Λ S（A2），由此可以得出qh的定义是好的。其余的都是例行公事。作为这一评论的结果，Fm/ES是自由S-代数。2.2自延逻辑模型与对偶性一个τ-参照代数是一个对H=（X，A），其中X是一个非空集，A是X的子集的τ-代数。 H是离散的i∈X，如果a∈Y i ∈B∈Y，则a=b。由H导出的结果关系定义如下：对于Γ{}Fm， |=Hi我的宝贝|= H。 后果关系|= H是结构性的和自伸展的通过建设。相反，如果S是自扩张的，则存在一个H，使得S=|= H。对于每个H=（W，A）和HJ=（XJ，AJ），h∈Hom（H，HJ）i <$h∈Set（X，XJ）和h−1∈Hom（AJ， A）。h∈Hom（H，HJ）是严格的i <$h −1∈Hom（AJ， A）是onto。一个τ-atlas是一个对Q=（A，B）使得A是一个τ-代数，B是一个A 的 子 集 的 集 合 。 图集Q的 弗 雷 格 关 系 是 等 价 关 系 Λ Q={<$a ，b<$∈A×A|对每个B∈ B，a∈B惠b∈B}。 Q是Fregean的，i ∈ ΛQ是A的同余。Q是Frege约化的（FRA）i <$ΛQ是A上的恒等关系。如果Q =（A，B）是Fregean的，则商图谱Q=（A，B），其中A = A/Λ Q，B={B|B∈ B}，B<$= p [B]，p：A → A<$是正则投影，是Frege约化的.由Q诱导的结果定义为：对于每个Γ <${<$}<$F m，Γ|对每个h∈Hom（Fm，A）和每个B∈ B，若h [Γ]<$B则h（<$）∈B. Q是一个S-atlasi|= Qi <$B <$F iS（A）。对于所有的Q和Q J，h∈Hom（Q，Q J）i <$h∈Hom（A，A J）和{h−1（BJ）|BJ∈ B J}<$B. h∈Hom（Q，Q J）是严格i <${h−1（BJ）|BJ∈ B J}= B.例如，正则投影p∈Hom（Q，Q<$）是严格的且在上。 如果h∈Hom（Q，Q J）是严格的且在上，则|= QJ=|= Q。特别地，如果h∈Hom（Q，QJ）是严格的且在上，且Q是S-图集，则QJ是S-图集.因此，如果Q是一个FregeanS-atlas，那么Q是一个Frege-reducedS-atlas。Fregean图集Q =（A，B）的对偶参照代数为Q+=（B，A），其中A ={a |a ∈ A，a ={B ∈ B |a ∈ B}，对于每个a ∈ A。由于Λ Q是一个同余，f或每一个f ∈ τ，我们可以通过声明fA（a1，.，an）= fA（al，.，an）对于每个a1，.，an∈A. Q+是一个整数，|= Q+。|= Q+ .特别地，如果Q是S-图谱，则Q+是S-参照代数。 若h∈Hom（Q，QJ），则nh+：=h−1∈Hom（QJ+，Q+）. 如果h是0，250A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243∈ H H ∈ HH公司简介FG∈V→ VV（）+（）+那么h+是严格的，如果h是严格的，那么h+是onto。H=（X，A）的对偶图谱是H+=（A，X），其中X={x|x ∈X}+且x={Y∈A|x∈Y}对于每个x∈X. H是一个FRA，|=H=|=H+。特别是如果是一- 引用代数，则+是一- 阿特拉斯如果hHom（，J），则h+：=h−1Hom（J+，+）。 如果h是onto，则h+是strict，如果h是strict，则h+是onto。这些对应定义了Frege约化的图谱和图谱态射的范畴FRA与离散参照代数和参照代数态射的范畴FRA之间的对偶等价。这种对偶的一个特征是，具有分配格部分的代数范畴的一大类对偶可以均匀地“嵌入”其中，这就是Stone和Priestley对偶的情况，以及BAO和描述性一般框架的对偶的情况。例如，对于每个布尔代数（BA）A，设QA=（A，Ultr（A）），其中Ultr（A）是A的超滤子的集合，对于每个Stone空间X=（X，λ），设HX=（X，A），其中A是X的闭子集的BA。这些分配定义了两个协变的，忠实的和充分的函子Q. ：BA −→ FRA和H. ：Stn−→Stn，使得Hom（A，AJ）=Hom（QA，QAJ），Hom（X，XJ）=Hom（HX，HXJ），并且以下图可交换：BA−−−→StnStn −−→BAQ.. 。你... 。你... 。Q.. 。⏐FRA-3模态闭子集正如在引言中提到的，我们想在引用代数上定义一个函子V，使得V-余代数V：（W，A）−→（VW，VA）由一个转换关系W：W W W W和一个代数A组成，A的元素解释了可以从A中的谓词和经典模态算子Q和Q中构建的公式。也就是说，对于所有UA，A将包含集合QU ={X∈ VW|XU} 且QU ={X∈ VW|X U}。然后，给定（W，A），n：W→ VW和U∈ A，我们通过w D QU惠得到了Q和Q的经典语义 且wDQU惠（w）∈QU.A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243251ΦLQ，Φ LQlet [[Φ]]Q={U |QU ∈ Φ}和[[]] Q= W\{U |QU/∈θ}。从逻辑的角度来看，我们用两个模态算子扩展了A的签名，其语义如上所述。本节重点讨论独立于代数签名的VW的定义。在代数符号为空的情况下，我们也描述了VA.对于每个H，我们引入抽象符号集LQ（H）={QU|U ∈A}和LQ（H）={QU|U∈ A}，关系式|=由X| = QU 惠X UandX| = QU 优惠XU/=对于X∈W和U∈A. 设ThQ（X）={QU|X| = QU}，并且ThQ（X）={QU|X| = QU}。 Th（X）=（ThQ（X），ThQ（X））是X的模态理论。X，Y<$W模态等价，（X<$ThY）i <$Th（X）= Th（Y）. 为下面的命题是直接的。命题3.1对于所有XW，ΦLQ，ΦLQ(i) X[[Φ]]Q惠ΦThQ（X）(ii) X[[]]Q惠ThQ（X）上 面 的 1 和 2 都 构 成 了 一 个 伽 罗 瓦 连 接 （ 附 加 ） ， 并 且 写 作 [[<$Φ ，<$$>]]=[[Φ]]Q<$[[<$]]Q，我们可以将它们组合成一个伽罗瓦连接[[−]]E<$ThQ，ThQ<$（·）QQPWThQ，ThQ[[·]]（PLQ）op×PLQ特别地，（·）QQ=[[·]]ThQ，ThQ，明确地给出为XQQ={U∈A|X|= QU}（W\{U∈A|X|=/QU}）是将X映射到最大模态等价集的闭包算子。我们称集合XQQ为模态闭集。定义3.2设（W，A）是空签名的引用代数。VW ={XW|X = XQQ}。 V A ={QU|U∈ A}<${QU|U∈ A}。为f：（W，A）→（WJ，AJ），我们把Vf：VW→ VWJ，X<$→f[X]QQ。不难检验（Vf）−1（QUJ）=Qf−1（UJ），（Vf）−1（QUJ）=Qf −1（U J）. 因此（Vf）−1确实是一个映射V A J→ V A。备注3.3252A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243H≤VV(i) 在Vietoris函子的定义中对模态闭子集的限制保证了二叉引用代数映射到二叉引用代数。(ii) 由于这种基于模态闭子集的幂构造在拓扑学和Domain理论中是标准的，我们想在引用代数=（W，A）的上下文中提到一些相关的拓扑概念。特殊化顺序由下式给出：w≤wJ惠a∈ A. w∈a<$wJ∈ a.≤是一个preorder。 如果≤是偏序，则H是可微分的。每一个可容许的集合（即A中的每一个元素）都是上集合.1实际 上，是W上的最大关系，使得所有的容许集都是上集。上集与在任意并和交下可容许集的封闭性。一个集合是饱和的，如果它是可容许集合的交集;开放的，如果它是可容许集合的并集;封闭的，如果它是开放集合的补集。[[Φ]]Q与饱和集重合，[[Φ]]Q与闭集重合。也就是说，一个集合是模态闭的，如果它是饱和集和闭集的交集。在域理论中，饱和集和上集重合，模态闭集被称为凸集或透镜。4指涉代数在这一节中，我们假设一个完全自扩张逻辑S。给定一个S-参照代数（W，A），我们将构造Vietoris参照代数（W，A）， 执行以下步骤。(i) 构造由{ Q U}生成的自由S-代数G|U∈ A}<${QU|U ∈A}。(ii) 定义G的S -Filt e r s ' M的集合M = V W。(iii) 取（G，M）的商（G，M）w.r.t.模态S滤波器M.(iv) 求出（VW，VA）作为（同构于）（G，M）的对偶（M，G）。第一步是可能的，因为S是完全自延的。对于第二步，我们假设我们可以找到G的S-滤器的集合M，称为模态S-滤器，使得对于每个F∈ VW，存在唯一的MF∈ M，满足C1. 对于每个U∈A，QU∈MF惠F U和QU∈MF惠 FU，1Z <$W是上的，如果x ∈ Z且x ≤ y蕴涵y ∈ Z。A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243253S QG MQ GM以下属性适用于- 地图集=、、J=J，J（从参照代数（W，A），（WJ，AJ）得到）C2. A是G的一个同余，C3. 每个φ：G → G J 由一个参照代数态射（WJ，A J）导 出 →（W，A）是一个图集态射φ：Q →QJ。粗略地说，C1保证了MF的行为像F的模态理论，C2允许我们取将成为Vietoris代数的商，C3注意到也可以对态射进行构造为了完成第二步，我们注意到，通过C1，映射VW→ M，F<$→MF是单射的（因此也是双射的）：引理4.1对每个F，G∈ VW，如果FG，然后MFMG.证据如果F/= G，则我们可以假设x∈F\G。由于G是模态闭的，则U∈A使得a）x∈/U且G|=QUorb）x∈U和G|=/QU. 然后，使用ifF/U，nQU∈/MF，QU∈MG\MF. 然后，利用ifG<$U=<$nQU∈/MG，证明了QU∈MF\MG.Q对于第三步注意，如果C2成立，那么我们可以考虑商代数G=G/ ΛQ和正则投影p：G −→G。C3表明态射G → GJ诱导态射G → Gj：引理4.2对于每个h∈Hom（G，GJ），(i) 若<$a，b<$∈ΛQ，则< $h（a），h（b）<$∈ ΛQJ;(ii) 对于每个a∈ G，赋值h∈（a）−→pJ（h（a））定义一个态射h：G→ Gj。证据首先，对每个MJ∈ M J，如果h（a）∈MJ，则a∈h−1（MJ）∈ M，所以<$a，b<$∈ΛQ意味着b∈h−1（MJ），即h（b）∈MJ。其次，如果p（a）=p（b），则<$a，b<$∈ΛQ，所以<$h（a），h（b）<$∈ ΛQJ，即PJ（h（a））=PJ（h（b））。Q根据这一图谱，得到了Q=（G，M），即：，M={MF|F∈VW}，其中MF∈ V W=p[MF]。 如果ncep（a）=p（b），则对于每个F∈ V W，p−1（p[MF]）=MF成立。 因此p是一个空间t，是Q和Q_n之间的态射，当Q是一个Frege S-图集时，Q_n是一个Frege约化S-图集.特别地，M是G和M=M的S -滤波器的集合。 G.B.C. D. E.最后，考虑（G，M）的对偶M，G，它是一个S-RA（因为（G，M）是一个S-FRA）和双射θ：VW→M，F<$→MF. 新的维图像映射θ−1：P（MV）−→P（VW）严格限制到一个pΘ：G−→254A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243P VVQQJJ（W）. 我们定义A为Θ的像。下图概括了该构造。（W，A）f（WJ，AJ）（G，M）φ （GJ，MJ）p（G，M）PJ（Gj，Mj）（M，G）φ−1 （MJ，Gj）θ θ（VW，VA）Vf（VWJ，VAJ）定义4.3（Vietoris参照代数）对于每个S-参照代数H=（W，A），H的Vietoris参照代数是VH=V VW，VA与hVW的关系如定义3.2所示，VA由ive图像θ−1给出作为a bove。对任意的S-参照代数态射f：（W，A）→（WJ，AJ），设φ：GJ→Gbe有一个lgebrmorphism诱导dbyf−1：AJ→A，且Vf=θ−1<$φ <$− 1<$θ.模态算子的解释是预期的：命题4.4 Θ[p（QU）]= Q U和Θ[p（QU）]= Q U，对所有U ∈ A。证据对于每个F∈ VW，F∈Θ（p（QU））iF∈θ−1（p（QU））F∈Θ（p（QU））我的F∈θ−1（p（QU））我的p[MF]∈p（QU）我的p[MF]∈p（QU）我的我的p（QU）∈p[MF]QU∈MF我的我的p（QU）∈p[MF]QU∈MF我的FU我的FU/=我的F∈Q（U）我的F∈Q（U）. QVf由f的直接镜像给出：命题4.5 Vf（F）= f [F]对所有f：（W，A）→（W，A），F ∈ VW.证 据 我 们 省 略 了 同 构 p[·] ： M→M 。 对 于 所 有 UJ∈AJ ， 我 们 计 算f[F]QQ<$UJ惠f[F]<$UJ惠F<$f−1（UJ）惠Qf−1（UJ）∈φ∗A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243255G{|{|∈}MKMF优惠φ（QUJ）∈MF惠QUJ∈φ−1（MF）andndsimilarlyf[F]QQ<$UJ=/φ j∈φ−1（MF）.由于MJ中的φ−1（MF），从C1可以得出：φ−1（MF）=MfJ[F]QQ，thatis，θ−1<$φ−1<$θ（F）=f[F].QQQ例4.6设（W，A）为空签名的引用代数。2是集合QU UAQU UA。因为我们选择子集满足C1。C2是平凡的满足。对于C3，我们计算φ−1（MF）={tJ∈MFJ|φ（tJ）∈ MF}={QU J|Qf −1（U J）∈ MF}<${QU J|Qf −1（U J）}={QU J|F <$f−1（UJ）}<${QUJ|Ff−1（UJ）=/}={QUJ|f[F]<$UJ}<${QUJ|f[F]UJ/=[F]QQ. V A和Vf与前面的定义3.2一致，这是由上面的两个命题得出的。下一节将讨论另一个例子。5扩展示例：Stone Spaces在本节中，我们将证明，我们可以在与Stone空间对应的参照代数上构造Vietoris内函子，这些参照代数在2.2节中描述的嵌入下，并且这个构造扩展了Stone空间上Vietoris内函子K的熟悉定义，即下图交换：StnRAS−→Stn−−V−→RAS。在这种情况下，S是经典的命题演算，所以自由S-代数是自由布尔代数，S-滤波器是格滤波器。 设X=（X，A）是Stone空间，H=（X，A）是它的关联参照代数，即A是X的闭闭子集的布尔代数.众所周知，Vietoris空间K（X）的载体是X的闭子集的集合K（X），并且K（X）的闭子集的布尔代数由下式生成：QU ={X∈ VW|XU} 且QU ={X∈ VW|XU/=}，对于所有的U∈A。因此，命题4.4和4.5将考虑上面图的交换性，前提是：(i) H的模态闭子集族与K（X）重合2相应的逻辑S有序列Γφ惠φ∈ Γ;因此S-滤波器只是子集。256A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243{|∈}LH{|∈}QU}\（X\F{U∈ A |F|=/ QU}）已关闭。对于逆包含，令∈ ⊆·(ii) 存在由抽象符号集L（H）=LQ（H）<$LQ（H）生成的自由布尔代数G的一族滤波器M，其中LQ（H）=QU UA且Q（）=的QU UA，满足条件C1– C3 of Section命题5.1对任何Stone空间X =（X，λ），VX = K（X）.证据（1）显然，每个模态闭子集FQQ={U∈ A |F| =FK（X），并证明F = FQQ。 ‘’ is clear since ( )操作符. 相反，注意，由于X是Stone空间，则Clopen子集形成一个基，因此F={U∈ A|去你的。Q设G是由L（H）生成的自由布尔代数.众所周知，布尔代数的超滤子恰好是二元布尔代数2的顶元素的逆同态像。当G是自由的时，则每个h∈Hom（G，2）由它对L（H）的限制唯一确定。对于每一个F∈K（X），让我们考虑hF∈Hom（G，2）由以下赋值定义：对于每一个U∈A，hF（QU）= 1 i <$F<$U，hF（QU）= 1 i FU/=.设MF= h−1（1）是G的相应超滤子。通过构造，它认为，对于每个F∈K（X），MF是G的唯一超滤子，使得对于每个U∈A，QU ∈ MFi <$F <$U和QU ∈ MFi <$F<$U/=<$。所以集合M={MF|F∈K（X）}Ultr（A）满足第4节的条件C1。让我们考虑图集Q=（G，M）。很容易看出，对于布尔代数A的超滤子的每一个集合U，A上的关系ΛU，定义为aΛUbiV∈ U（a∈V惠b∈V），是A的一个同余。因此ΛQ是G的同余，所以M满足第4节的条件C2。对于C3，设f：X→XJ是连续映射，则f∈Hom（H，HJ）.下面的命题证明了相伴的自由布尔代数之间对应的同态φ∈Hom（GJ，G）是一个图集态射φ：QJ→ Q.命题5.2对每个F ∈ K（X），φ−1（MF）= Mf[F]。证据由于MF是G的超滤器，则φ−1（MF）是GJ的超滤器。对每个U∈AJ，QU∈φ−1（MF）i <$Qf−1（U）=φ（QU）∈MF，i<$F<$f −1（U），i <$f[F]<$U ， i <$QU∈Mf[F]. 同 样 地 ， 我 们 证 明 了 QU∈φ−1 （ MF ） i<$QU∈Mf[F]。这就足以证明这个命题，因为通过构造，Mf[F]是G的唯一超滤子，它包含f[F]的模态理论。Q我们通过显示商的超滤子来结束这一节-gebraG=G/ΛQ通常是模（超）滤波器MF=p[MF]，其中A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243257G → GG∈ G›−→∈−→p：p是正则投影。因此，是Vietoris布尔代数。命题5.3Ultr（G）= M。这个命题的证明使用了以下关于布尔代数的标准事实：引理5.4对于每个布尔代数A和A上的每个同余Λ，标准投影p：A → A/Λ在Ultr（A/Λ）和A的超滤子集合V之间导出双射对应，使得p−1（p [V]）=V。特别是，Ultr（A/Λ）={p [V] |V ∈ Ultr（A）且p−1（p [V]）= V}。让我们看看命题5.3：证据通过引理5.4，我们必须证明M ={p [V] |V∈Ultr（G）且p−1（p [V]）=V}。证明对G的每个超滤子V，如果p−1（p[V]）=V，则对某个F∈K（X），V=MF设存在G的超滤子V，使得对于每个F∈K（X），p−1（p[V]）=V且V/=MF只要证明存在a∈Vsucha∈/MF，对每个F∈K（X），若fi为0，则p（a）=0，因此0 ∈p−1（p [V]）= V，矛盾就足够了。我们考虑Stone空间XG，它是G的对偶.通过Stone对偶，XG的点是G的超滤子，XG的闭子集恰是集合a ={U∈Ultr（G）|a∈U}。让我们考虑集合M={MF|F∈K（X）}是X G的子集. 我们出现了V∈/M。我想知道为什么M是XG的一个封闭的基础，通过标准的紧性论证，V∈a且a∈ M=A，对于某些闭环，X G的子集a，即 对于每个F∈K（X），存在a ∈ V，使得a ∈ /MF，这就是我们想要的。所以让我们证明M是XG的闭子集。设K（X）为Vietoris空间，让我们考虑映射K：K（X）XG，由赋值FMF 对 每 个 FK（X）。由于K（X）是紧的，那么就足以证明K（X）是连续的，也就是说，对于每个a，K（X）的闭闭子集是K（X 通过对a的结构的归纳：对于基，QU和QU是K（X）的闭闭子集，对于X的每个闭子集U，并且K（X）={F ∈ K（X）|MF ∈ QU}<$−1（QU）={F ∈ K（X）|MF ∈QU}={F ∈ K（X）|QU ∈ MF}={F ∈ K（X）|QU ∈ MF}={F ∈ K（X）|F<$U}={F ∈ K（X）|FU/=}=QU=QU。归纳步骤是例行的。Q258A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243SSVL H LHS6结论、未来工作、未决问题在本文中，我们提出了一个Vietoris空间或powerdomain的一般概念的状态空间配备了一个代数的谓词。我们希望这在系统理论、泛余代数、代数逻辑、模态逻辑和格理论等领域有应用为了理解这一结构的重要性，还需要做更多的工作，其中一些工作我们将在下面进行概述。模态S-滤波器正如我们在引言中所提到的，我们的研究项目的目的是刻画支持模态的自扩张逻辑，并且我们提议使用第4节的构造来进行这种刻画，即说自扩张逻辑S支持经典模态当且仅当可以在（微分）-参照代数的范畴上构造Vietoris内函子V：那么-余代数可以表示为扩展代数签名的参照代数，并且它们将产生的逻辑将是S的经典模态扩展。这一构造的关键步骤是，对于每个S-参照代数H，存在环上的自由S-代数的模态S-滤子族。Q（）Q（）。 在斯通空间的情况下，这个家庭是由于布尔代数范畴中的精神分裂对象2的存在而构建的。一个自然的问题是，精神分裂症客体的存在是否表征了模态过滤器族可以被建设性地呈现的情形正如我们在2.2节中提到的，自延逻辑的对偶的一个特征是，它统一地解释了一类对偶，其中包括Stone和Priestley对偶（它们由一个精神分裂对象诱导），以及Jonsson-Tarski对偶（它们不是由一个精神分裂对象诱导的）。关于精神分裂对象的存在是否是模态S过滤器族被构造性地呈现的特征条件或充分条件的问题，也可以与比较克拉克和戴维的自然对偶和自扩张逻辑的对偶理论。其他模态扩展在本文中，我们集中在扩展的语言与模态签名组成的正常运营商Q和Q是相互关联的，就像在模态逻辑K。进一步的研究是将这种设置扩展到模态扩展，其中Q和Q不再像模态逻辑K中那样相关，而是独立的，或者更确切地说，它们彼此相关A. Kurz，A.Palmigiano/Electronic Notes in Theoretical Computer Science 106（2004）243259比如在直觉模态逻辑IK [10]中，等等。其他有趣的模态扩展将包括n元模态运算符，并且列表可以继续。这些情况中的每一种都对应于在参照代数上定义一个内函子。也许将其他超空间拓扑的定义扩展到参照代数上的内函子将是一个很好的起点，可以进行系统的研究，希望能为广泛的模态展开类提供一种通用的方法。有界格展开一 个 有 趣 的 研 究 方 向 是 关 于 与 Gehrke-Jo′nsontheo