Intuitionistic modal logics: a minimal setting
Philippe Balbiani, Çigdem Gencer
TL;DR
This paper develops a minimal yet normal intuitionistic modal logic ${\bf L}_{\min}$ strictly contained in ${\bf IK}$ by adopting a novel truth condition for ${\lozenge}$ within forward/backward confluent frame semantics. It provides a comprehensive axiomatization, establishes soundness and completeness via canonical-frame constructions, and proves decidability through filtration and the finite-frame property. The work positions ${\bf L}_{\min}$ relative to classical intuitionistic modal logics (e.g., ${\bf IK}$, ${\bf WK}$, ${\bf CK}$) and related definability results, yielding a solid framework for minimality and modular extensions (e.g., ${\bf L}_{\mathbf{fc}}$, ${\bf L}_{\mathbf{bc}}$, ${\bf L}_{\mathbf{dc}}$, and their combinations). It also develops a robust theory of L-theories and canonical models that underpins the completeness theorems and clarifies the landscape of decidable fragments and open questions on modal definability and fragment axiomatizability.
Abstract
We introduce an intuitionistic modal logic strictly contained in the intuitionistic modal logic IK and being an appropriate candidate for the title of ``minimal normal intuitionistic modal logic''.