Ajtai's theorem for T²₂(R) and pebble games with backtracking

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²₂(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²₂(R) is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory T₂(R)), up-to-date no methods working for T²₂(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.