
> 
> **QUESTIONS.**
> 
> 
> (a) What is the formal system $(\Pi^1\_1$-CA)${}+{}$BI?
> 
> 
> (b) 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).


I asked this question [at math.stackexchange](https://math.stackexchange.com/questions/1966781/), but no one knows the answer there.



What is ($\Pi^1_1$-CA)${}+{}$BI? And what is ID${}_\omega$?
BI = Bar Induction.


See <https://www.jstor.org/stable/2270902> for the abbreviation


and


<https://en.wikipedia.org/wiki/Bar_induction> for the definition.


