Models for normal intuitionistic modal logics

Abstract

Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal system K based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for an investigation of intuitionistic analogues of systems stronger than K. A brief survey is given of the existing literature on intuitionistic modal logic.