On the complexity of propositional quantification in intuitionistic logic

We define a propositionally quantified intuitionistic logic Hsub-pi+ by a natural extension of Kripke's semantics for propositional intuitionistic logic. We then show that Hsub-pi+ is recursively isomorphic to full second order classical logic. Hsub-pi+ is the intuitionistic analogue of the modal systems S5sub-pi+, S4sub-pi+, S4.2sub-pi+, K4sub-pi+, Tsub-pi+, Ksub-pi+ and Bsub-pi+, studied by Fine