论文标题
直觉模态逻辑$ \ operatatorName {iel}^{ - } $的分类和代数方面及其谓词扩展
Categorical and Algebraic Aspects of the Intuitionistic Modal Logic $\operatorname{IEL}^{-}$ and its predicate extensions
论文作者
论文摘要
S. Artemov和T. protopopescu提出了直觉模态逻辑$ {\ bf iel}^{ - } $的系统，作为信念逻辑的直觉版本。我们构建了咖喱豆曲线的模态lambda conculus，它是$ {\ bf iel}^{ - } $作为函数编程中广泛已知的应用计算的类型理论表示。我们还提供了这种模态lambda微积分的分类解释，考虑到与笛卡尔封闭类别上与单型函数相关的山地。 最后，我们使用相应的操作员研究Heyting代数和地区。此类操作员也用于无点拓扑。我们研究了使用Dedekind-Macneille完成和Modal覆盖系统，研究;该论文扩展了在LFCS'20卷\ cite {rogozin2020modal}中发表的会议论文。
The system of intuitionistic modal logic ${\bf IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic \cite{Artemov}. We construct the modal lambda calculus which is Curry-Howard isomorphic to ${\bf IEL}^{-}$ as the type-theoretical representation of applicative computation widely known in functional programming. We also provide a categorical interpretation of this modal lambda calculus considering coalgebras associated with a monoidal functor on a cartesian closed category. Finally, we study Heyting algebras and locales with corresponding operators. Such operators are used in point-free topology as well. We study compelete Kripke-Joyal-style semantics for predicate extensions of ${\bf IEL}^{-}$ and related logics using Dedekind-MacNeille completions and modal cover systems introduced by Goldblatt \cite{goldblatt2011cover}. The paper extends the conference paper published in the LFCS'20 volume \cite{rogozin2020modal}.
