Herbrand Game Complexity
Abstract
The Student-Teacher game is an extension of Herbrand's theorem. In the game, Student and Teacher take turns giving values for existentially and universally quantified variables, and Student is allowed to backtrack to propose other values for existentially quantified variables. The game has become increasingly important for proving lower bounds on provability in theories of bounded arithmetic. In those applications, the game is played in an arithmetical theory; however, this paper studies the Student-Teacher game in the setting of pure first-order logic, so it is more closely related to Herbrand's theorem and the midsequent theorem. When played in pure first-order logic, a prenex formula ϕ is logically valid if and only if there is a Student-Teacher game with a winning strategy for Student for establishing ϕ. We present a refined version of the Student-Teacher game in arbitrary first-order universal theories and include a proof of the validity of Student-Teacher games from the sequent calculus midsequent theorem in an appendix. The game is presented as a finite tree with vertices and edges labeled by terms, and with a total order on the nodes. The totally ordered tree represents the players' interaction. Our main results show that minimal trees in the Student-Teacher game can be arbitrarily complex. Specifically, for every totally ordered tree T, we construct a valid prenex formula ϕ such that every winning Student-Teacher game for ϕ contains T as a substructure. Using formulas parameterized by numerals, we prove similar results for computable and partial computable sequences of totally ordered trees. It follows not only that there is no computable bound on the size of Herbrand disjunctions, which is a well-known fact, but also that there is no computable bound on their complexity.
Related
- Spatiotemporal Dynamics of Conway's Game of Life in the Entropy--Complexity Plane
- Chevalley-Herbrand formulas and Zp -extensions of a p-principal imaginary quadratic field
- On noncooperative oligopoly equilibrium in the multiple leader–follower game
- Cops and Robber game in higher-dimensional manifolds with spherical and Euclidean metric
- A classification of the Nim-sequences for the two-element subtraction game with a single pass
BibTeX
@misc{buss2026herbrand,
title = {{Herbrand Game Complexity}},
author = {Sam Buss and Pavel Pudlák},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2607.19085},
eprint = {2607.19085},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2607.19085},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Herbrand Game Complexity
AU - Sam Buss
AU - Pavel Pudlák
PY - 2026
DA - 2026/10/16
PB - arXiv
DO - 10.48550/arxiv.2607.19085
UR - https://arxiv.org/abs/2607.19085
AB - The Student-Teacher game is an extension of Herbrand's theorem. In the game, Student and Teacher take turns giving values for existentially and universally quantified variables, and Student is allowed to backtrack to propose other values for existentially quantified variables. The game has become increasingly important for proving lower bounds on provability in theories of bounded arithmetic. In those applications, the game is played in an arithmetical theory; however, this paper studies the Student-Teacher game in the setting of pure first-order logic, so it is more closely related to Herbrand's theorem and the midsequent theorem. When played in pure first-order logic, a prenex formula ϕ is logically valid if and only if there is a Student-Teacher game with a winning strategy for Student for establishing ϕ. We present a refined version of the Student-Teacher game in arbitrary first-order universal theories and include a proof of the validity of Student-Teacher games from the sequent calculus midsequent theorem in an appendix. The game is presented as a finite tree with vertices and edges labeled by terms, and with a total order on the nodes. The totally ordered tree represents the players' interaction. Our main results show that minimal trees in the Student-Teacher game can be arbitrarily complex. Specifically, for every totally ordered tree T, we construct a valid prenex formula ϕ such that every winning Student-Teacher game for ϕ contains T as a substructure. Using formulas parameterized by numerals, we prove similar results for computable and partial computable sequences of totally ordered trees. It follows not only that there is no computable bound on the size of Herbrand disjunctions, which is a well-known fact, but also that there is no computable bound on their complexity.
ER -