System F is a system of parametric polymorphism that corresponds to second order propositional logic. As a system of typed λ-calculus, it has the strong normalization property (where not all such terms are typed) and types all normal forms. These imply that some β-expansions fail. In this talk we will explore the properties of this system and give some partial results regarding the question of ω (λx.xx) expansions.