单调模态逻辑与余代数的联系和共代数概念的研究

PP →→理论计算机科学电子笔记106（2004）121-143www.elsevier.com/locate/entcs单调模态逻辑Helle Hvid Hansen1阿姆斯特丹大学逻辑、语言和计算研究所Plantage Muidergracht 24，NL克莱门斯·库普克2阿姆斯特丹大学逻辑、语言和计算研究所，Plantage Muidergracht 24，NL-1018 TV Amsterdam，Centrum voor Wiskunde en Informatica，P.O. 94079号信箱NL摘要本文主要有两个部分：首先，我们通过定义函子Up：SetSet和U pV：StoneStone，使得Up-和U pV-余代数分别对应于单调邻域框架和描述性一般单调框架，从而使单调模态逻辑与余代数的一般理论之间的联系更加精确。然后，我们研究的等价和单调互模拟的共代数概念之间的关系。特别是，我们表明，UpP-函子不保持弱拉回，利用UpP-互模拟的结果证明了一些单调模态逻辑的插值。保留字： 模态逻辑，余代数，互模拟，框架。1介绍余代数和模态逻辑之间有着明显的联系：内函子T的余代数可以被看作是抽象的动态系统或变迁系统，模态逻辑似乎是谈论的自然规范语言1电子邮件地址：hhhansen@science.uva.nl2电子邮件地址：ckupke@science.uva.nl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.028122H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）P2→→→ P P∧ →∧T参与T参与关于这些系统。从定义模态逻辑的共代数语义中可以预期的主要好处是以统一的方式获得不同类型模态逻辑的结果这里模态逻辑的类型由内函子T决定。 在这个方向上的研究已经进行了归纳定义的克里普克多项式函子（cf。[10，13，30]），但也适用于任意的内函子T（见[24，19，26，27]）。在正规模态逻辑中，模态算子Q是有限保交的（用Q表示Q（p（q）QpQq）。 单调模态逻辑通过将这种对Q的要求弱化为单调性（pq/QpQq）来生成正常模态逻辑这意味着克里普克框架不再构成一个自等价的语义;相反，（非正规）单调模态逻辑被解释在形式为（W，ν：W（ （ W）的单调邻域框架上，其中ν（w）是向上闭的。单调模态逻辑自然出现在开放系统和类似游戏的情况下的建模中（见[25，2，29]），其中代理人实现结果的能力被表示为Q。在这样的形式化中，QQQ（）不再需要有效，因为智能体可能需要使用不同的动作/策略来分别实现。然而，单调性显然是一个有效的原则。本文的一个目的是表明，单调模态逻辑属于上述概述的模态逻辑的共代数方法的范围。这将在第3节中实现，首先定义集上的函子UpP，使得UpP-余代数对应于单调邻域框架。 类似于对正常模态逻辑所做的（cf. [17]）我们还在Stoneof Stone空间范畴上定义了一个函子UpV，使得UpV-余代数范畴是单调布尔代数展开范畴BAM的对偶范畴，它构成了单调模态逻辑的代数语义。在第4节中，我们将研究UpP-余代数的不同等价概念，即Aczel和Mendler [1]定义的UpP-双相似性众所周知，如果函子T是弱拉回保持的，则T-双相似性和行为等价性是相同的（参见图1）。[31]）。然而，这两个概念对于我们的上P函子是不同的。这意味着Up不保持弱回调，尽管它与Gumm [11]中定义的弱回调保持过滤函子非常相似具有这种性质的函子的两个标准例子是Aczel和Mendler在[1]中定义的（-）3-函子和逆变函子。与自身组合的幂集函子（cf. [31]）。 然而，上P-函子的优点是，它的定义是通过将单调邻域框架转化为余代数设置而自然产生的。此外，我们认为，行为等价是更好的概念，研究P-余代数，因为它符合单调邻域框架之间的互模拟。H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）123P在第5节中，我们使用上互模拟来定义两个单调邻域框架的互模拟乘积，从而推广了Kripke框架的互模拟乘积（参见马克思[23]）。然后，我们使用互模拟积来证明某些单调模态逻辑的Craig插值，遵循[23]中关于正规模态逻辑中插值的证明思想。确认我们要感谢我们的同事提出了有益的意见。特别感谢Yde Venema主动与我们合作，并就本文件草稿提出了有益的意见。2预赛2.1拓扑矩阵由于我们要在Stone空间范畴上定义一个内函子，我们将简要地说明Stone空间的定义和著名的Stone对偶。对于一般拓扑学的基本概念，我们请读者参考[6]。给定一个拓扑空间X =（X，τ），我们用K（X），O（X）和Clp（X）分别表示闭子集，开子集和闭子集的集合.定义2.1（Stone）设X=（X，τ）是一个拓扑空间。则X是Stone空间，如果X是紧的，Hausdor空间，且有闭子集基。用Stone我们将Stone空间表示为对象，连续映射表示为它们之间的态射的范畴。定义2.2（Vietoris拓扑）设X=（X，τ）∈Stone.此外，我们定义了一个封闭U<$X，[3] U：={F∈K（X）|FU}，3U：={F ∈ K（X）|F<$U/= F <$}，设τ为K（X）上的拓扑，{[3] U|U∈Clp（X）}<${<$3 <$U|U∈Clp（X）}. 则VX：=（K（X），τ∈）称为X上的Vietoris空间。事实2.3（Vietoris函子）我们可以定义一个函子V：Stone→Stone，X ›→VX（f：X→ Y）›→f[ ]：VX→ VY有关Vietoris拓扑和Vietoris函子的信息，请读者参考[14]，第III.4节。事实2.4布尔代数的范畴BA和Stone是对偶等价的. 我们用C lp：Stoneop表示见证这一事实的著名函子。124H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）→◦◦∈∈BA和Sp：BA →Stoneop。2.2余代数预极限我们假定读者熟悉范畴论的基本概念作为标准参考，我们参考[20]。定义2.5（Coalg（T））设C是范畴，T：C → C是C上的内函子。则T -余代数或T -系是一对（X，γ：X其中X表示C的对象，γ表示C中的态射。箭头f：X1→ X2∈ C是两个T-余代数（X1，γ1）和（X2，γ2）之间的T -余代数态射，若γ2f=Tfγ1。T-余代数和T-余代数态射的范畴记为Coalg（T）.余代数与（正常）模态逻辑的Kripke语义密切相关。例2.6（余代数和模态逻辑）幂集函子P：Set→Set的余代数范畴Coalg（P）（平凡地）同构于Kripke框架范畴和它们之间的有界态射。一个稍微复杂一点的例子是Vietoris函数V的余代数范畴：Stone→Stone（cf.事实2.3），它对应于描述性一般Kripke框架的范畴[17]。系统的等价性有两个标准的概念：双相似性和行为等价性。然而，一个众所周知的事实是，对于函子T的大多数选择，这两个概念是一致的（即如果T保持弱回调）。现在我们将介绍这两个概念，稍后我们将看到，我们所定义的函子是函子的一个自然例子，其中双相似性强于行为等价性。定义2.7（T-互模拟）设T：Set→Set是函子，且（X1，γ1），（X2，γ2）∈Coalg（T）.如果存在函数γ：Z→TZ使得下图交换，则称关系Z<$X1×X2为T-互模拟X，π1Zπ2 X1 .一、2γ1。γγ2J.JJT X1，，TZX2T π1T π 2点x1X1和x2X2，使得对于T-互模拟Z，x1Zx2，称为T-互相似.定义2.8（行为等价）设T：Set→Set是函子，且（X1，γ1），（X2，γ2）∈Coalg（T）.则两个状态x1∈X1和x2∈X2H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）125→→L→LQ称为行为等价的，如果在Coalg（T）中存在一个（X，γ）和态射fi：（Xi，γi）→（X，γ）使得f1（x1）= f2（x2）. T-余代数（X1，γ1）和（X2，γ2）是行为等价的，如果存在T-余代数（X，γ）和满射fi：（Xi，γi）→（X，γ）∈Coalg（T）.2.3单调模态逻辑我们假设读者熟悉正规模态逻辑[4]，并参考[5，12]了解非正规模态逻辑。在这一小节中，我们将固定我们的模态设置，并介绍基本的语义结构。为了简单起见，我们将使用只有一个模态运算符的模态语言L。假设PROP是一组命题字母。然后由下式给出一组良构L-公式：：：=|p| ¬ϕ|ϕ∨ϕ|其中p∈ PROP。T、、→和Participare定义为常用缩写，而Q表示.一个-公式集Λ是单调模态逻辑，如果Λ包含所有的命题重言式，并且Λ在肯定前件规则（p，p）下是闭的q/q），一致替换和单调性（pq/QpQq）。最小的单调模态逻辑将被称为M，在第5节中，我们将考虑用下面方框中的一个或多个公理对M进行各种扩展。若M是一个-公式集，则M. M表示包含M的最小单调模态逻辑。NQT4QQp→ Qp不Qp→pPQ4’Qp→ QQpDQp→ Qp单调模态逻辑的语义是用单调邻域框架表示的我们将把这些结构和它们的态射一起定义为范畴MNF。定义2.9（MNF）单调（邻域）框架（对于语言L）是一对F =（W，ν），其中W是（世界的）非空集，ν：W→ P（P（W））是上闭的邻域函数，即，<$w∈W，<$X，Y∈ P（W）：X<$Y，X∈ν（w）<$Y∈ν（w）. 设F=（W，ν）和FJ=（WJ，νJ）是单调框架.函数f：W→WJ是从F到FJ的有界态射（记法：f：F→ FJ），如果（BM1）X∈ν（w）=<$f[X]∈νJ（f（w））.（BM2）XJ∈νJ（f（w））= <$X<$W：f [X]<$XJ&X∈v（w）.范畴MNF由单调邻域框架和有界态射组成。126H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）L∈在某些情况下，使用为逆像映射而不是像映射制定的有界态射的定义更方便，并且很容易证明（BM 1）和（BM 2）在以下条件下是等价的：对于所有XJ<$WJ，f−1 [XJ] ∈ν（x）i <$XJ∈νJ（f（x））。（一）类似于Kripke语义，邻域函数ν定义了一个映射，mν：P（W）→ P（W）：mν（X）={w∈W|X∈ v（w）}。（二）注意，当ν向上闭时，mν最后，单调模型是一个三元组（W，ν，V），其中（W，ν）是单调框架，V：PROP→ P（W）是命题字母的赋值。我们现在可以定义状态集[k]]，其中在单调模型M =（W，v，V）中，一个公式k为真，如下所示：[[]]=;[p]]=V（p）;[<$]]=W\[[]];[[]]=[[]][[]];[[Q]]=mν（[[]]）.2.4代数与对偶简要介绍单调模态逻辑代数对偶理论的主要概念和结果。除了固定符号，本节的目的是让读者了解代数对偶和3.2节的UpV-函子之间的关系。我们假设熟悉正规模态逻辑的代数对偶理论[32，8，9]，特别是描述性（Kripke）框架，带有算子的布尔代数和Stone表示[15，16]。关于单调模态逻辑的代数对偶的详细说明，我们参考[12]。2.4.1基本概念单调布尔代数展开（BAM）是代数结构A =（A，+，-，0，f），其中B1 A =（A，+，-，0）是布尔代数，f：A → A是单调映射，即，a ≤ b蕴涵f（a）≤ f（b），对所有的a，b ∈ A，其中a ≤ bi<$b = a +b. 因此，一个带有算子（BAO）的布尔代数可以看作是一个BAM，其中f是正规的和可加的。如果A1=（A1，+，-，0，f1）和A2=（A2，+，-，0，f2）是BAM s，则映射η：A1→A2是BAM-同态，如果η是布尔同态，并且对所有a1A1，η（f1（a1））=f2（η（a1））.我们定义BAMs和BAM-同态范畴为BAM。H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）127^^^^^{∈|∈}→^ ^您的位置：^^对于基本对偶，我们从单调框架F =（W，ν）出发，取全复代数F+=（P（W），m，v，m，v），得到一个bam. 在另一个方向，我们将使用石头二元性。给定一个BAMA，设SpA =（UfA，A）表示BlA的对偶Stone空间，其中UfA是BlA的超滤子集，A是A在Stone表示映射r：A→ P（UfA）下的像，定义为r（a）=a=uUfAau。回想一下，A是S p A的开闭基。本文定义了A+=（UfA，v+）的一个新的结 果式，其中v+（u）是由SpA的子集s的不同类型定义的，（clopen）A∈A：a∈v+（u） 我的f（a）∈u.（d）<$C∈K（SpA）：C∈ν+（u）我的f（a）∈u. （仲裁）XX∈v+（u） 我的 <$C∈K（SpA）：C<$X&C∈v+（u）.一般的单调框架是结构G =（W，ν，A），其中（W，ν）是单调框架，而A P（W）是一个子集的集合，这些子集包含W，有限并和映射m ν，并且在W，有限并和映射mν的补下是闭的。设G1=（W1，ν1，A1）和G2=（W2，ν2，A2）是两个一般单调框架，θ：W1W2是一个映射，则θ是G1和G2之间的一个一般框架有界态射，如果θ是单调框架（W1，ν1）和（ W2 ， ν2 ） 之 间 的 一 个 有 界 态 射 ， 且 θa 是 满足以下条件的函数：θ−1[a2]∈A1，对所有a2∈A2. GMF范畴由一般单调框架和一般框架有界态射组成。一般单调框架与BAM之间的基本对偶是通过下列构造得到的。 给定一个一般单调框架G =（W，ν，A），我们定义G的底层BAM为G=（A，v，\，v，mν）. 对于一个BAMA，A的遗传算法滤波器公式定义为：A=（A+，A）。他是个孩子。 本文用（A+）+定义了A的非正则扩张.一个巴姆的类K是正则的，如果K在取正则扩张下是闭的。单调模态逻辑Λ是正则的，如果由Λ定义的簇VΛ是正则的。2.4.2描述性一般框架在正规模态逻辑的代数对偶理论中，引入了描述（Kripke）框架，得到了与BAO[8，9]的范畴等价。我们将要定义的描述性的一般单调框架对于BAM范畴也有同样的作用。 更准确地说，描述性的一般单调框架s将被定义为具有Gisisiveiigi=（Gi）i。我们还记得，在一般单调框架G=（W，ν，A）中，容许集A可以作为W上拓扑τA的基。我们称W =（W，τA）为G的拓扑空间。设G =（W，ν，A）是一般单调框架.128H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）→P↑则称G是离散的，如果对任意的w，v∈W：w=vi∈A（w∈a惠v∈a）;紧的，如果对所有的AJ<$A，AJ/=A j如果AJ有有限个交集性质;紧如果对所有w∈W，所有C∈K（W）和所有X<$W，C∈ν（w）ia∈A（Ca→a∈ν（w）），X∈ν（w）i <$$>C∈K（W）（C<$XC&∈ν（w））.最后，如果G是离散的、紧的和紧的，则G是描述的为了简洁起见，我们将描述性一般单调框架简称为描述性单调框架。请注意，紧度条件是自然的，对于一般的单调性，需要求出G=（G）框架G，因为在一般超滤框架G中的邻域函数G将是这种形式。此外，其扩张性和紧性的条件与一般Kripke框架相同，因此我们有以下事实。事实2.10设G是一般单调框架。则G是扩张的紧的，且W是Stone空间，其中A构成闭根基。设DMF是具有一般框架有界态射的描述单调框架范畴。在[12]中，证明了下面的基本结果定理2.11范畴DMF和BAM是对偶等价的。3单调模态逻辑3.1作为上P-余代数的单调框架不难看出单调框架是余代数：单调框架是（X，ν：X22X）型的对。然而，不是每个22（-）-余代数对应于一个单调框架。本节的目的是定义一个函子UpP：Set→Set，使得UpP-余代数和单调框架相同。定义3.1（对象上的UPP）设X是一个集合，则集合UPPX被定义为X的子集的所有向上闭集的集合：上PX：={W <$PX |<$U1，U2∈ PX. （U1<$U2<$U1∈W）<$U2∈W}此外，对于任意的W X，我们定义其向上闭包（W）如下：↑（W）：={U ∈ PX |<$U J∈ W.U J<$U}。H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）129P↑ ◦2∈P→∈∈⊆∈ ∈P∈ P ∈ PP→ ∈P引理和定义3.2下面的映射定义了一个函子UpP：设置→设置：X›→向上 PX（f：X→Y）<$→上Pf：=（f−1）−1[]证据我们首先检查映射是否在态射上定义良好。令f：X Y是一个函数，假设W上X，那么我们必须证明V：=（f−1）−1 [W]向上Y。很容易看出V是Y，所以它表明V是向上闭合的。为了达到这个目的，U1V和一个U2Y使得U1U2乐队。 而V的定义，已知f−1[U1]W. 此外，我们知道f−1[U1]f−1[U2]，由于W是上闭的，我们得到f−1[U2] W。 但是，U V。UP满足函子律，这是不难看出的，并且直接从它是22（-）的子函子这一事实得出。Q在我们建立范畴MNF和Coalg（UpP）之间的明显联系之前，我们首先想更好地理解UpP如何作用于态射。引理3.3设f：X→Y且W∈UpPX. 然后上Pf（W）= ↑（{f [U J] |U J∈ W}）。证据 很容易检查。Q很明显，单调框架（W，ν）与UpP-余代数是相同的数学结构.此外，很容易证明有界态射是UpP-余代数态射，反之亦然.引理3.4范畴Coalg（UpP）和MNF同构。证据 关于详细的证明，我们请读者参阅[12]。Q在下文中，我们将不作任何区分的概念P-余代数和单调框架之间的上，余代数态射和有界态射。注3.5有人可能会问，为什么我们不把22（-）-余代数范畴看作单调框架的余代数类似物。事实上，这在对象上很有效：给定一个22（-）-余代数（W，ν：W22W），对应的单调框架将是对（W，νJ：=ν）。 态射然而，Coalg（22（-））的范畴将不再对应于有界的态射130H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）→→3.2作为UpV-余代数的在[17]中，有人认为函子T：Stone→Stone的余代数从正常模态逻辑的角度来看是有趣的。这在单调模态逻辑的情况下也将被证明是真的。我们将首先定义函子UpV：Stone Stone，然后证明描述单调框架范畴同构于范畴Coalg（UpV）。作为推论，我们得到范畴Coalg（UpV）和BAM之间的对偶，BAM是BAM s的一个表示作为函子的代数和最终UpV-余代数的存在性定义3.6（UpVon objects）设X =（X，τ）∈Stone，且U<$K（X），则U是上闭的（upc），如果对所有F，FJ∈K（X）使得F<$FJ，F∈U蕴涵FJ∈U。称U为[3]-闭的，如果对所有闭集F，F属于U，且对所有闭集F，a∈U，a∈F.我们定义UpV（X，τ）：={U∈K（VX）|U是upc且[3]-闭}。注3.7所有集合都是[3]-闭的要求是一般单调框架紧性条件 选择术语[3]-闭的是因为集合U是[3]-闭的，且对于所有F∈ −U，存在a∈Clp（X）使得F∈ [3] a且U∈ [3] a = n。很明显，UpVX等于 VVX。因此，如果我们能证明UpV X是VVX中的闭子集，则UpV X是具有相对拓扑的Stone空间。引理3.8设X =（X，τ）∈ Stone. 则UpVX是VVX中的闭子集。证据证明只使用一般拓扑学的标准技术，由于篇幅有限，这里不得不省略。Q定义3.9（U pV-函子）映射U pV：Stone Stone定义如下。对于Stone空间X =（X，τ），U pVX =（{U∈K（VX）|U是upc且[3]-闭}，τJ）其中τJ是由VVX上的拓扑诱导的相对拓扑。对于连续函数f：X →Y，UpVf：UpVX → UpV YU<$→UpVf（U）=（f−1）−1[U]= 22f（U）={D ∈ K（Y）|f −1 [D] ∈ U}从引理3.8可以得出，UpV在物体上有很好的定义。接下来的两个引理表明UpVf也是在态射上定义良好的。H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）1313Z（Z）设ak∈Clp（Y），使得b=MK 其中Mk∈ {[3]，<$3 <$}.是--类似的方式。注意，如果b∈Clp（VY），则存在合适的闭根族因为[3]分布在满足我们得到：[3]b=[3]第一章MK MKAK。 因此它分布在连接上，此集合的形式我们必须证明i=1[]aia. 所以总结M引理3.10设f：X→ Y∈Stone，其中 X=（X，τX），Y=（Y，τY），且U∈ U pV X. 则UpVf（U）∈ UpVY.证据U pVf（U）是upc很容易检验。它仍然表明U pVf（U）=（f−1）−1 [U]是[ ]-闭的。证明使用了标准的紧凑性参数，由于缺少空间而被省略Q引理3.11函数U pVf：U pV X → U pV Y是连续的。证据 出于完整性的原因，我们提供了相当技术性的证明。建议对技术细节不感兴趣的读者跳过它。它表明（UpVf）−1[[3]b]和（UpVf）−1[3b]对于一个ar-n是封闭的，VY的二进制闭子集b我们只考虑这样一种情况我们处理的是一个形式为[3]b的集合。2003年的病例可以在一个nik=1i=1我我我k=1i=1我 我表来查看形式为mJ的集合bMiai（Mi∈ {[3]，<$3 <$}）. 因为⟨3⟩i=1M3∪ ⟨3⟩Z：=（UpVf）−1[3]Mi=1[3]ai3a=（U pVf）−1[{U∈ U pV Y |F∈U。（i.Fai）或Fa}]对任意ai，a∈Clp（Y）是闭闭的.首先，我们对任何i∈ {1，...，m}一个集合Ui∈ {U∈ U pV Y |F∈U。（i.Fai）或Fa/=}和一个集合Fi∈Ui使得Fiai和Fia=.我们可以假设这是可能的，因为假设对于一个iJ，不存在这样的UiJ和FiJ。然后{U∈ U pV Y |F∈U。（i.Fai）或Fa/=}={U∈ U pV Y |F ∈ U。（i.i iJFai）orFa/ =}我们就可以忘了AIJ 我们现在主张，={V ∈ U pV X |G ∈ V。（i.f [G] ai）or f [G] a/=}=[3][3]f−1[ai]<$$>3<$f−1[a]i=1最后一个集合显然是UpV X的闭闭尾子集这还有待证明（A）确实是正确的。等式的第二部分很容易检验. 所以我们将集中在第二部分。设V∈{V∈ U pVX|G∈V。（f [G] ai）或f [G] ai = n}。我们必须证明U pVf [V] ∈ {U∈ U pV Y |F∈U。（i.Fai）或Fa/=}。132H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）→33∈{|∈设FJ∈UpVf[V]，即存在G∈V使得f[G]<$FJ.情况：f [G] a/=。那么很明显F J<$a/=<$。Case：f[G]ai for somei. 假设对于所有i∈{1， . . . ，m}有一个FJ/ai，且FJa=. WenowdefineeF<$：=FJFi. 当U i向上闭合时，F<$∈Ui。FurF<$/aiJfor所有iJ∈{1， . . . ，m}（其他wi s eFJaiJ）。因为F<$∈Uiwethereformethave你好但这意味着FJa=Fia，并且weharrived一个矛盾。Q既然我们已经定义了函子UpV，我们就可以证明本节的主要结果了。定理3.12描述单调框架范畴DMF与范畴Coalg（UpV）同构.证据我们只定义了函子C oa：DMF→Coalg（U pV）和D mf：Coalg（UpV）DMF，它们诱导了范畴之间的同构。我们有同构的证明仅仅是列出定义，并被省略。我们首先定义函子Coa：Coa（W，ν，A）：=（W，ν：W→ UpV W）Coaf：=f其中W =（W，τA）且ν（w）：={F<$W|F∈K（W）和F∈ν（w）}。 映射ν定义良好，因为（W，ν，A）上的紧性条件确保ν（w）是[ ]-闭的。事实2.10告诉我们函子在对象上是有明确定义的。现在让我们定义Dmf：Dmf（W，ν）：=（W，ν，Clp（W））Dmff：=f其中v（w）=UWFv（w）.F联合事实2.10再次告诉我们 ， （ W ， ν ， Clp （ W ） ） 是 离 散 的 和 紧 的 。[1][2][3][4][5][5][6][7][8][9][9][9][10][10][10][10][11][10][11][10][11][12][10][11][11][12][11][12][11][10][11][12][12][13][11][12][11][12][13][12][14][14][15][15][16][17][11][17][19][10][11][19][10][11][10][11][12][19][10][11][11][11][12][19][11][1此外，它是直接证明，一个有界态射fDMF也是一个UpV-余代数态射，反之亦然，这是一个在定义Coa和Dmf时都需要的事实。Q为了使这一节圆满，我们陈述这个定理的一些直接结果。推论3.13 BAM范畴和Coalg（U pV）范畴是对偶等价的。证据直接遵循BAM和DMF之间的二元性（参见定理2.11）和定理3.12。QH.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）133PCoroll3.14R是函子L：BA→BA_n，使得Al_g（L）_n= BA_M.我的律师。 一个关于Coalg（U pV）opn= B AM和Stone对偶的直接等式.Q推论3.15范畴Coalg（U pV）有余自由余代数，特别是最终的U pV-余代数存在。证据对偶的结果和从BAM到BA的遗忘函子有左伴随的事实。Q4等值概念在第3节中，我们建立了UpP-余代数和单调框架之间的等价性，现在我们将研究与单调模态逻辑的这两个观点相关的各种等价概念之间的关系。在4.1小节中，我们将证明共代数上互模拟严格强于单调互模拟的逻辑概念（定义4.1），在4.2小节中，主要结果表明行为等价于单调互相似。这些结果使我们能够得出结论，上P函子不保持弱回调（推论4.10）。4.1互模拟模态逻辑中模型等价的中心概念是双模拟。Kripke模型的互模拟由vanBentham在[3]中引入，其中还发现了著名的特征化结果，该结果表明（正常）模态逻辑是一阶逻辑的（Kripke）互模拟不变片段。对于单调（邻域）模型，Pauly [28]已经提出了单调互模拟最后一个结果也包含在[12]中，它是单调互模拟是模型等价的正确逻辑概念的有力论据。134H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）∈∈我我→P定义4.1（单调互模拟）设（X1，ν1），（X2，ν2）∈ MNF. 一个非空关系Z<$X1×X2是（X1，ν1）和（X2，ν2）之间的单调互模拟，如果对所有的x1X1和x2X2使得x1Zx2，满足以下两个条件。（第四）<$C1∈ ν1（ x1）. <$C2∈ ν2（ x2）使得（<$c2∈ C2. c1∈C1：c1Zc2）。（背面）< $C2∈ ν2（ x2）. <$C1∈ ν1（x1）使得（<$c1∈ C1. c2∈C2：c1Zc2）。若dom（Z）=X1，ran（Z）=X2，则称Z为完全单调互模拟.两个单调框架（X1，ν1）和（X2，ν2）称为（完全）单调双相似，如果它们之间存在（完全）单调互模拟，两个状态x1∈X1和x2∈X2称为（完全）单调双相似状态，如果在（X1，ν1）和（X2，ν2）之间存在（完全）单调互模拟Z，使得x1Zx2.对于上P-函子，上P-互模拟等于以下内容.定义4.2（UpP-互模拟）设（X1，ν1），（X2，ν2）∈Coalg（UpP）.非空关系Z<$X1×X2是（X1，ν1）和（X2，ν2）之间的UpP互模拟，如果存在函数μ：Z→UpPZ使得：ν1<$π1=UpPπ1<$μ和ν2<$π2=UpPπ2<$μ。X，π1Zπ2X1ν1 J向上Pπ.2µ。ν 2.JUpPπ J上PX1，，1上PZ2上PX2我们说（X1，ν1）和（X2，ν2）通过（Z，μ）是上P-双相似的，如果μ使上图可换。若πi：Z→Xi，i∈ {1， 2}，即投影是满射的，则称Z为完全UpP-互模拟.因此，为了证明Z是两个UpP-余代数（X1，ν1）和（X2，ν2）之间的UpP-互模拟，我们必须能够赋予Z一个合模结构μ，使得投影πi：（Z，μ）→（Xi，νi）是有界态射。对于i∈ {1， 2}，πi是有界态射当且仅当Ci （Ci∈νi（xi）π−1 [Ci] ∈μ（x1，x2））。（三）或者等价地，对于所有的Y<$Z，Ci<$Xi，（BM 1）Y∈μ（x1，x2）蕴涵πi[Y]∈νi（xi），（BM 2）Ci∈νi（xi）蕴涵π−1[Ci]∈μ（x1，x2）。这些条件为我们提供了具体的约束，除了向上闭包之外，μ：ZUpZ还必须满足这些约束条件（BM 1）告诉我们什么时候可以给μ（x1，x2）加上一些Y<$Z，即当π1[Y] ∈ν1（x1）H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）135（四）∈ ∈ {}且π2[Y]∈ν2（x2）.这是（BM1）产生的最大μ。另一方面，（BM 2）告诉我们什么时候必须给μ（x1，x2）加上一些Y，即当πi−1[Ci] Y对一些Ciνi（xi）和一些i 1，2，从而产生最小的μ。现在我们给出一个正式的定义。定义4.3（μs和μl）设（X1，ν1），（X2，ν2）∈Coalg（UpP），且π/=给出Z<$X1×X2 然后我们定义μs，μl：Z→UpPZ如下。Y∈μs（x1，x2）i∈μ sC1∈ν1（x1）. π1−1[C1]<$Y或<$C2∈ν2（x2）。π2−1[C2]Y。 Y∈μl（x1，x2）我的π1 [Y] ∈ν1（x1）和π2 [Y] ∈ν2（x2）。（五）从定义中可以清楚地看出，μs和μl都是向上封闭的，对于满足（3）的任何μ，我们有μs（x1，x2）<$μ（x1，x2）<$μl（x1，x2）。当然，不能保证μs和μl本身满足两个有界态射条件。下一个命题告诉我们，案子命题4.4设（X1，ν1），（X2，ν2）∈ Coalg（UpP），且n/= Z <$X1× X2.则Z是（ X1，ν1）和（X2，ν2）之间的Up P -互模拟当且仅当Z对所有（x1，x2）∈Z满足以下两个条件。（向上P-向前）<$C1∈ν1（x1）. <$C2∈ν2（x2）使得c2∈ C2。C1∈ C1s. t. c1Zc2和Z−1 [C2]<$C1∈ ν1（x1）。（上P-后）<$C2∈ν2（x2）. <$C1∈ν1（x1）使得c1∈C1。C2∈C2s.t.c1Zc2和Z [C1]<$C2∈ ν2（x2）.证据我们只是勾勒出证据。对于从左到右的方向，可以直接检查（UpP-forth）和（UpP-back）条件是否对UpP-互模拟成立。对于从右到左的方向，可以证明当Z满足（UpP-forth）和（UpP-back）条件时，则（X1，ν1）和（X2，ν2）通过（Z，μs）和（Z，μl）都是UpP-双相似的Q由于上述特征，下一个推论是直接的。推论4.5如果Z是上P-互模拟，则Z也是单调互模拟.136H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）正如我们在本小节开始时所宣布的，UP-互模拟是单调互模拟的严格子集。下面的例子说明了这一点。H.H. 汉森角，澳-地Kupke/Electronic Notes in Theoretical Computer Science 106（2004）137例4.6考虑单调框架F 1=（{s1，t1，u1，v1}，v1），其中v1（s1）= ↑（{{t1}，{u1，v1}}），v1（u1）= ↑（{{u1}}）且v1（t1）= v1（v1）=;F2=（{s2，t2}，v2），其中v2（s2）= ↑（{{t2}}）且v2（t2）=。则Z ={（s1，s2），（t1，t2），（v1，t2）}是单调互模拟。事实上，Z是F1和F2上的最大单调互模拟。但Z不满足（UpP-forth），对相邻的hourhod{u1，v1}∈ν1（s1），sinceZ−1[{t2}]<${u1，v1}={v1}∈/ν1（s1）. 这个问题将发生在任何连接s1和s2的单调互模拟中，因为u1与F2中的任何状态都不是单调互相似的，因此s1和s2是单调互相似的，但不是UpP-互相似的。对于单调互模拟Z，如果Y1∈ν1（x1），Y1/ν1（Z），且对于X1<$Y1，X1∈/ν1（x1），对于n y Y 2，nZ−1[Y2]<$Y1<$Y1，ndheZ−1[Y2]<$Y1∈/ν1（x1）。Th是如果我们考虑完全单调互模拟，则可以消除故障我们离开这是对下面引理的简单证明。引理4.7设（X1，ν1），（X2，ν2）∈Coalg（UpP），且Z<$X1×X2. 如果Z是完全单调互模拟，则Z是上P-互模拟。下一个例子表明，向上P-互模拟不需要是完全的。例4.8设F1 =（{s1，t1，u1}，ν1）且F2 =（{s2，t2}），其中νi（si）=↑（{{ti}}），νi（ti）=π，其中i∈ {1， 2}，且ν1（u1）=↑（{{u1}}）.则Z={（s1，s2），（t1，t2）}是（最大）上P-互模拟，但Z显然不是满的。4.2行为等价事实证明，行为等价的概念更好地与互模拟的框架理论概念联系在一起，我们现在将证明两个状态是单调互相似的当且仅当它们是行为等价的（定理4.9）。回想一下定义2.8，对于两个UpP-余代数（X1，ν1）和（X2，ν2），两个状态s1∈X1和s2∈X2是行为等价的，如果它们可以通过某个UpP-余代数（Y，δ）中的两个有界态射fi：Xi→Y，i∈ {1， 2}来行为等价在X1×X2上导出一个关系，pb（f1，f2）={（x1，x2）∈ X1× X2|f1（x1）= f2（x2）}，众所周知，（pb（f1，f2），π1，π2）是集合中f1和f2的拉回，π1<$f1=π2<$f2. 它直接表明pb（f1，f2）-关系实际上是一个单调互模拟。因此，状态之间的关系意味着单调双相似性。本节的主要结果表明，另一个含义也成立138H.H. 汉森角，澳-地Kupke/Electronic Notes