Games with backtracking options corresponding to the ordinal analysis of $PA$

Abstract

We give another proof of ordinal analysis of $I{\Sigma }_k$-fragments of Peano Arithmetic which is free from cut-elimination of $\omega$-logic. Our main tool is a direct witnessing argument utilizing game notion, motivated from the realm of proof complexity and bounded arithmetic.

36 pages, figures added, Corollary 4.13 added, revisiting characterization of provably total recursive functions of IΣ_k and that of dynamic ordinal analysis are removed for simplicity, presentation improved