查看文章

The benefits of the extended Curry-Howard Correspondence relating the simply typed lambda-calculus to proofs of intuitionistic propositional logic and to appropriate classes of categories are widely known. In this note we pursue an analogous correspondence for a basic intuitionistic (or constructive) modal logic IKwith both necessity (2) and possibility (3) operators. Similar work for intuitionistic S4 (IS4) has appeared in [BdP00, AMPR01, GdPR98].

This is a natural logic to consider, if one is determined to push the frontiers of the Curry-Howard Isomorphism, as far as they will go. Modal system K is less symmetric than S4 as far as the modality rules are concerned. Modal S4 has introduction and eliminatin rules for both necessity and possibility, whereas modal K has only one rule for necessity and one rule for possibility. But modal K (to be precise, a multimodal modal K) is also a solution to a question first posed by McCarthy [McC93] and expounded on by Buvac, Buvac and Mason in [BBM95], when discussing future work: