Ajtai's theorem for $T^2_2(R)$ and pebble games with backtracking

TL;DR

This paper introduces a pebble game with backtracking to analyze provability in bounded arithmetic, establishing new connections between game strategies and logical principles, and demonstrating limitations of Prover's strategies under simplified conditions.

Contribution

It extends pebble game techniques with backtracking to study provability in $T^2_2(R)$, providing new insights into the complexity of logical proofs.

Findings

No winning strategy exists for Prover in the simplified game.

Reduces provability questions in bounded arithmetic to game-theoretic strategies.

Links pebble game strategies to logical unprovability results.

Abstract

We introduce a pebble game extended by backtracking options for one of the two players (called Prover) and reduce the provability of the pigeonhole principle for a generic predicate $R$ in the bounded arithmetic $T^2_2(R)$ to the existence of a particular kind of winning strategy (called oblivious) for Prover in the game. While the unprovability of the said principle in $T^2_2(R)$ is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory $T_2(R)$), up-to-date no methods working for $T^2_2(R)$ directly (in particular without switching lemma) are known. Although the full analysis of the introduced pebble game is left open, as a first step towards resolving it, we restrict ourselves to a simplified version of the game. In this case, Prover can use only two pebbles and move in an extremely oblivious way. Besides, a series of backtracks can be made only once during a play. Under these assumptions, we show that no strategy of Prover can be winning.