Curry-Howard-Lambek Correspondence for Intuitionistic Belief

2020/06/03 by Cosimo Perini Brogi, Brogi, Cosimo Perini
Computer Science · #03F03 #03F05 #03F07 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2006.02417

openalex publication_date 2020/06/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

This paper introduces a natural deduction calculus for intuitionistic logic of belief IEL^- which is easily turned into a modal λ-calculus giving a computational semantics for deductions in IEL^-. By using that interpretation, it is also proved that 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 IEL^- showing the general structure of such a modality for belief in an intuitionistic framework.

Citations

• Calculi for Intuitionistic Normal Modal Logic

Related

• Categorical and Algebraic Aspects of the Intuitionistic Modal Logic\n \IEL^- and its predicate extensions
• An analytic calculus for intuitionistic belief
• Justification Logic of the Lambda Calculus
• Base-extension Semantics for Intuitionistic Modal Logics
• A Proof-theoretic Semantics for Intuitionistic Linear Logic