Witnessing flows in arithmetic

Abstract One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in PA+ TI (_{}), the extension of Peano arithmetic by transfinite induction up to the ordinals below. Roughly speaking, we identify the functions as the ones that are computable by a sequence of PV -provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below, decreasing by the modifications. In the second part, and choosing l k, we use similar technique to capture the functions with bounded definitions in the theory Tᵏ₂ (resp. Sᵏ₂) as the functions computable by exponentially (resp. polynomially) long sequence of PV₊-₋ +₁ -provable reductions between l -turn games starting with an explicit PV₊-₋ +₁ -provable winning strategy for the first game.