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 formula~$\varphi$ is logically valid if and only if there is a Student-Teacher game with a winning strategy for Student for establishing~$\varphi$. 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~$\varphi$ such that every Student-Teacher game for~$\varphi$ contains $T$ as a substructure. 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 bound on their complexity in the sense that it is not possible to restrict the types of totally ordered trees knowing only the length of the formula.