@ARTICLE{PittsAM:intsoq, AUTHOR={A.~M.~Pitts}, TITLE={On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic}, JOURNAL={Jour.\ Symbolic Logic}, VOLUME=57, YEAR=1992, PAGES={33--52}, ABSTRACT={We prove the following surprising property of Heyting's intuitionistic propositional calculus, $\IpC$. Consider the collection of formulas, $\phi$, built up from propositional variables ($p,q,r,\ldots$) and falsity ($\F$) using conjunction ($\conj$), disjunction ($\disj$) and implication ($\imp$). Write $\vdash\phi$ to indicate that such a formula is intuitionistically valid. We show that for each variable $p$ and formula $\phi$ there exists a formula $\All_p\phi$ (effectively computable from $\phi$), containing only variables not equal to $p$ which occur in $\phi$, and such that for all formulas $\psi$ not involving $p$, $\vdash\psi\imp\All_p\phi$ if and only if $\vdash\psi\imp\phi$. Consequently quantification over propositional variables can be modelled in $\IpC$, and there is an interpretation of the second order propositional calculus, $\IpC^2$, in $\IpC$ which restricts to the identity on first order propositions.\par An immediate corollary is the strengthening of the usual Interpolation Theorem for $\IpC$ to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of $\IpC$, the theory of Heyting algebras. In particular we show that a model of $\IpC^2$ can be constructed whose algebra of truth-values is equal to any given Heyting algebra.}}