A Reflection Calculus for Bar Induction and the Linearity of Consistency Strength Ordering

We introduce a novel extension of reflection calculus, $\mathsf{R}{\mathsf{C}}_{\mathsf{B}\mathsf{I}}$, to analyze a family of extensions of ${\mathsf{A}\mathsf{C}\mathsf{A}}_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 ($\mathsf{B}\mathsf{I}$). We prove that $\mathsf{R}{\mathsf{C}}_{\mathsf{B}\mathsf{I}}$ is arithmetically sound, and that it is sound and complete with respect to a natural class of Kripke models. Leveraging these modal semantics, we demonstrate that the class of theories denoted by $\mathrm{\nabla }$-free closed formulas is a pre-wellordering with respect to ${\mathrm{\Pi }}_1^1$-soundness and consistency strength. This allows us to establish an ordinal analysis for $\mathsf{B}\mathsf{I}$ and its fragments, analogous to Beklemishev’s analysis of $\mathsf{P}\mathsf{A}$. The structural properties of $\mathsf{R}{\mathsf{C}}_{\mathsf{B}\mathsf{I}}$ naturally give rise to a novel ordinal notation system for the Bachmann-Howard ordinal which differs substantially from existing representations.