Доказана теорема о классификации пропозициональных логик доказуемости. Получена характеризация ограниченных правил индукции в арифметике в терминах итерированных схем рефлексии. Найдены классы доказуемо тотальных вычислимых функций для фрагментов арифметики с беспараметрической индукцией. В частности, беспараметрическая индукция для Π2-формул соответствует классу примитивно рекурсивных функций. Предложен подход к ординальной теории доказательств на основе понятия алгебры доказуемости.
Основные публикации:
Л. Д. Беклемишев, “О классификации пропозициональных логик доказуемости”, Изв. АН СССР, сер. матем., 53:5 (1989), 915–943; English transl. Math. USSR-Izv., 35:2 (1990), 247–275
L. D. Beklemishev, “Iterated local reflection versus iterated consistency”, Ann. Pure Appl. Logic, 75 (1995), 25–48
L. D. Beklemishev, “A proof-theoretic analysis of collection”, Arch. Math. Logic, 37:5-6 (1998), 275–296
L. D. Beklemishev, “Parameter-free induction and provably total computable functions”, Theoret. Comput. Sci., 224 (1999), 13–33
Л. Д. Беклемишев, “Схемы рефлексии и алгебры доказуемости в формальной арифметике”, Успехи математических наук, 60:2 (2005), 3–78; English transl. Russian Mathematical Surveys, 60:2 (2005), 197–268
; English transl. Math. USSR-Izv., 35:2 (1990), 
ИСТИНА
