论文标题
直觉信念
Curry-Howard-Lambek Correspondence for Intuitionistic Belief
论文作者
论文摘要
本文介绍了一种自然的扣除微积分，以实现信念的直觉逻辑$ \ mathsf {iel}^{ - } $，很容易变成模态$λ$ -CALCULUS，以$ \ MATHSF {iel}^{ - } $中的计算语义进行计算语义。通过使用该解释，还可以证明$ \ mathsf {iel}^{ - } $具有很好的证明理论属性。然后，将扣除术语和键入项之间的对应关系扩展到一个分类语义，以标识$ \ Mathsf {iel}^{ - } $中的证据，以表明对直觉框架的信念的一种通用结构。
This paper introduces a natural deduction calculus for intuitionistic logic of belief $\mathsf{IEL}^{-}$ which is easily turned into a modal $λ$-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.
