| Title: |
Curry-Howard-Lambek Correspondence for Intuitionistic Belief |
| Authors: |
Brogi, Cosimo Perini |
| Publication Year: |
2020 |
| Collection: |
Computer Science; Mathematics |
| Subject Terms: |
Mathematics - Logic; Computer Science - Logic in Computer Science; 03F03, 03F05, 03F07; F.4.1 |
| Description: |
This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $\lambda$-calculus giving a computational semantics for deductions in $\mathsf{IEL}^{-}$. By using that interpretation, it is also proved that $\mathsf{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 $\mathsf{IEL}^{-}$ showing the general structure of such a modality for belief in an intuitionistic framework.; Comment: Submitted to Studia Logica on January 31st, 2020 |
| Document Type: |
Working Paper |
| Access URL: |
http://arxiv.org/abs/2006.02417 |
| Accession Number: |
edsarx.2006.02417 |
| Database: |
arXiv |