file.pdf (251.49 kB)
0/0

A Judgmental Reconstruction of Modal Logic

Download (251.49 kB)
journal contribution
posted on 01.01.1976 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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1976

Exports

Exports