Kavvos, G. A. - Dual-Context Calculi for Modal Logic

lmcs:4740 - Logical Methods in Computer Science, August 19, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:10)2020
Dual-Context Calculi for Modal Logic

Authors: Kavvos, G. A.

We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor.

Volume: Volume 16, Issue 3
Published on: August 19, 2020
Submitted on: August 7, 2018
Keywords: Computer Science - Logic in Computer Science,F.4.1


Consultation statistics

This page has been seen 326 times.
This article's PDF has been downloaded 287 times.