The intuitionistic propositional calculus with quantifiers

Let L be the language of the intuitionistic propositional calculus J completed by the quantifiers ∀ and ∃, and let calculus 2J in language L contain, besides the axioms of J, the axioms ∀xB (x) ⊃ B(y) and B(y) ⊃ ∃xB (x). A Kripke semantics is constructed for 2J and a completeness theorem is proven. A result of D. Gabbay is generalized concerning the undecidability of C2J+-extension of 2J by schemes ∃x (x ≡B) and ∀x(A ∀ B(x))⊃A ∀xB (x) specificially: the undecidability is proven of each T theory in language L such that [2J]⊑T ⊑[C2J+] ([2J] ([2J] denotes the set of all theorems of calculus 2J).