ON THE COMPLEXITY OF PROPOSITIONAL QUANTIFICATION IN INTUITIONISTIC LOGIC

We define a propositionally quantified intuitionistic logic H pi+ by a natural extension of Kripke's semantics for propositional intuitionis tic logic. We then show that H pi+ is recursively isomorphic to full s econd order classical logic. H pi+ is the intuitionistic analogue of t he modal systems S5 pi+, S4 pi+, S4.2 pi+, K4 pi+, T pi+, K pi+ and B pi+, studied by Fine.