On Proof Equivalence for Constructive Modal Logic
Università Roma Tre
Abstract: In this talk we discuss various notions of proof equivalence for constructive modal logics.
For this purpose, we first illustrate the correspondence between winning innocent strategies for games on arenas, lambda calculus, and combinatorial proofs in propositional intuitionistic logic. After showing how to extend the syntax of combinatorial proofs to represent proofs in constructive modal logics, we use this correspondence to identify the additional conditions required to ensure a full-complete correspondence between winning innocent strategies and sequent calculus derivations for constructive modal logic.
We conclude by comparing the notion of proof equivalence enforced by combinatorial proofs, modal lambda-calculus and winning innocent strategies for these logics.