Canonicity of Proofs in Constructive Modal Logic

TL;DR

This paper develops a new lambda-calculus for constructive modal logic, establishing normalization, confluence, and a correspondence between normal forms and winning strategies, thus advancing the Curry-Howard correspondence in this domain.

Contribution

It introduces an enriched lambda-calculus with new reduction rules and a focused proof system, bridging proof equivalences and winning strategies in constructive modal logic.

Findings

Proved normalization and confluence of the new calculus

Established a one-to-one correspondence between normal forms and strategies

Provided a unique proof representation for each normal form

Abstract

In this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We define a new lambda-calculus for a minimal constructive modal logic by enriching the calculus from the literature with additional reduction rules and we prove normalization and confluence for our calculus. We then provide a typing system in the style of focused proof systems allowing us to provide a unique proof for each term in normal form, and we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies.