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.

翻译：我们为双人卵石游戏中的一方（称为证明者）引入了回溯选项，并将有界算术理论$T^2_2(R)$中关于一般谓词$R$的鸽巢原理的可证性，约化为证明者在该游戏中存在一类特定获胜策略（称为遗忘策略）的问题。尽管该原理在$T^2_2(R)$中的不可证性是Ajtai著名定理（针对更强理论$T_2(R)$）的直接推论，但迄今为止，尚未出现能直接适用于$T^2_2(R)$的方法（尤其是不依赖切换引理的方法）。虽然对所引入卵石游戏的完整分析仍有待解决，但作为迈向该目标的第一步，我们仅限于研究该游戏的简化版本。在此简化版本中，证明者仅能使用两枚卵石，且必须以极度遗忘的方式移动。此外，在一局游戏中仅允许执行一次连续回溯操作。基于这些假设，我们证明了证明者不存在任何获胜策略。