Can we prove weak normalization for System F by induction on a transfinite ordinal Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak normalization strategy by induction on $\epsilon_0$.

What about System F (or weaker)? Is there a weak normalization proof in this style? If not, can it be done at all?
In a very silly way, weak normalization for any reasonable system can be proved by induction on a constructive ordinal, provided of course that weak normalization holds. Indeed, the statement that System F has weak normalization is formalizable in arithmetic as a $\Pi^0_2$ sentence, and as such is provable (since it's true) by transfinite induction along a non-natural constructive ordinal-notation of height $\omega^2$. (See this question on the mathematics stack exchange for how this ordering could work.) 

However, as jbapple mentions, we don't know of a "natural" ordinal notation that works. We don't even know how to define "natural", but the one above isn't natural (since to see that it's well-founded we'd have to know weak normalization of System F to begin with), whereas the standard ones for $\varepsilon_0$, $\Gamma_0$, and various larger ones using ideas from large cardinal axioms, are natural.

Hopefully one day someone will come up with an ordinal notation for second order arithmetic that everyone will agree is natural, and then that could be used in an honest way to prove weak normalization for System F.