Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
The most comprehensive survey of the relationship between constructive proof theory (which is tied closely to the theory of constructive ordinals) and second-order impredicative arithmetic (which as Ulrik points out is equivalent in strength to System F) is Girard (1989). There he builds on his theory of dilators (1981), which I don't really follow, but I think essentially provides a nonconstructive theory of higher-order Skolemisation.
My understanding is that you can't express $\Sigma^1_2$ formulae constructively in the Bishop—Martin-Löf sense, because they are impredicative in a way you can't eliminate by adding any sort of first-order induction scheme.
I remember suggesting to an ordinal theorist that one could simply stipulate that you can ground an impredicative constructivism in a type theory based on the polymorphic lambda calculus, and use the reduction candidate technique from Girard's SN proof for System F to impose a reasonable total order on the universe of constructions, calling the equivalence classes you get from this the ordinals; he said something intelligent which I took away as saying you might get that to work, but it would have all the advantages of theft over honest toil. To get it to work, it is not good enough that you can prove in set theory the existence of such ordinals, you would need a constructive proof of trichotomy for the order.
To sum up, with the regular notion of intuitionistic construction due to Bishop—Martin-Löf, the literature I know of strongly suggests no. If you are averse to honest toil and would embrace an impredicative constructivism, then my guess is that it can probably be done. You would, naturally, need a stronger theory that System F to constructively prove the required trichotomy, but the Calculus of Inductive Constructions provides an obvious candidate.
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.
I think that System F corresponds to second-order arithmetic, in that the total functions from $\mathbb{N} \to \mathbb{N}$ are the same in both.(Proofs and Types, 15.1.3 and 15.2).
Furthermore, I think second order arithmetic is quite strong and that no constructive upper bound is yet known for its "proof theoretic ordinal" (The art of ordinal analysis, section 3).
I think this constructive ordinal bound is what is needed to do the induction you request.
