 The next challenge after \((\Delta^1_2{\Hy}\bCA)\) was posed by the theory \((\Delta^1_2{\Hy}\bCA)+{{\BI}}\). Its treatment not only required a considerably stronger ordinal representation system but also coincided with a shift away from \(\cL_2\) theories and theories of iterated inductive definitions to a direct proof-theoretic treatment of set theories. Pioneering work on the proof theory of set theories is mainly due to Jäger (1980, 1982). The analysis of \((\Delta^1_2{\Hy}\bCA)+{{\BI}}\) in Jäger &amp; Pohlers 1982 provides a particularly nice application of this new approach which has been called admissible proof theory, owing to its concern with theories extending Kripke-Platek set theory by axioms asserting the existence of admissible sets (for some details see  Appendix D.1).