[TYPES] Question about the polymorphic lambda calculus

[Miles Sabin]

On Tue, Jun 3, 2008 at 11:38 AM, Samuel E. Moelius III
<moelius at cis.udel.edu> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Suppose that T is a type with exactly one free variable X.  Further
> suppose that for every closed type U, there is some term with type
> T[U/X].  Then, does there necessarily exist some term with type (forall
> X. T)?
>
> In other words, in the situation described above, can the meta-level
> ``forall'' be pushed down into the types?

Maybe I'm missing something, but I would have thought that in general
the answer has to be no: it doesn't follow from the fact that
universal quantification is expressible in the meta-language that it's
expressible in the object-language.

Compare the analogous situation with first-order predicate calculus as
the meta-language for first-order propositional calculus with
countably infinite named constants and a finiteness constraint on
proposition and proof length.

Cheers,


Miles