Curry–Howard–Lambek Correspondence for Intuitionistic Belief
Cosimo Perini Brogi · Studia Logica · 2021
Abstract This paper introduces anatural deduction calculus for intuitionistic logic of belief $$\mathsf {IEL}^{-}$$ IEL- which is easily turned into amodal $$\lambda $$ λ -calculusgiving a computational semantics for deductions in $$\mathsf {IEL}^{-}$$ IEL- . By using that interpretation, it is also proved that $$\mathsf {IEL}^{-}$$ IEL- hasgood proof-theoretic properties. The correspondence between deductions and typed terms is then extended to acategorical semanticsfor identity of proofs in $$\mathsf {IEL}^{-}$$ IEL- showing the general structure of such a modality for belief in an intuitionistic framework.