Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Eitetsu Ken, Mykyta Narusevych

TL;DR

The paper tackles the problem of proving the pigeonhole principle unprovability in bounded arithmetic without resorting to Switching Lemmas by introducing a backtracking pebble game $\\\\mathcal{G}_{2}$ tied to $T^{2}_{2}(R)$. It connects formal proofs to winning strategies for Prover under the notion of obliviousness and analyzes a toy regime with two pebbles and a single backtrack, showing Delayer can win in that setting. The work clarifies how partial assignments of polylogarithmic size and carefully restricted strategies could pave a Switching-Lemma-free path to Ajtai-style lower bounds for $T^{2}_{2}(R)$, bridging proof complexity with bounded arithmetic. It also provides detailed formal apparatus, including propositional translations, equivalent game formulations, and labeling derivations, to support this program and points to open questions about extending the toy-case insights to the full theory.

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.

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

TL;DR

The paper tackles the problem of proving the pigeonhole principle unprovability in bounded arithmetic without resorting to Switching Lemmas by introducing a backtracking pebble game tied to . It connects formal proofs to winning strategies for Prover under the notion of obliviousness and analyzes a toy regime with two pebbles and a single backtrack, showing Delayer can win in that setting. The work clarifies how partial assignments of polylogarithmic size and carefully restricted strategies could pave a Switching-Lemma-free path to Ajtai-style lower bounds for , bridging proof complexity with bounded arithmetic. It also provides detailed formal apparatus, including propositional translations, equivalent game formulations, and labeling derivations, to support this program and points to open questions about extending the toy-case insights to the full theory.

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 in the bounded arithmetic 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 is an immediate consequence of a celebrated theorem of Ajtai (which deals with a stronger theory ), up-to-date no methods working for 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.
Paper Structure (10 sections, 23 theorems, 36 equations, 24 figures)

This paper contains 10 sections, 23 theorems, 36 equations, 24 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A review of unprovability of the pigeonhole principle over $T^{1}_{2}(R)$
  4. A game notion for $T^{2}_{2}(R)$
  5. Analysis of simplified $\mathcal{G}_{2}$
  6. Acknowledgement
  7. Appendix
  8. Our formulation of $T^{2}_{2}(R)$-proofs and its propositional translation
  9. An equivalent formulation of $\mathcal{G}_{2}$
  10. Derivation of labelings

Key Result

Proposition 2.8

Suppose $T^{d}_{2}(R) \vdash ontoPHP^{n+1}_{n}(R)$, where $ontoPHP^{n+1}_{n}(R)$ is a natural formalization of the pigeonhole principle for bijections using $(n+1)$ pigeons and $n$ holes. Then $ontoPHP^{n+1}_{n}$ has $2^{|n|^{O(1)}}$-sized $LK^{*}_{d+\frac{1}{2}, O(1)}$-proofs.

Figures (24)

  • Figure 1: - example of $\mathcal{G}_{F}$
  • Figure 2: - globally consistent path in $\mathcal{G}_{F}$ of length $n$
  • Figure 3:
  • Figure 8:
  • Figure 9: - cover-by-two derived under the assumption $F(3, 1) = 1$
  • ...and 19 more figures

Theorems & Definitions (74)

  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Example 2.4
  • Definition 2.5
  • Remark 2.6
  • Definition 2.7
  • Proposition 2.8: essentially, Corollary 9.1.4 and the proof of Lemma 9.5.1 in Krajicek
  • Remark 2.9
  • Remark 2.10
  • ...and 64 more