 The ordinal that Feferman and Schütte determined as the least upper bound for \(\{{{\bR}}_a\}\) is \(\Gamma_0\), the least non-zero ordinal closed under the Veblen function \(\alpha,\beta\mapsto\varphi_{\alpha}(\beta)\). This was a genuine proof-theoretic result with the tools coming ready-made from Schütte’s (1960b) monograph. There he had calculated the proof-theoretic ordinals of the \({{\bR}}_a\) as a function of \(\lvert a\rvert\), using cut elimination techniques for logics with infinitary rules (dubbed “semi-formal systems”). If \(\lvert a\rvert =\omega^{\alpha}\) then \(\lvert {{\bR}}_a\rvert =\varphi_{\alpha}(0)\). “Semi-formal” is a terminology employed by Schütte and refers to the fact that this proof system has rules with infinitely many premises, similar to the \(\omega\)-rule.