[TYPES] typability in Curry-style System F

[Uwe Nestmann]

Dear Types,

while we have many possible types for \omega in Curry-style System F (or \lambda 2, as by Barendregt): is there any publication that contains a reasonably formal “direct" argument/proof why \Omega = \omega\omega is _not_ Curry-typable in System F?

I mean “direct” in the sense of not indirectly arguing with the strong normalization theorem.

The closest I could find is in the book “Type Theory and Formal Proof” by Nederpelt and Geuvers just telling that it would be “far from obvious” (p 81) ...

== Uwe ==