Concurrent Heyting algebras: an algebraic semantics for an intuitionistic modal logic

We semantically define an intuitionistic bimodal logic through certain neighbourhood structures. We call these neighbourhood structures ic-frames. We propose a Hilbert-style axiomatisation and prove a completeness theorem with respect to the class of ic-frames. We introduce a class of algebras called concurrent Heyting algebras and prove an algebraic completeness theorem for this class. We show a categorical dual equivalence between a category whose objects are concurrent Heyting algebras and a category of Esakia spaces equipped with an ic-frame structure (see Section 6 for the corresponding morphisms). We present an alternative relational semantics for our logic through specific structures that mix Kripke-semantics and neighbourhood-semantics for the interpretation of the modal operators. We call these structures intuitionistic Kripke Neighbourhood frames (IKN-frames). We show that the category of IKN-frames with certain morphisms is isomorphic to the category of ic-frames.