Provability in relativized arithmetics and games with backtracking options

Eitetsu Ken

In the realm of propositional proof complexity and bounded arithmetics, the notion of a pebble game gives us a neat way to analyze resolution proof system and \(T^{1}_{2}(R)\).

In this talk, towards a deeper understanding of the method, we consider the relativized arithmetic \(I\Sigma_k(X)\) (\(k \geq 1\)) and a game notion corresponding to it and reprove some classical results of ordinal analysis without cut-elimination for \(\omega\)-logic.

 Overview  Program