Parallelism and Adaptivity in Student-Teacher Witnessing

1. Problem Statement and Motivation

The paper addresses fundamental open problems in Bounded Arithmetic, specifically concerning the hierarchy of theories between $PV_1$ (a weak theory capturing polynomial-time reasoning) and $S^1_2$ (a theory capturing polynomial-time reasoning with length induction).

The core issues are:

1. Separation of Theories: It is known that $T^i_2 \subseteq S^{i+1}_2$, but it is an open question whether these inclusions are strict under standard complexity assumptions. Specifically, the paper investigates the strength of two specific axiom schemes:
   • Bounded Replacement ($BB$): Also known as the collection axiom, allowing the exchange of bounded quantifiers.
   • Length Induction ($LIND$) vs. Double Length Induction ($LLIND$): The paper investigates whether induction on "strict" formulas (where sharply bounded quantifiers are pushed inward) is equivalent to induction on general formulas, and how these relate to the replacement axiom.
2. Unprovability Results: The authors aim to lift known unprovability results regarding circuit complexity (specifically circuit upper bounds and average-case lower bounds) from the weak theory $PV_1$ to stronger theories.
3. The Witnessing Gap: Existing separation results often rely on specific cryptographic assumptions (e.g., factoring hardness) or only apply to the first level of the hierarchy. The authors seek a unified framework based on worst-case complexity assumptions (non-collapse of the polynomial hierarchy) to separate these theories across all levels.

2. Methodology: Student-Teacher Games

The central technical tool is the Student-Teacher Game, a computational model derived from the KPT witnessing theorem (Krajíček, Pudlák, Takeuti).

• The Model: A "Student" (a computationally restricted function) attempts to find a witness for an existential quantifier in a $\forall\exists\forall$ formula. A "Teacher" (an oracle) provides counterexamples if the Student's guess is wrong.
• Parameters: The authors classify search problems based on two dimensions:
  1. Adaptivity (Rounds, $r$): The number of interaction rounds between Student and Teacher.
  2. Parallelism (Queries, $q$): The number of candidate answers the Student can submit simultaneously in a single round.
• Complexity Classes: They define classes $ST\Sigma^p_i[r(n), q(n)]$ representing total search problems solvable by a Student in the $i$-th level of the polynomial hierarchy using $r$ rounds and $q$ parallel queries.

Key Technical Insight: The authors prove that adaptivity (adding a round) and parallelism (adding queries) are distinct sources of computational power. Neither can be fully substituted by the other, even with polynomial blow-ups.

3. Key Contributions and Results

A. Separation of Student-Teacher Classes

The authors establish strict separations between the defined classes under the assumption $\Sigma^p_{i+1} \not\subseteq \Delta^p_{i+1}/poly$ (a standard worst-case hardness assumption):

1. Adaptivity is Irreplaceable: Even with a polynomial number of parallel queries ($q$), a Student with $r$ rounds cannot solve problems solvable by a Student with $r+1$ rounds (Theorem 1.4).
   • Implication: $ST[r+1, 1] \not\subseteq ST[r, \text{poly}]$.
2. Parallelism is Irreplaceable: A Student with $r$ rounds and $q$ queries cannot solve problems solvable by a Student with fewer total "query-equivalents" ($r'q' < rq$), provided $r \ge 2$ (Theorem 1.5).
   • Implication: $ST[2, q-1] \subsetneq ST[2, q]$.

B. Generalized Witnessing Theorems

The paper provides a unified model-theoretic framework (Theorem 4.6) to map axioms in Bounded Arithmetic to specific Student-Teacher classes:

• Bounded Replacement ($BB$): Corresponds to constant rounds but polynomial parallel queries.
  • $T^i_2 + BB(\Sigma^b_{i+1}) \implies ST[r=O(1), q=\text{poly}]$.
• Length Induction ($LIND$): Corresponds to polynomial rounds but constant queries.
  • $S^{i+1}_2 \implies ST[r=\text{poly}, q=1]$.
