Parallelism and Adaptivity in Student-Teacher Witnessing

TL;DR

This paper introduces a new framework using Student-Teacher Witnessing Games to analyze bounded arithmetic, leading to separations of complexity classes and resolving open problems in the field.

Contribution

It defines subclasses of total search problems in the polynomial hierarchy based on game rounds, and applies this to prove separations and unprovability results in bounded arithmetic.

Findings

Separated classes of total search problems based on game rounds.

Resolved open problems on the strength of bounded collection and induction.

Extended unprovability results to new theories assuming NP not in P/poly.

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\'i\v{c}ek, Pudl\'ak, 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\'i\v{c}ek and Oliveira [KO17] to the theory $PV_1+BB(\Sigma^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\Sigma^b_1)$. By the preceding separations, both theories strictly extend $PV_1$ assuming $NP\nsubseteq P/poly$.