We prove the following surprising property of Heyting's intuitionistic
propositional calculus, IpC. Consider the collection of formulas,
<i>A</i>, built up from propositional variables and falsity using
conjunction, disjunction and implication . Write |-<i>A</i> to
indicate that such a formula is intuitionistically valid. We show that
for each variable <i>p</i> and formula <i>A</i> there exists a formula
<i>All_p(A)</i> (effectively computable from <i>A</i>), containing
only variables not equal to <i>p</i> which occur in <i>A</i>, and such
that for all formulas <i>B</i> not involving <i>p</i>,
|-<i>B</i>=><i>All_p(A)</i> if and only if |-<i>B</i>=><i>A</i>.
Consequently quantification over propositional variables can be
modelled in <i>IpC</i>, and there is an interpretation of the second
order propositional calculus, IpC2, in IpC which restricts to the
identity on first order propositions.

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 IpC2 can be constructed whose algebra of truth-values is
equal to any given Heyting algebra.