Encoding universal types in terms of existential types?

Question

In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.

In "Types and Programming Languages", the following exercise appears:

Can we encode universal types in terms of existential types?

My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?

I am not even sure what I need to prove to formally show this result.

Byron

You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form – Transformation

@JuanPabloSantos I fail to see the connection – Byron

I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of Yoneda T ~ (forall a. (T->a)->a) where we can take T = exists b. f b and exploit the type isomorphism (T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-Yoneda T ~ (exists a. a * (a -> T)), but here T is in positive (covariant) position, so choosing T ~ (forall b. f b) does not allow to turn forall into some exists. – Assertion

There is an extended Curry–Howard isomorphism (aka the Brouwer–Heyting–Kolmogorov interpretation) between intuitionistic predicate calculus and simply-typed lambda calculus.¹ In classical logic the following formulas hold. ◦ ∃xφ(x)↔¬∀x¬φ(x), ◦ ∃x(φ(x)→∀yφ(y)), ◦ ∀x(φ(x)∨¬φ(x)). In intuitionistic logic these formulas do not hold, although the following do. ◦ ∃xφ(x)→¬∀x¬φ(x), ◦ ∀x¬¬(φ(x)∨¬φ(x)).² See: ¹cs.nott.ac.uk/~psznza/papers/Alechina++:01a.pdf ²phil.uu.nl/~iemhoff/Mijn/Slides/seattle17.pdf – Sultanate