Under Lock and Key: A Proof System for a Multimodal Logic

TL;DR

This paper introduces a proof system for a multimodal logic with a mode theory framework, extending to a lambda calculus to connect logic and computation through Curry-Howard correspondence.

Contribution

It develops a novel proof system for multimodal logic based on a 2-category mode theory, integrating it with lambda calculus for computational interpretation.

Findings

Defines a mode theory as a 2-category for multimodal logic

Extends the logic to a lambda calculus with Curry-Howard correspondence

Provides a formal proof system for multimodal logic

Abstract

We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category. The logic is extended to a lambda calculus, establishing a Curry-Howard correspondence.