Intuitionistic Master Modality

We present a cyclic sequent calculus for intuitionistic modal logic with the master
modality. Formulas of the logic are evaluated over bi-relational Kripke models with
three different frame conditions: functional frames, ‘triangle’ confluent frames, and
arbitrary frames. It is shown that the calculus is sound and complete for all three
classes of models. This, in particular, proves that intuitionistic modal logic with the
master modality cannot distinguish between arbitrary models and functional models.
Soundness is established by a standard argument while completeness is proven via
a detour to non-wellfounded proofs, using a proof-search argument that draws on
analyticity of the calculus. The framework is robust in the sense that it can be
naturally adapted to account for various frame conditions, such as serial models,
reflexive models or S4-models, as well as for a polymodal extension that can be
interpreted as intuitionistic common knowledge.