[TYPES] Question about the polymorphic lambda calculus

[Herman Geuvers]

Samuel E. Moelius III 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?
>
> If this is a theorem, could someone please point me to a proof of it?
>
> Thanks in advance.
>
> Sam Moelius
>
>   

Dear Sam,

If I look at your question in the polymorphic lambda calculus (system 
F), then it is basically a question about derivability in second order 
proposition logic PROP2:
Does the following hold?
    If |- Phi(U)  for every closed proposition U, then |- forall X Phi(X)

PROP2 is constructive proposition logic: only implication -> and a 
second order quantifier over propositions.

Now, in the classical case, your conjecture holds, because then, if |- 
Phi(U)  for every closed proposition U, then
|- Phi(top) and |- Phi(bot) and so |- forall X. Phi(X).
(In classical PROP2, let's call it CPROP2, we have an axiom forall X.(X 
\/ ~X); bot is forall X.X and
top is forall X. X->X. The definition of the connectives is just the 
usual one from PROP2.)
That |- Phi(top) and |- Phi(bot) imply |- forall X. Phi(X) is because we 
have a complete truth table semantics for CPROP2. I have spelled that 
out in detail in my PhD thesis in 1993.

Now, can we conclude anything from this for PROP2?
Yes, because there is a G"odel not-not translation from CPROP2 to PROP2. 
One can take the one from Coquand-Herbelin (called "A-translation" in 
their paper) or the "standard one" in the book of Van Dalen (Logic and 
Structure):
Coquand-Herbelin:
    X* := X
    (A->B)* := ~~A* -> ~~B*
    (forall X.A)* := forall X. ~~A*
van Dalen:
    X* := ~~X
    (A->B)* := A* -> B*
    (forall X.A)* := forall X. A*
For the first one, we have
    Gamma |-_{CPROP2} phi   <=> ~~(Gamma*) |- _{PROP2} ~~(phi*)
For the second one, we have
    Gamma |-_{CPROP2} phi   <=> Gamma* |- _{PROP2} phi*

So if we consider the van Dalen translation, we can derive that for 
formulas of the form Phi(X)*, we have (in PROP2):
       If |- Phi(U)*  for every closed proposition U, then |- forall X. 
Phi(X)*

Proof: If |-_{PROP2} Phi(U)*  for every closed proposition U, then 
|-_{PROP2} Phi(top)*
and |-_{PROP2} Phi(bot)*, so |-_{CPROP2} Phi(top) and |-_{CPROP2} 
Phi(bot), so |-_{CPROP2} forall X. Phi(X),
so |-_{PROP2} forall X. Phi(X)*.

I have no idea to which extent this extends to the general case.

Best Regards

Herman Geuvers

References:
========
My PhD thesis:
J.H. Geuvers, Logics and Type systems 
<http://www.cs.ru.nl/%7Eherman/PUBS/Proefschrift.ps.gz>, PhD. Thesis, 
University of Nijmegen, September 1993. 
http://www.cs.ru.nl/~herman/PUBS/Proefschrift.ps.gz

Thierry Coquand, Hugo Herbelin
A-translation and Looping Combinators in Pure Type Systems, 1994, 
Journal of Functional Programming

Dirk van Dalen
Logic and Structure (3rd extended ed.). Springer Verlag, Berlin.