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

TL;DR

This paper presents a new proof of the ordinal analysis of certain Peano Arithmetic fragments using game-theoretic methods, avoiding traditional cut-elimination techniques.

Contribution

It introduces a novel witnessing argument based on game notions, providing an alternative approach to ordinal analysis of $I ext{-} ext{Sigma}_k$-fragments.

Findings

Provides a cut-elimination free proof of ordinal analysis

Utilizes game-based witnessing arguments from proof complexity

Offers insights into the structure of arithmetic fragments

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.