On Constructive Modality

Abstract

Fitch [8] first developed an intuitionistic modal logic based on Heyting’s intuitionistic logic. No special attention to this system was paid by those researchers working on intuitionism nor by those on modal logic. This is probably because Fitch gave only a proof theory, and because it was before the appearance of the so-called Kripke semantics for modal and intuitionistic logics. Recently, there has been a considerable interest in this topic as shown in the works of Ono [18], Gabbay [10], Ewald [7], Font [9], Božic and Dosen [5], Dosen [6].