  The ramified hierarchy has been also the source of much work in proof theory. After the discovery by Gentzen that the consistency of Arithmetic could be proved by transfinite induction (over decidable predicates) along the ordinal \(\varepsilon_0\), the natural question was to find the corresponding ordinal for the different levels of the ramified hierarchy. Schütte (1960) found that for the first level of the ramified hierarchy, that is if we extend arithmetic by quantifying only over first-order properties, we get a system of ordinal strength \(\varepsilon_{\varepsilon_0}\). For the second level we get the ordinal strength \(\varepsilon_{\varepsilon_{ \varepsilon_0}}\), etc. We recall that \(\varepsilon_{\alpha}\) denotes the \(\alpha\)-th \(\varepsilon\)-ordinal number, an \(\varepsilon\)-ordinal number being an ordinal \(\beta\) such that \(\omega^{\beta} = \beta\), see Schütte (1960).