 for \(\nu=\omega^{\gamma}\) with \(\gamma\) limit. However, Zucker (1973) showed that there are definite obstacles to a straightforward reduction of the theories \(\text{ID}_{\nu}\) for \(\nu &gt; 1\) to their intuitionistic cousins. Sieg (1977) attacked the problem by a method adapted from Tait (1970) who had used cut elimination for an infinitary propositional logic with formulae indexed over constructive number classes to obtain a consistency proof for second order arithmetic theory with the schema of \(\Sigma _2^1\) dependent choices. He achieved a reduction of \(\bID_{&lt;\nu}\) to \(\bID_{&lt;\nu}^i(\cO)\) for limit \(\nu\) by carrying out the proof theory for a system of \(\PL_{\alpha}\) of propositional logic with infinitely long conjunctions and disjunctions indexed over the constructive number classes \(\cO_{\alpha}\) for \(\alpha&lt;\nu\) inside \(\bID^i_{\alpha+1}(\cO)\). As \(\bID_{\alpha}\) can be reduced to \(\PL_{\alpha}\) this brought about the reduction. Ordinal analyses for theories of iterated inductive definitions, first for finite and then also for transfinite iterations, were obtained by Pohlers using Takeuti’s reduction procedure for \(\Pi_1^1\)-comprehension (see Pohlers 1975, 1977). Working independently, Buchholz (1977a) used a new type of rules, dubbed \(\Omega_{\mu+1}\)-rules to recapture these results without use of Takeuti’s methods. These rules are an extension of the Ω-rule described in  Definition C.3.