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

Martin-Löf introduced the notion of universes in type theory motivated, in part, by the discovery of a paradox with a type of all types [see \textit{P. Martin-Löf}, ``An intuitionistic theory of types'', in: G. Sambin (ed.) et al., Twenty-five years of constructive type theory, Oxford Logic Guides 36, 127-172 (1998; Zbl 0931.03070)]. This is a natural reflection principle, which can be seen as an intuitionistic version of the notion of Grothendieck universes in set theory. Palmgren, motivated by his domain model of universes, introduced in his Ph.D. thesis, the notion of next universe operator and of superuniverse, which is a universe closed by the universe operator. He introduced also an higher-order version of this notion, which can be seen as an intuitionistic version of Mahlo cardinals. In the absence of generalised inductive definitions, all these systems can be called predicative. This paper provides an ordinal analysis of type theory with a superuniverse. Hancock found the lower bound \(\phi_{\epsilon_0}(0)\) (where \(\phi_{\alpha}(\beta)\) is the usual Veblen hierarchy) for one universe, and the lower bound \(\Gamma_0\) for a sequence of universes (these bounds were proved optimal by, respectively, Aczel and Feferman [see \textit{S. Feferman}, in G. Metakides (ed.), Patras Logic Symp., Proc., Patras, Greece 1980, Stud. Log. Found. Math. 109, 171-196 (1982; Zbl 0522.03045)]). The ordinal of type theory with a superuniverse is \(\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\). This ordinal is below the Howard ordinal (the ordinal of one generalised inductive definition) but bigger than \(\Gamma_0\). This is quite interesting because it has been argued previously (following the work of Schütte and Feferman in the 60s) that \(\Gamma_0\) is an upper bound for predicative systems. This is a rich paper. Among other things, it presents a fragment of intuitionistic second-order arithmetic, Intuitionistic Analysis with Replacement, that can be interpreted in type theory with one universe (Martin-Löf had considered a similar system, with an axiom of choice instead, in the reference given above). The lower bound argument uses techniques from \textit{K. Schütte}'s book [Proof theory (Springer, Berlin) (1977; Zbl 0367.02012)]. Finally a realisability interpretation of type theory with a superuniverse is given in a classical set theory which is a proper extension of Kripke-Platek set theory with the crucial exception of Foundation (which would correspond in type theory to the \(W\)-type, or generalised inductive definitions). This interpretation will be used in the second part to give a proof that this lower bound is optimal.