Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part II

This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style proof. For that, we make use of a family of intuitionistic deduction theorems, which are also presented in this paper by means of Mizar system [2], [1]. Our axiom system of intuitionistic propositional logic IPC is based on the propositional subsystem of H₁-IQC in Troelstra and van Dalen [6, p. 68]. We also owe Heyting [4] and van Dalen [7]. Our treatment of a set-theoretic intuitionistic deduction theorem is due to Agata Darmochwał’s Mizar article “Calculus of Quantifiers. Deduction Theorem” [3].