Abstract

We define a propositionally quantified intuitionistic logic $\mathbf{H}\pi +$ by a natural extension of Kripke's semantics for propositional intutionistic logic. We then show that $\mathbf{H}\pi+$ is recursively isomorphic to full second order classical logic. $\mathbf{H}\pi+$ is the intuitionistic analogue of the modal systems $\mathbf{S}5\pi +, \mathbf{S}4\pi +, \mathbf{S}4.2\pi +, \mathbf{K}4\pi +, \mathbf{T}\pi +, \mathbf{K}\pi +$ and $\mathbf{B}\pi +$, studied by Fine.