The paper develops a new logical system for studying a collection of mathematical theories that live between a baseline theory called ACA_0 and a stronger theory called Bar Induction (BI). Bar Induction is a principle from the foundations of mathematics that says, roughly, if you can verify something holds along every infinite path through a tree, you can conclude it holds for the whole tree. The authors build a "reflection calculus" called RC_BI, which is a kind of modal logic where the operators represent saying that a theory is consistent or that it can prove certain statements about arithmetic. The key insight is that by taking the union of a carefully chosen family of such theories, you recover exactly Bar Induction.
The authors prove two important properties of their system. First, it is arithmetically sound, meaning anything it proves is actually true in the standard mathematical universe. Second, it is complete with respect to a natural class of Kripke models, which are graph-like structures used to give meaning to modal statements about possibility and necessity. This semantic framework gives the authors powerful tools to compare theories against one another in a precise way.
Using this framework, the authors show that the theories expressible in their system are linearly ordered by logical strength, and that this ordering is well-behaved in a technical sense called a pre-wellordering. This lets them carry out an "ordinal analysis" of Bar Induction and its fragments, assigning ordinal numbers that measure how strong each theory is. This mirrors a celebrated earlier analysis of Peano Arithmetic by Beklemishev. As a byproduct, their approach produces a new way of naming and organizing the ordinal numbers up to the Bachmann-Howard ordinal, which is a large ordinal that serves as the benchmark for the strength of Bar Induction, and this new notation system looks quite different from all previously known representations.