 As inductively defined sets can be the starting point of another inductive definition, the procedure of inductively defining predicates can be iterated along any well-ordering \(\nu\) in a uniform way. This leads to the theories \(\bID_{\nu}\) which allow one to formalize \(\nu\)-times iterated inductive definitions, where \(\nu\) stands for a primitive recursive well-ordering. If \(\nu\) is a well-ordering on constructive grounds then also the \(\nu\)-times iterated version of Kleene’s \(\cO\) has a clear constructive meaning. As a result the formal theories \({{\bID}}^i_{\nu}(\cO)\) that embody this process are constructively justified. The topic of theories of iterated inductive definitions was flourishing at the 1968 conference on Intuitionism and Proof Theory in Buffalo (see Kino et al. 1970). One of the main proof-theoretic goals was to find a reduction of the classical theories \(\bID_{\nu}\) to their intuitionistic counterparts \({{\bID}}^i_{\nu}(\cO)\). This was all the more desirable because of known reductions of important fragments of second order arithmetic to theories of the former kind. Friedman (1970) had shown that the second order system with the \(\Sigma _2^1\)-axiom of choice can be interpreted in the system \(\hbox{($\Pi_1^1$-CA)}_{&lt;{\varepsilon_0}}\) of less than \({\varepsilon_0}\)-fold iterated \(\Pi_1^1\)-comprehensions and Feferman (1970a) had shown that less than \(\nu\)-fold iterated \(\Pi_1^1\)-comprehensions could be interpreted in the system 