[TYPES] Question about the polymorphic lambda calculus

[Samuel E. Moelius III]

Miles,

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

I appreciate your point.  But this case is special in at least two 
respects: (1) the quantified statements are all of a certain form (i.e., 
there exists a term with a certain type), and (2) the object language is 
the polymorphic lambda calculus, specifically.  For this special case, I 
think there is good reason to suspect that the universal quantifier can 
be expressed in the object language.

Sam