Student-Teacher Constructive Separations and (Un)Provability in Bounded Arithmetic: Witnessing the Gap

Let C be a complexity class and A be a language. The statement "A λC"is a separation of A from C. A separation is constructive if there is an efficient algorithm called a refuter that prints counterexamples to the statement "M decides A"for every C-algorithm M. Concretely, refuters witness errors of M on A by printing, on input 1ⁿ, an n-bit string x such that M(x) λ A(x). Many recent breakthroughs in lower bounds and derandomization that use the algorithmic method rely on constructive separations as a core component (Chen, Lyu, Williams 2020, for example). Chen, Jin, Santhanam, and Williams (2022) studied the consequences of constructivizing classical non-constructive lower bounds in complexity theory. They showed that (1) constructivizing many known separations would imply breakthrough lower bounds, and (2) some separations are impossible to constructivize. We study a more general notion of "efficient refutation"by C-Student-Teacher Games, where the C-refuter (Student) is allowed to adaptively propose candidate counterexamples x to an omniscient Teacher. If x fails to witness an error, Teacher reveals a counterexample y to the statement "x is a counterexample to the statement 'M decides A' "- the nature of y depending on how the separated language A and complexity class C are defined. We show: If there is a P-Student-Teacher constructive separation of Palindromes from one-tape nondeterministic O(n^{1 + ϵ}) time (Maass 1984), then NP λ.,SIZE[n^k] for every k. If there is a uniform AC⁰[qpoly]-Student-Teacher protocol generating truth tables of super fixed polynomial circuit complexity, then P λ NP. There is no P-Student-Teacher protocol which for infinitely many c>0, generates high-K^nc strings. Our results imply a conditional separation of JeÅ™ábek's theory VAPC from V¹. This improves and simplifies the work of Ilango, Li, and Williams (2023), who separate VAPC from the weaker theory VPV under the existence of indistinguishability obfuscation. We do not use cryptographic assumptions in our separation. Instead we introduce a natural and plausible conjecture on the uniformity of proofs in bounded arithmetic, inspired by Kreisel's Conjecture in logic. We believe this conjecture to be of independent interest.