 He not only introduced theories of one inductive definition but also of \(\nu\)-times transfinitely iterated inductive definitions, \(\bID_{\nu}\). Albeit it soon became clear that even the theories \(\bID_{\nu}\) couldn’t reach the strength of \(\bZ_2\) (in point of fact, such theories are much weaker than the fragment of \(\bZ_2\) based on \(\Pi^1_2\)-comprehension); they became the subject of proof-theoretic investigation in their own right and occupied the attention of proof theorists for at least another 15 years. One reason for this interest was surely that the intuitionistic versions corresponding to the accessible (i.e., well-founded) part of a primitive recursive ordering are immediately constructively appealing and a further reason was that they were thought to be more amenable to direct proof-theoretic treatments than fragments of \(\bZ_2\) or set theories.