Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic
Gianluigi Bellin, Valeria de Paiva, Eike Ritter · 2001
this paper. This calculus satises cut-elimination, as for instance shown (in a more complicated form) in [Wij90]. This calculus is dierent from what is usually taken as the basic constructive system K, as we do not assume the distribution of possibility (3) over disjunctions neither in its binary form 3(A _ B) ! (3A _ 3B) nor in its nullary form 3? ! ? The sequent calculus above corresponds to an axiomatic formulation given by axioms for intuitionistic logic, plus axioms: 2(A ! B) ! (2A ! 2B) 2(A ! B) ! (3A ! 3B) 2A3B ! 3(A B) together with rules for Modus Ponens and Necessitation: ` A ! B ` A ` B MP ` A ` 2A Nec Wijesekera proved a Craig interpolation theorem, one of the usual consequences of syntactic cut-elimination and produced Kripke, algebraic and topological semantics for a calculus very similar to the one above. The only dierence is that he does assume 3? ! ?. From our \\wish list" for logical systems only a natural deduction formulation and a categorical semantics are missing. These we proceed to discuss