A Judgmental Reconstruction of Modal Logic
journal contributionposted on 01.01.1976 by Frank Pfenning, Rowan Davies
Any type of content formally published in an academic journal, usually following a peer-review process.
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.