Intuitionistic Monotone Modal Logic: Proof Theory and Semantics

We study the recently introduced intuitionistic monotone modal logic IM.

We first provide a semantic characterisation for a family of natural extensions of IM in terms of constructive neighbourhood models.

We then present a calculus for IM and its extensions, obtained by adapting a structured calculus for the classical monotone modal logic M.

Based on the calculus, we prove some preliminary results for IM, including its decidability.

Our calculus also reveals an interesting analogy between constructive and intuitionistic variants of M and the corresponding variants of K, thereby further justifying IM as a faithful intuitionistic variant of M.