Intuitionistic monotone modal logic via translation

We introduce a monotone modal analogue of the intuitionistic (normal) modal logic IK using a translation into a suitable (intuitionistic) first-order logic. We axiomatise the logic and give a semantics by means of intuitionistic neighbourhood models, which contain neighbourhoods whose value can change when moving along the intuitionistic accessibility relation. We compare the resulting logic with other intuitionistic monotone modal logics and show how it can be embedded into a multimodal version of IK.