 Definition 5.7 In the following we assume that the ordinals come from some representation system. The language of \(\bRA^*\) is an extension of that of first order arithmetic. For each ordinal \(\alpha\) and \(\beta&gt;0\) it has free set variables \(U_0^\alpha,U^\alpha_1,U^\alpha_2\ldots\) of level \(\alpha\) and bound set variables of level \(\beta\). The level, \({\textrm{lev}(A)}\), of a formula A of \(\bRA^*\) is defined to be the maximum of the levels of set variables that occur in A. Expressions of the form \(\{x\mid A(x)\}\) with \(A(u)\) a formula will be called abstraction terms, their level being the same as that of the formula \(A(u)\).