The relation between intuitionistic and classical modal logics

Intuitionistic prepositional logic Int and its extensions, known as intermediate or superintuitionistic logics, in many respects can be regarded as just fragments of classical modal logics containing S4. The main aim of this paper is to construct a similar correspondence between in-termediate logics augmented with modal operators - we call them intuitionistic modal logics - and classical polymodal logics. We study the class of intuitionistic polymodal logics in which modal operators satisfy only the congruence rules and so may be treated as various sorts of □ and ◇. © 1997 Plenum Publishing Corporation.