@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.}}