On Some Syntactic Properties of the Modalized Heyting Calculus

Abstract

We show that the modalized Heyting calculus~\cite{esa06} admits a normal axiomatization. Then we prove that in this calculus the inference rule $\square \alpha /\alpha$ is admissible (Proposition 5.6), but the rule $\square \alpha \to \alpha /\alpha$ is not (Proposition 6.1). Finally, we show that this calculus and intuitionistic propositional calculus are assertorically equipollent, which leads to a variant of limited separation property for the modalized Heyting calculus.

arXiv comment16 pages