Progressions of Theories of Bounded Arithmetic
Recursive progressions of axiomatic theories generated by reflection principles were introduced by Turing [Tur39] in 1939 and developed by Feferman [Fef62] in 1962. Later, other authors investigated this subject. The contributions which are most closely related to our work are those of Schmerl [Sch79], who studied in depth progressions starting from PRA, and Wilkie [Wil84], who investigated the strength of reflection principles in some weak fragments of arithmetic. Our aim is to develop a polynomial time analog of Feferman’s work about progressions of axiomatic theories. More specifically, we are interested in fragments of bounded arithmetic (cf. Buss [Bus86]), and in bounded reflection principles, and we wish to pay attention to the computational complexity of the algorithms involved; thus, we start from Buss’ S 2 1 and we require that the axiom systems and the functions involved in the definition of our progressions be polynomial time computable. Our choice of S 2 1 as a base theory is motivated by the fact that this system is sensitive to computational aspects and is also one of the weakest fragments in which we have a satisfactory arithmetization of syntax. The first step towards the realization of our project consists of an investigation of the strength of various reflection principles (some are taken from Feferman’s paper, some others are new). For some of these principles, (namely the bounded reflection principles), we investigate the strength of progressions at finite ordinals based on them. A second step consists of an investigation of transfinite progressions of theories by means of these principles; to this end, after introducing a coding of polynomial time computable functions, we define the notion of polynomial time (p-related) system of notations; we develop a system of notations O P (which is a polynomial time analog of Church Kleene’s O C K ) for polynomial time ordinals, in which every recursive ordinal is coded. We investigate other recursion theoretic properties of this system, paying attention to the possibility of formalizing properties of O P inside S 2 1 . In particular, our definition of O P allows for the use of p-inductive definitions (cf. 124 [Bus86]). The next step should be the definition of progressions of theories, (verifiable in S 2 1 or in some other fragment of bounded arithmetic) for each reflection principle, and the study of their relative strength. For the moment, we have not been able to define progressions in O P satisfying at the same time the following conditions: (i) verifiability provably in S 2 1 and (ii) Δ 1 b axiomatizability provably in S 2 1 . However if one considers the syntactic analog of a polynomial time ordinal notation, namely Δ 1 b definitions of polynomial time well orderings, then one can obtain, along the lines of Beklemishev [Bek94], an analog of Feferman’s verifiable progressions of Δ 1 b axiomatizable theories provably in relative to the Δ 1 b formula defining the well ordering. For such progressions, we prove a completeness result which has some analogies with the completeness result of Turing (cf. [Tur39] and [Fef62, Theorem 4.1]) for progressions based on consistency (this result, Theorem 6.9, is an improvement, due to Lev Beklemishev, of a previous result due to the authors); however we also prove an incompleteness result, showing an importance difference between progressions starting from S 2 1 and progressions starting from a strong theory like PA.