Categorical and Algebraic Aspects of the Intuitionistic Modal Logic\n \IEL^- and its predicate extensions

2020/05/03 by Daniel Rogozin, Rogozin, Daniel
Computer Science · #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2005.01135

openalex publication_date 2020/05/03 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28

Abstract

The system of intuitionistic modal logic bf IEL^- was proposed by S.\nArtemov and T. Protopopescu as the intuitionistic version of belief logic\n citeArtemov. We construct the modal lambda calculus which is Curry-Howard\nisomorphic to bf IEL^- as the type-theoretical representation of\napplicative computation widely known in functional programming. We also provide\na categorical interpretation of this modal lambda calculus considering\ncoalgebras associated with a monoidal functor on a cartesian closed category.\n Finally, we study Heyting algebras and locales with corresponding operators.\nSuch operators are used in point-free topology as well. We study compelete\nKripke-Joyal-style semantics for predicate extensions of bf IEL^- and\nrelated logics using Dedekind-MacNeille completions and modal cover systems\nintroduced by Goldblatt citegoldblatt2011cover. The paper extends the\nconference paper published in the LFCS'20 volume citerogozin2020modal.\n

Citations

• Cover Schemes, Frame-Valued Sets and Their Potential Uses in Spacetime Physics
• The Many Worlds of Modal \λ-calculi: I. Curry-Howard for\n Necessity, Possibility and Time
• Calculi for Intuitionistic Normal Modal Logic

Related

• Curry-Howard-Lambek Correspondence for Intuitionistic Belief
• Intuitionistic logic, dual intuitionistic logic, and modality
• A Coalgebraic Semantics for Intuitionistic Modal Logic
• Lax Modal Lambda Calculi
• Base-extension Semantics for Intuitionistic Modal Logics