Cosimo Perini Brogi

Curry–Howard–Lambek Correspondence for Intuitionistic Belief

2021 · Studia Logica

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 …