A Reflection Calculus for Bar Induction and the Linearity of Consistency Strength Ordering
We introduce a novel extension of reflection calculus, $\mathsf{RC_{BI}}$, to analyze a family of extensions of $\mathsf{ACA}_0$ generated by uniform $\omega$-model and syntactic reflection principles, together with several other related operators. The union of these theories coincides with the theory of Bar Induction...