Iterated $\omega$-model reflection and $\Pi^1_2$ proof-theoretic analysis

This is a joint work with James Walsh.
From works of Schmerl and Beklemishev it is known that transfinite iterations of reflection principles in first-order arithmetic provide a powerful tool for proof-theoretic analysis of fragments of first-order arithmetic. In this talk I'll present a study of certain reflection principles in the language of second-order arithmetic that give a new method of proof-theoretic analysis of theories of meta-predicative strength range ($\mathrm{ATR}_0$ and some moderately stronger systems of second-order arithmetic). We consider the principles of uniform $\Pi^1_n$-reflection as well as uniform $\Pi^1_n$ $\omega$-model reflection and establish a number of connections between them. This allows us to calculate proof-theoretic ordinals of certain theories expressed in the terms of these reflection principles. An interesting feature of our approach is that we assign to theories T under consideration their proof-theoretic dilators D such that D(ot(≺))=|T+WO(≺)|. In addition to the calculation of $\Pi^1_1$, $\Pi^0_2$, and $\Pi^0_1$ proof-theoretic ordinals, our approach allows at the same time to find well-ordering principles corresponding to the analyzed systems.