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$.

翻译：学生-教师博弈是一种计算模型，其中计算能力受限的学生试图生成满足可证伪性质的字符串，而拥有无限计算能力的教师则通过提供反例来证伪错误的候选解。根据Krajíček、Pudlák和Takeuti的经典结果[KPT90]，此类博弈刻画了有界算术中$\forall\exists\forall$公式的见证机制。本文在多项式层级中引入了全搜索问题的子类，这些子类根据相应层级的学生解决问题所需的轮次和每轮候选答案数量进行分类。假设多项式层级不坍塌，我们分离了具有不同轮次和查询次数的类别。作为应用，我们获得以下结果：（a）我们研究了由细粒度变体的长度归纳和有界收集公理化的有界算术理论。我们证明了一个通用见证定理，将其$\forall\exists\forall$推论与适当类别的学生-教师博弈相关联。在多项式层级不坍塌的前提下，我们分离了这些理论。（b）这些条件性分离解决了有界算术中的两个开放问题：一是Buss和Ressayre[Bus85, CK93]提出的关于有界收集强度的问题，二是Pollett[Pol97]提出的严格与非严格双长度归纳之间的差异问题。（c）最后，我们将Krajíček和Oliveira[KO17]关于电路上界不可证性的结果扩展到理论$PV_1+BB(Σ^b_1)$，并将Pich和Santhanam[PS21]关于强共非确定性电路下界不可证性的结果扩展到理论$PV_1+LLIND(sΣ^b_1)$。根据前述分离结果，在假设$NP\nsubseteq P/poly$的条件下，这两个理论都严格扩展了$PV_1$。