Curry–Howard–Lambek Correspondence for Intuitionistic Belief

Abstract This paper introduces a natural deduction calculus for intuitionistic logic of belief $$\mathsf {IEL}^{-}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:msup><mml:mrow><mml:mi>IEL</mml:mi></mml:mrow><mml:mo>-</mml:mo></mml:msup></mml:math> which is easily turned into a modal $$\lambda $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:mi>λ</mml:mi></mml:math> -calculus giving a computational semantics for deductions in $$\mathsf {IEL}^{-}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:msup><mml:mrow><mml:mi>IEL</mml:mi></mml:mrow><mml:mo>-</mml:mo></mml:msup></mml:math> . By using that interpretation, it is also proved that $$\mathsf {IEL}^{-}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:msup><mml:mrow><mml:mi>IEL</mml:mi></mml:mrow><mml:mo>-</mml:mo></mml:msup></mml:math> 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}^{-}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mml:msup><mml:mrow><mml:mi>IEL</mml:mi></mml:mrow><mml:mo>-</mml:mo></mml:msup></mml:math> showing the general structure of such a modality for belief in an intuitionistic framework.