Curry-Howard-Lambek Correspondence for Intuitionistic Belief

TL;DR

This paper develops a Curry-Howard-Lambek correspondence for intuitionistic belief logic, providing a natural deduction calculus, a modal lambda calculus semantics, and categorical proof identity insights.

Contribution

It introduces a new natural deduction calculus for intuitionistic belief logic and extends the Curry-Howard-Lambek correspondence to this modal setting.

Findings

The calculus has good proof-theoretic properties.

A computational semantics for belief deductions is established.

Categorical semantics for proof identity in belief logic is developed.

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.