Mathematical Structures in Computer Science

Special Issue: Modalities in Type Theory

A judgmental reconstruction of modal logic

a1 Department of Computer Science, Carnegie Mellon University, Pittsburgh PA 15213-3891, USA


We reconsider the foundations of modal logic, following Martin-Löf's methodology of distinguishing judgments from propositions. We give constructive meaning explanations for necessity and possibility, which yields a simple and uniform system of natural deduction for intuitionistic modal logic that does not exhibit anomalies found in other proposals. We also give a new presentation of lax logic and find that the lax modality is already expressible using possibility and necessity. Through a computational interpretation of proofs in modal logic we further obtain a new formulation of Moggi's monadic metalanguage.

(Received December 3 1999)
(Revised May 3 2000)


1 This work was partly supported by the National Science Foundation under grant CCR-9619832.