Skip to main content

Dual−Context Calculi for Modal Logic

G. A. Kavvos

Abstract

We show how to derive natural deduction systems for the necessity fragment of various constructive modal logics by exploiting a pattern found in sequent calculi. The resulting systems are dual-context systems, in the style pioneered by Girard, Barber, Plotkin, Pfenning, Davies, and others. This amounts to a full extension of the Curry-Howard-Lambek correspondence to the necessity fragments of a constructive variant of the modal logics \textsfK, \textsfK4, \textsfGL, \textsfT, and \textsfS4. We investigate the metatheory of these calculi, as well as their categorical semantics. Finally, we speculate on their computational interpretation.

Book Title
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Year
2017