Recursion, reflection, and second-order arithmetic

Hilbert's second problem, posed in 1900, was to prove that there are no contradictions in arithmetic; in modern terms his arithmetic corresponds to second-order arithmetic PA_2. Gentzen in 1939 identified the characteristic ordinal of first-order arithmetic PA, which among many other striking results gave a proof that PA isn't contradictory. The extension of Gentzen's analysis to the case of PA_2 is one of the main open problems in proof theory.
The analysis of PA_2 is extremely difficult since PA_2 allows highly non-computable definitions of new sets in terms of the whole universe of sets. In the first part of this project we will develop the connections between PA_2 and higher order recursion on ordinals. The latter is a computational procedure on ordinals, which should open the door to compute the characteristic ordinals of PA_2 and its strong fragments.
Beklemishev originated the approach, where the characteristic ordinal of a theory is computed via the investigation of a suitable reflection algebra. A recent result of James Walsh and the proposer demonstrated that this approach should in principle be applicable to very strong theories. In the second part of the project we will develop a reflection algebra suitable for the ordinal analysis of PA_2.
Within the framework of the project, the proposer plans to mentor two postdocs and two graduate students, as well as to organize a weekly seminar and an annual meeting.