Categorical and Kripke Semantics for Constructive S4 Modal Logic
Categorical and Kripke Semantics for Constructive S4 Modal Logic
复制标题
构造性 S4 模态逻辑的分类语义和 Kripke 语义
DOI：
10.1007/3-540-44802-0_21
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Eike Ritter
中科院分区：
文献类型：
--
作者：
N. Alechina;M. Mendler;Valeria C V de Paiva;Eike Ritter
我们考虑了两个受计算激励的构造性模态逻辑系统。它们的形态允许几种计算解释，并被用来捕捉内涵特征，如计算概念、约束、并发性等。到目前为止，这两个系统主要是从类型理论和范畴理论的角度进行研究，但类似系统的Klipke模型是独立研究的。在这里，我们将这些线索结合在一起，并证明了对偶结果，这些结果表明了如何将克里普克模型与代数模型联系起来，并进而将这些模型转化为这些逻辑的适当范畴模型。
We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.