A Judgmental Reconstruction of Modal Logic
journal contributionposted on 01.01.1976, 00:00 by Frank Pfenning, Rowan Davies
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.