Dual-Context Calculi for Modal Logic

TL;DR

This paper introduces dual-context natural deduction and lambda calculi for various modal logics, establishing their properties and semantics, and connecting them to existing Hilbert systems.

Contribution

It develops dual-context calculi for modal logic fragments, analyzes their metatheory, and provides categorical semantics linking modalities to functors.

Findings

Calculi are confluent and strongly normalizing.

Calculi coincide with Hilbert systems up to provability.

Categorical semantics interprets modality as a product-preserving functor.

Abstract

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.