On Some Syntactic Properties of the Modalized Heyting Calculus

TL;DR

This paper establishes a normal axiomatization for the modalized Heyting calculus, analyzes the admissibility of certain inference rules, and compares its assertoric strength to intuitionistic propositional calculus.

Contribution

It provides the first normal axiomatization for the modalized Heyting calculus and examines the admissibility of key inference rules, highlighting its logical properties.

Findings

The calculus admits a normal axiomatization.

The rule $oxdoteta/eta$ is admissible, but $oxdoteta ightarroweta/eta$ is not.

The calculus is assertorically equivalent to intuitionistic propositional 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\rightarrow\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.