Reflection Algebras for Predicative Extensions of Peano Arithmetic

We will give a brief introduction to the problems of ordinal analysis, a branch of proof theory related to the study of the correspondence between axiomatic systems and some explicitly given countable well-orderings. The foundations of this theory were laid in the works of G. Gentzen in the 1930s and have since been significantly developed.
The ideas of an algebraic approach to ordinal analysis arose in the early 2000s. The key role in it is played by algebraic structures on sets of sentences of one or another formal language, called reflection algebras. However, the use of such methods has so far been limited to relatively weak systems of axioms of the arithmetic of natural numbers. In this paper, these methods are extended to a much wider class of axiomatic theories in which the main theorems of mathematical analysis (the so-called predicative theories) can be proved.

References

1. Lev D. Beklemishev, Fedor N. Pakhomov, “Reflection algebras and conservation results for theories of iterated truth”, Ann. Pure Appl. Logic, 173:5 (2022)