Parallelism and Adaptivity in Student-Teacher Witnessing

TL;DR

This work develops a fine-grained framework of Student–Teacher Games to capture witnessing for bounded arithmetic at multiple levels of the polynomial hierarchy. By classifying total search problems by rounds and parallel queries, the authors prove adaptivity and parallelism yield distinct computational powers, enabling separations among theories extending $ extsf{T}^i_2$ and $ extsf{S}^{i+1}_2$. They then unify witnessing theorems model-theoretically, and apply these results to derive conditional separations across the PV1–S1 hierarchy, as well as lift unprovability results for circuit upper and lower bounds to stronger theories like $ extsf{PV}_1+ extsf{BB}( ext{Σ}^b_1)$ and $ extsf{PV}_1+ extsf{LLIND}( ext{sΣ}^b_1)$. Under the standard assumption that the polynomial hierarchy does not collapse, these results show a robust ladder of non-equivalent theories and reinforce the deep connections between proof complexity, bounded arithmetic, and computational hardness. The paper also poses open questions about extending these separations and locating the precise boundary of unprovability across the hierarchy.

Abstract

Student-Teacher Games are a model of computation in which a computationally restricted Student attempts to produce a string satisfying a refutable property, while an all-powerful Teacher refutes incorrect candidates by providing counterexamples. By the classical result of Krajíček, Pudlák, and Takeuti [KPT90], such games capture the witnessing of $\forall\exists\forall$-formulas in bounded arithmetic. In this paper, we introduce subclasses of total search problems in the polynomial hierarchy, classified by the number of rounds and candidate answers per round required for a Student at the corresponding level to solve them. Assuming the polynomial hierarchy does not collapse, we separate these classes for different number of rounds and queries. As applications we obtain the following results: (a) We study theories of bounded arithmetic axiomatized by fine-grained variants of length induction and bounded collection. We prove a general witnessing theorem connecting their $\forall\exists\forall$-consequences to the appropriate classes of Student-Teacher Games. Under the non-collapse of the polynomial hierarchy, we separate these theories. (b) These conditional separations resolve two open problems in bounded arithmetic: one by Buss and Ressayre [Bus85, CK93] on the strength of bounded collection, and one by Pollett [Pol97] on the difference between strict and non-strict double length induction. (c) Finally, we extend the unprovability of circuit upper bounds due to Krajíček and Oliveira [KO17] to the theory $PV_1+BB(Σ^b_1)$, and the unprovability of strong co-nondeterministic circuit lower bounds due to Pich and Santhanam [PS21] to the theory $PV_1+LLIND(sΣ^b_1)$. By the preceding separations, both theories strictly extend $PV_1$ assuming $NP\nsubseteq P/poly$.

Figures (2)

• Figure 1: Partial order of theories between $\mathsf{PV}_1$ and $\mathsf{S}^{1}_2$. There are two hierarchies, one with extensions axiomatised by length induction axioms (right), and one with extensions axiomatised by bounded replacement axioms (left). The levels are for the bounds $\mathsf{poly},\log,\log\log$, etc. Under the hardness assumption $\mathsf{NP}\not\subseteq \mathsf{P}/\mathsf{poly}$, all these theories are distinct. The arrows symbolise the only possible inclusions.
• Figure 2: Summary of the unprovability results. Both results were previously known for the theory $\mathsf{PV}_1$, while we show them for $\mathsf{PV}_1+\mathsf{BB}(\Sigma^b_{1})$ and $\mathsf{PV}_1 + \mathsf{LLIND}(\mathsf{s}\Sigma^b_{1})$. We get unprovability of both results for the theory $\mathsf{PV}_1 + \mathsf{BB}(\mathsf{s}\Sigma^b_{1},\log)$ which lies in the intersection. All the inclusions are strict under the hardness assumption $\mathsf{NP}\not\subseteq \mathsf{P}/\mathsf{poly}$.

Theorems & Definitions (75)

• Definition 1.1
• Definition 1.2: Student--Teacher Game
• Theorem 1.3: KrajicekPS90
• Theorem 1.4
• Theorem 1.5
• Theorem 1.6: General KPT Theorem
• Theorem 1.7
• Theorem 1.8: $\mathsf{S}^i_2$-analogue to KPT krajivcek1992noPudlak92
• Theorem 1.9
• Theorem 1.10