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\rightarrow\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 $\mathsf{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.
翻译:Artemov 和 Protopopescu 将异端信仰作为直觉理论理论逻辑的延伸,通过分配性方案K和共同反射 $A\rightrowr\Box A$(美元) 和共同反射 $A\rightrowr\Box A$(美元) 的延伸。 这样,通过核查来解释信仰,它符合对直观理论理论逻辑的延伸的Broewer-Heyting-Kolmogorov 解释, 并带有感知性模式。 本文调查了自然推算系统($\mathsf{IEL}- $) 的结构性特性, 用于直觉信仰的结构性特性。 重点是微积分的解析性, 从而首先证明正统的理论和亚形属性。 从这些角度, 逻辑的分解性和一致性作为引力。 最后, 使用纯证据理论方法确定了分离属性、 $\Box$- Primality, 和反射规则的可接受性。