Subsystems of true arithmetic and hierarchies of functions

AbstractRatajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic 64 (1993) 95–152. The combinatorial method coming from the study of combinatorial sentences independent of PA is developed. Basing on this method we present the detailed analysis of provably recursive functions associated with higher levels of transfinite induction, I(εα), and analyze combinatorial sentences independent of I(εα). Our treatment of combinatorial sentences differs from the one given by McAloon [18] and gives more natural sentences. The same method give also a combinatorial technique with no use of the cut-elimination theorem which is appropriate to study proof-theoretic strength of subsystems of first order arithmetic and some of their expansions. It was used to analyze iterated reflection principle and system of transfinite induction with a satisfaction class