Well-ordering proofs for Martin-Löf type theory (Q1295372)

In his Ph.D. thesis [Proof theoretical strength of Martin-Löf type theory with \(W\)-type and one universe, Diss., Univ. München (1993; Zbl 0863.03029)], the author proved an upper bound \(\alpha= \psi_{\Omega_1} \Omega_{I+\omega}\) for the proof-theoretic ordinal of Martin-Löf's intuitionistic type theory with \(W\)-type and one universe. In the present paper he proves in this system transfinite induction up to every ordinal less than \(\alpha\). This determines the proof-theoretic strength of the theory and shows that it is slightly stronger than Feferman's theory \(T_0\) and \((\Delta^1_2- \text{CA})+ (\text{BI})\). The author points out that the proof extends to show that the strength of Martin-Löf's type theory with \(n\) universes is \(\psi_{\Omega_1} \Omega_{I_n+ \omega}\) where \(I_n\) is the \(n\)th inaccessible, and this implies that the strength of the theory with arbitrary finitely iterated universes is \(\psi_{\Omega_1} I_\omega\) where \(I_\omega= \sup\{I_n\mid n\in\omega\}\).