Classification theorem for propositional provability logics is proved. A characterization of restricted induction rules in arithmetic in terms of iterated reflection principles is obtained. Classes of provably total computable functions for fragments of arithmetic with parameter-free induction are characterized. In particular, parameter-free induction for Π2-formulas corresponds to the class of primitive recursive functions. An approach to the theory of proof-theoretic ordinals on the basis of a notion of provability algebra is suggested.
Main publications:
L. D. Beklemishev, “On the classification of propositional provability logics”, Izv. Akad. Nauk SSSR Ser. Mat., 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
L. D. Beklemishev, “Reflection principles and provability algebras in formal arithmetic”, Uspekhi Matematicheskikh Nauk, 60:2 (2005), 3–78; English transl. Russian Mathematical Surveys, 60:2 (2005), 197–268
; English transl. Math. USSR-Izv., 35:2 (1990), 
ISTINA
