2021/03/02 by Cosimo Perini Brogi, Brogi, Cosimo Perini
Computer Science · #AI-based Problem Solving and Planning #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2103.01734
openalex publication_date 2021/03/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-reflection A→\Box A. This way, belief is interpreted as a result of verification, and it fits an extended Brouwer-Heyting-Kolmogorov interpretation for intuitionistic propositional logic with an epistemic modality. In the present paper, structural properties of a natural deduction system IEL- for intuitionistic belief are investigated. The focus is on the analyticity of the calculus, so that the normalization theorem and the subformula property are proven firstly. From these, decidability and consistency of the logic follow as corollaries. Finally, disjunction properties, \Box-primality, and admissibility of reflection rule are established by using purely proof-theoretic methods.