What is ($\Pi^1_1$-CA)${}+{}$BI? And what is ID${}_\omega$? What is the formal system ($\Pi^1_1$-CA)${}+{}$BI? And what is ID${}_\omega$, the formal theory of $\omega$-times iterated inductive definitions?
They are both mentioned in the following paper without any further explanations:
W. Buchholz, An independence result for (Pi^1_1-CA)+BI, Annals of Pure and Applied Logic 33, 131-155, 1987.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.573.420&rep=rep1&type=pdf
 A: $\Pi^1_1$-CA + BI is the system $\Pi^1_1$-CA (a subsystem of second order arithmetic called $\Pi^1_1$ comprehension axiom, which is studied in reverse mathematics ) plus BI which stays for Bar Induction schema
Suppose $\prec$ is a two-place relation symbol defined on a set $X$ and $F(a)$ is an arbitrary $\mathcal{L}_2$-formula. We define:
$Prog(\prec; F) := \forall x[\forall y(y \prec x \rightarrow F(y)) \rightarrow F(x)] \text{(progressiveness)}$
$TI(\prec; F) := Prog(\prec; F) \rightarrow \forall xF(x) \text{(transfinite induction)}$
$WF(\prec) := \displaystyle (\forall S \subseteq X)[S\neq \emptyset \implies (\exists m\in S)(\forall s\in S)\lnot (s\prec m)]\text{(well-foundedness)}$
In other words well-foundedness means that every non-empty subset $S \subseteq X$ has a minimal element with respect to $\prec$.
Bar Induction  is the axiom schema consisting of all formula with the form
$WF(\prec)\rightarrow TI(\prec,F)$
where $\prec$ is an arithmetical relation and $F(a)$ is an arbitrary $\mathcal{L}_2$-formula.
I took this definition from the PhD thesis of Ian Alexander Thomson: Well-Ordering Principles and $\Pi^1_1$-Comprehension + Bar Induction (In this document well-foundedness is defined as $WF(\prec) := \forall YTI(\prec;Y)$, I don't know this definition and I cannot say much about it)
For additional information you can check wikipedia and also this link where they provide a definition of bar induction in terms of finite sequences of natural numbers and infinite tree.
ID$_\omega$ is one example of Systems of iterated inductive definitions, a class of formal systems. Check this link for more details.
You can also check the following book:
Buchholz, Feferman, Pohlers and Sieg: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics 897 (1981)
ID$_\omega$ is proof theoretic equivalent to $\Pi^1_1$-CA + BI (and also to KPl, which is the KP (Kripke–Platek set theory) asserting "the universe is a limit of admissible sets").
Their proof theoretic ordinal is the Takeuti-Feferman–Buchholz  ordinal $\psi_0(\varepsilon_{\Omega_{\omega}+1})$ expressed with the Buchholz's psi collapsing function.
This ordinal is also the limit of the Buchholz's psi collapsing function notation.
