Curry-Howard-Lambek Correspondence for Intuitionistic Belief
Cosimo Perini Brogi

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 which is easily turned into a modal -calculus giving a computational semantics for deductions in . By using that interpretation, it is also proved that has good proof-theoretic properties. The correspondence between deductions and typed terms is then extended to a categorical semantics for identity of proofs in showing the general structure of such a modality for belief in an intuitionistic framework.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies
