 It entails of course the special case that \(\bRA^* \stile{\alpha}{\omega^\nu} \Gamma\Rightarrow \Delta\) yields \(\bRA^* \stile{\varphi_{\nu}(\alpha)}{0} \Gamma\Rightarrow \Delta\), and thus, as the latter deduction is cut-free, all cuts can be removed. Several subtheories of \(\bZ_2\) can be interpreted in \(\bRA^*\), yielding upper bounds for their proof-theoretic ordinals via  Theorem 5.8.  Here is a selection of such  results:[24] 