Multi-agent coordination research
paperAuthor
Credibility Rating
Good quality. Reputable source with community review or editorial standards, but less rigorous than peer-reviewed venues.
Rating inherited from publication venue: arXiv
This is a formal logic paper on modal type theory and epistemic logic; it has limited direct relevance to AI safety despite its current tags, which appear to be mislabeled. It may have tangential relevance to formal verification or multi-agent epistemic reasoning frameworks.
Paper Details
Metadata
Abstract
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.
Summary
This paper develops a natural deduction calculus for intuitionistic epistemic logic (IEL⁻) and establishes a modal λ-calculus providing computational semantics for belief modalities. The authors prove key proof-theoretic properties and extend the Curry-Howard correspondence to a categorical semantics for proof identity, clarifying how belief operators function within an intuitionistic framework.
Key Points
- •Introduces natural deduction calculus for IEL⁻, an intuitionistic logic of belief based on the BHK interpretation of epistemic statements.
- •Establishes a modal λ-calculus (proofs-as-programs correspondence) providing computational semantics for deductions involving belief modalities.
- •Proves good proof-theoretic properties for IEL⁻ using the modal type-theoretic interpretation.
- •Extends the Curry-Howard-Lambek correspondence to categorical semantics, clarifying the general structure of belief modality in intuitionistic logic.
- •Builds on Artemov and Protopopescu's intuitionistic epistemic logic, distinguishing belief (weaker) from knowledge (stronger) in a constructive setting.
Cited by 1 page
| Page | Type | Quality |
|---|---|---|
| Corrigibility Failure Pathways | Analysis | 62.0 |
Cached Content Preview
\\UseAllTwocells
# Curry-Howard-Lambek correspondence for intuitionistic belief††thanks: The present version is a revised one; the original manuscript was submitted for publication to _Studia Logica_ in January 2020.
Cosimo Perini Brogi
(Department of Mathematics ⋅⋅\\cdot University of Genova
perinibrogi@dima.unige.it)
###### Abstract
This paper introduces a _natural deduction calculus for intuitionistic logic of belief_ 𝖨𝖤𝖫−superscript𝖨𝖤𝖫\\mathsf{IEL}^{-} which is easily turned into a _modal λ𝜆\\lambda-calculus_ giving a computational semantics for deductions in 𝖨𝖤𝖫−superscript𝖨𝖤𝖫\\mathsf{IEL}^{-}. By using that interpretation, it is also proved that 𝖨𝖤𝖫−superscript𝖨𝖤𝖫\\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 𝖨𝖤𝖫−superscript𝖨𝖤𝖫\\mathsf{IEL}^{-} showing the general structure of such a modality for belief in an intuitionistic framework.
- Keywords:
Intuitionistic modal logic, epistemic logic, categorial proof theory, modal type theory, proofs-as-programs.
## Introduction
Brouwer-Heyting-Kolmogorov (BHK) interpretation is based on a semantic reading of propositional variables as problems (or tasks), and of logical connectives as operations on _proofs_. In this way, it provides a semantics of mathematical statements in which the computational aspects of proving and refuting are highlighted.111The reader is referred to \[ [16](https://ar5iv.labs.arxiv.org/html/2006.02417#bib.bib16 "")\] for an introduction.
In spite of being named after L.E.J. Brouwer, this approach is rather away from the deeply philosophical attitude at the origin of intuitionism: In BHK interpretation, reasoning intuitionistically is similar to a safe mode of program execution which always terminates; on the contrary, according to the founders of intuitionism, at the basis of the mathematical activity there is a continuous mental process of construction of objects starting with the flow of time underlying the chain of natural numbers, and intuitionistic reasoning is what structures that process.222For instance, Dummett’s \[ [6](https://ar5iv.labs.arxiv.org/html/2006.02417#bib.bib6 "")\] advocates a purely philosophical justification of the whole current of intuitionistic mathematics.
This reading of the mathematical activity is formally captured by Kripke semantics for intuitionistic logic \[ [9](https://ar5iv.labs.arxiv.org/html/2006.02417#bib.bib9 "")\]: Relational structures based on pre-orders capture the informal idea of a process of growth of knowledge in time which characterises the mental life of the mathematician.
It is worth-noting that the focuses of these semantics are quite different: BHK interpretation stresses the importance of the concept of proof in the semantics for intuitionistic logic; Kripke’s approach highlights the epistemic process behind the provability of a statement.
In \[ [2
... (truncated, 59 KB total)221e83bb5f66ddc0 | Stable ID: YTg0ZGQ3NT