Categorical and Algebraic Aspects of the Intuitionistic Modal Logic ${\mathrm{IEL}}^{-}$ and its predicate extensions

Abstract

The system of intuitionistic modal logic ${\mathbf{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 ${\mathbf{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 ${\mathbf{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}.

This paper is to appear in Journal of Logic and Computation. https://doi.org/10.1093/logcom/exaa082