Multi-agent coordination research

paper

2020·arXiv·arxiv.org/abs/2006.02417

Author

Cosimo Perini Brogi

Credibility Rating

3/5

Good(3)

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

Citations

0 influential

Year

2011

Methodology

book-chapter

Metadata

Importance: 12/100arxiv preprintprimary source

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

HTTP 200Fetched Apr 7, 202660 KB

[2006.02417] Curry-Howard-Lambek correspondence for intuitionistic beliefThe present version is a revised one; the original manuscript was submitted for publication to Studia Logica in January 2020. 
 
 
 
 
 
 
 
 
 
 
 

 
 
 

 
 
 
 
 
 
 
 \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. 1 1 1 The reader is referred to [ 16 ] 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. 2 2 2 For instance, Dummett’s [ 6 ] 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 ] : 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 seman

... (truncated, 60 KB total)

Resource ID: 221e83bb5f66ddc0 | Stable ID: sid_VpginPvTNn