 This section, at present, offers only a glimpse of intuitionistic modal logic. Any classical  modal logic  has an intuitionistic companion defined by replacing the underlying classical propositional or predicate logic by the corresponding intuitionistic propositional or predicate logic. Simpson [1994] and Plotkin and Stirling [1986] provide a general framework for intuitionistic modal logics which is adaptable to a multitude of uses.