Strong normalization for the parameter-free polymorphic lambda calculus based on the Ω-rule

Following Aehlig [3], we consider a hierarchy F^p = {F^p _n}_n∈ℕ of parameter-free subsystems of System F, where each F^p _n corresponds to ID_n, the theory of n-times iterated inductive definitions (thus our F^p _n corresponds to the n + 1th system of [3]). We here present two proofs of strong normalization for F^p _n, which are directly formalizable with inductive definitions. The first one, based on the Joachimski-Matthes method, can be fully formalized in IDn+1. This provides a tight upper bound on the complexity of the normalization theorem for System F^p _n. The second one, based on the Gödel-Tait method, can be locally formalized in IDn. This provides a direct proof to the known result that the representable functions in F^p _n are provably total in IDn. In both cases, Buchholz' Ω-rule plays a central role.