The intuitionistic propositional calculus with quantifiers

Let $L$ be the language of the intuitionistic propositional calculus $J$ completed by the quantifiers $\forall$ and $\exists$, and let calculus $2J$ in language $L$ contain, besides the axioms of $J$, the axioms $\forall\,x$ $B(x)\supset B(y)$ and $B(y)\supset\exists\,x$ $B(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 $\exists\,x$ $(x\equiv B)$ and $\forall\,x$ $(A\vee B(x))\supset A\vee\forall\,x$ $B(x)$ specificially: the undecidability is proven of each $T$ theory in language $L$ such that $[2J]\subseteq T\subseteq[C2J^+]$ ($[2J]$ denotes the set of all theorems of calculus $2J$).