Fitch-Style Modal Lambda Calculi

TL;DR

This paper develops Fitch-style modal lambda calculi with good computational properties for various intuitionistic modal logics, providing semantics in cartesian closed categories and simplifying the calculus for intuitionistic S4.

Contribution

It introduces a Fitch-style approach to modal lambda calculi with categorical semantics, including a simpler calculus for intuitionistic S4 and extensions to tense logic.

Findings

Calculi have good computational properties for intuitionistic modal logics

Semantics are given in cartesian closed categories with adjunctions

A simpler calculus for intuitionistic S4 is presented

Abstract

Fitch-style modal deduction, in which modalities are eliminated by opening a subordinate proof, and introduced by shutting one, were investigated in the 1990s as a basis for lambda calculi. We show that such calculi have good computational properties for a variety of intuitionistic modal logics. Semantics are given in cartesian closed categories equipped with an adjunction of endofunctors, with the necessity modality interpreted by the right adjoint. Where this functor is an idempotent comonad, a coherence result on the semantics allows us to present a calculus for intuitionistic S4 that is simpler than others in the literature. We show the calculi can be extended \`{a} la tense logic with the left adjoint of necessity, and are then complete for the categorical semantics.