An intuitionistic modal logic should be a logic that is both intuitionistic at its core, but is also equipped with modalities, usually denoted .
It is not so easy to tell what such a logic should look like, and many different variants have been studied.
In his PhD thesis [Simpson 1994], Alex Simpson proposed six criteria that an intuitionistic modal logic should satisfy:
The last condition is not formal. In Simpson's thesis it is interpreted as follows. Suppose we have a Kripke semantics given by a satisfaction relation . We can express the definition of that clause in a first-order logic, obtaining a sentence . Then, should be a theorem iff is a theorem of intuitionistic first-order logic.
Simpson, Alex K. ‘The Proof Theory and Semantics of Intuitionistic Modal Logic’. PhD Thesis, The University of Edinburgh, 1994. http://hdl.handle.net/1842/407.
@phdthesis{simpson_1994,
type = {{PhD} {Thesis}},
title = {The {Proof} {Theory} and {Semantics} of {Intuitionistic} {Modal} {Logic}},
url = {http://hdl.handle.net/1842/407},
school = {The University of Edinburgh},
author = {Simpson, Alex K.},
year = {1994},
}