ABSTRACT
Recursive progressions of axiomatic theories generated by reflection principles were introduced by A. M. Turing in 1939 and developed by S. Feferman in 1962. This chapter deals with progressions based on weak reflection principles. It introduces the framework of polynomial time (p-related) systems of ordinal notations. The chapter also introduces an indexing for polynomial time computable functions, and proves a polynomial analogue of the Snm Theorem and of the Recursion Theorem relative to the indexing. It explains weak (bounded) reflection principles. These principles are closer to the spirit of bounded arithmetic: they make sense even without reference to actual infinity. Moreover, when dealing with such principles, aspects concerning the complexity of the bounded formulas involved become relevant, and are sometimes connected with unsolved problems in complexity theory.
