{"id":"arxiv/2607.19085","url":"https://arxiv.org/abs/2607.19085","tags":["math.LO"],"score":0,"title":"Herbrand Game Complexity","domain":"math.LO","source":"arxiv","authors":["Sam Buss","Pavel Pudlák"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-21","reactions":{}}