• Double Length Induction ($LLIND$): Corresponds to polylogarithmic rounds and constant queries (for strict formulas).
  • $T^i_2 + LLIND(s\Sigma^b_{i+1}) \implies ST[r=\text{polylog}, q=1]$.
• Fine-Grained Variants: The authors introduce axioms $BB(\Sigma^b_{i+1}, b)$ and $LIND(\Sigma^b_{i+1}, b)$ where $b(n)$ is a sublinear function (e.g., $\log n, \log \log n$). These map to classes with $q=\text{poly}(b)$ or $r=\text{poly}(b)$ respectively.

C. Separation of Theories

Using the witnessing theorems and the class separations, the authors prove that various extensions of $T^i_2$ are distinct under the assumption $\Sigma^p_{i+1} \not\subseteq \Delta^p_{i+1}/poly$:

1. Hierarchy of Replacement: $T^i_2 + BB(s\Sigma^b_{i+1}, b_2) \not\vdash BB(s\Sigma^b_{i+1}, b_1)$ if $b_1$ grows significantly faster than $b_2$ (Theorem 1.9).
2. Hierarchy of Induction: $T^i_2 + LIND(s\Sigma^b_{i+1}, b_2) \not\vdash LIND(s\Sigma^b_{i+1}, b_1)$ (Theorem 1.10).
3. Independence of Schemes:
   • No theory in the $BB$ hierarchy includes any theory in the $LIND$ hierarchy (Theorem 1.11).
   • Specifically, $T^i_2 + BB(\Sigma^b_{i+1})$ does not prove $LIND(s\Sigma^b_{i+1})$, and $T^i_2 + LIND(s\Sigma^b_{i+1}, \log)$ is independent of $T^i_2 + BB(\Sigma^b_{i+1}, \text{poly})$.
4. Resolution of Open Problems:
   • Buss & Ressayre: Confirms that $S^i_2 \subsetneq S^i_2 + BB(\Sigma^b_{i+1}) \subsetneq S^{i+1}_2$ is a proper hierarchy.
   • Pollett: Confirms that $LLIND$ on strict formulas is strictly weaker than $LLIND$ on general formulas.

D. Lifting Unprovability Results

The authors apply their framework to strengthen two major unprovability results:

1. Circuit Upper Bounds: The result that $PV_1 \nvdash P \subseteq SIZE[n^k]$ (Krajíček-Oliveira) is lifted to $PV_1 + BB(\Sigma^b_1)$.
2. Average-Case Lower Bounds: The result that $PV_1 \nvdash NSubExp \not\subseteq Avg\text{-}coNSIZE[2^{n^\delta}]$ (Pich-Santhanam) is lifted to $PV_1 + LLIND(s\Sigma^b_1)$.
3. Intersection: They identify a theory $PV_1 + BB(s\Sigma^b_1, \log)$ (which is stronger than $PV_1$ but weaker than the previous two) where both unprovability results hold simultaneously.

4. Significance

• Unified Framework: The paper provides a single, coherent framework (Student-Teacher Games with varying adaptivity and parallelism) to analyze and separate a wide range of Bounded Arithmetic theories, moving away from ad-hoc model-theoretic arguments.
• Worst-Case Assumptions: Unlike previous separation results that relied on specific cryptographic assumptions (e.g., factoring hardness), these results rely on the standard worst-case assumption that the polynomial hierarchy does not collapse ($\Sigma^p_{i+1} \not\subseteq \Delta^p_{i+1}/poly$).
• Fine-Grained Complexity: The work establishes a precise correspondence between logical axioms (induction vs. replacement, strict vs. non-strict) and computational resources (rounds vs. parallel queries), offering a new lens on the structure of the polynomial hierarchy.
• Meta-Mathematics of Complexity: By lifting unprovability results to stronger theories, the paper demonstrates that these fundamental limits of circuit complexity are robust even when the underlying logical theory is significantly strengthened, provided the theory remains within the bounds of the Student-Teacher game classes defined.

In summary, the paper resolves long-standing open questions about the relative strength of induction and replacement axioms in Bounded Arithmetic by introducing a novel complexity-theoretic classification of witnessing games, proving that adaptivity and parallelism are distinct and non-interchangeable resources.