Curry-Howard-Lambek Correspondence for Intuitionistic Belief

Abstract

This paper introduces a natural deduction calculus for intuitionistic logic of belief ${\mathsf{IEL}}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational semantics for deductions in ${\mathsf{IEL}}^{-}$. By using that interpretation, it is also proved that ${\mathsf{IEL}}^{-}$ has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in ${\mathsf{IEL}}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.

Submitted to Studia Logica on January 31st, 2020