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.

翻译：我们提出了一种多模态逻辑的证明系统，该工作基于此前在多模态马丁-洛夫类型论上的研究。模态、模态词及其间的蕴涵关系以模态理论的形式给出，即一种小型2-范畴。该逻辑被扩展为一种lambda演算，从而建立了柯里-霍华德对应。