Алгебры рефлексии для предикативных расширений арифметики Пеано

В работе Л. Д. Беклемишева и Ф. Н. Пахомова понятие алгебры рефлексии распространено на класс предикативных расширений арифметики Пеано. С его помощью построены системы ординальных обозначений и получены результаты о консервативности для итерированных схем рефлексии, соответствующих уровням гиперарифметической иерархии подмножеств натурального ряда. На основе этих результатов единым методом для ряда предикативных теорий вычислены классы доказуемо тотальных вычислимых функций и $\Pi_1^0$-ординалы, а также порядковые типы доказуемо фундированных рекурсивных вполне упорядоченных множеств. Тем самым, методы алгебраического подхода к теории доказательств перенесены на существенно более широкий класс формальных теорий.
Идеи алгебраического подхода к проблемам теоретико-доказательственного анализа и понятие алгебры рефлексии возникли в начале 2000-х годов. Однако их применение по существу ограничивалось теориями, сформулированными в языке формальной арифметики Пеано, то есть ее фрагментами и относительно слабыми расширениями. Задача распространения этого метода на более широкие классы теорий стояла с тех самых пор (см., например, L. Beklemishev, A. Visser. Problems in the Logic of Provability, 2006), однако на этом пути возникли технические трудности. В данной работе, опирающейся на предыдущее развитие, эти трудности были преодолены.