Countable inductive definitions in AST Athanossios Tzouvaras (1986) Commentationes Mathematicae Universitatis Carolinae
Cut elimination for impredicative infinitary systems. Part II Ordinal analysis for iterated inductive definitions. W. Pohlers (1982) Archiv für mathematische Logik und Grundlagenforschung
Cut-elimination for impredicative infinitary systems. Part I. Ordinal-analysis for ID1. W. Pohlers (1981) Archiv für mathematische Logik und Grundlagenforschung