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 n , an n-bit string x such that M (x) ̸ = A(x). Many recent breakthroughs in lower bounds and derandomization, like the algorithmic method [12], rely on constructive separations as a core component. Chen, Jin, Santhanam, and Williams [14] 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" in terms of C-Student-Teacher Games, where the C-refuter (Student) is allowed to adaptively propose candidate counterexamples xi to an omniscient Teacher. If xi fails to witness an error, Teacher reveals a counterexample yi to the statement "xi is a counterexample to the statement 'M decides A' " -the nature of yi 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 [39], then NP ̸ ⊂ SIZE[n k ] for every k.

• If there is a uniform AC 0 [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 n c strings.

Our results imply a conditional separation of Jeřábek's theory VAPC from V 1 , a theory equivalent to Buss's theory S 1 2 . This improves and significantly simplifies the work of Ilango, Li, and Williams [25], 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.