The strength of Martin-Löf type theory with a superuniverse. II (Q5945010)

In Part I [ibid. 39, No. 1, 1-39 (2000; Zbl 0953.03065)] a realisability interpretation of \textbf{MLS}, i.e., type theory with a superuniverse, was given in a classical theory \({\mathbf T}^S\). It was shown that the proof-theoretic ordinal of \textbf{MLS} is at least \(\Phi_{\Gamma_0}(0)\), where \(\Phi_{\alpha}(\beta)\) is similar to the Veblen hierachy but starts with \(\Phi_0(\xi) = \Gamma_{\xi}\), where \(\Gamma_{\alpha}\) is the \(\alpha\)th ordinal \(\rho>0\) such that \(\phi_{\delta}(\xi)<\rho\) for all \(\xi,\delta<\rho\). In this part, it is proved that the proof-theoretic ordinal of \({\mathbf T}^S\) is at most \(\Phi_{\Gamma_0}(0)\), thus establishing that \textbf{MLS} and \({\mathbf T}^S\) have the same strength and that \(\Phi_{\Gamma_0}(0)\) is their proof-theoretic ordinal. This analysis is obtained using a suitable infinitary proof system. Thus \textbf{MLS} and \({\mathbf T}^S\) provide examples of theories of strength strictly between the Feferman-Schütte ordinal \(\Gamma_0\) and the Bachmann-Howard ordinal.