赫尔布兰德博弈复杂性
Herbrand Game Complexity
浏览论文内容
中文总结 AI 辅助
研究纯一阶逻辑环境下学生-教师博弈的赫尔布兰德博弈复杂性，给出细化版本，证明其有效性。通过构造前束公式\(\varphi\)，表明该博弈最小树可能任意复杂，得出赫尔布兰德析取大小和复杂性均无界的结论。
中文摘要 AI 辅助
学生-教师博弈是赫尔布兰德定理的扩展。在博弈中，学生和教师轮流为存在量词和全称量词限定的变量赋值，学生可回溯为存在量词限定变量提议其他值。该博弈在证明有界算术理论中可证性的下界时愈发重要。本文在纯一阶逻辑环境下研究此博弈，与赫尔布兰德定理和中序定理联系更紧密。在纯一阶逻辑中，公式\(\varphi\)逻辑有效当且仅当存在学生有获胜策略的学生-教师博弈来确立\(\varphi\)。我们给出任意一阶通用理论中该博弈的细化版本，并在附录中从相继式演算中序定理证明了学生-教师博弈的有效性。博弈表示为有限树，顶点和边由项标记，节点有全序，此全序树代表玩家互动。主要结果表明学生-教师博弈中的最小树可能任意复杂。具体而言，对每个全序树\(T\)，构造一个有效的前束公式\(\varphi\)，使得\(\varphi\)的每个学生-教师博弈都包含\(T\)作为子结构。这不仅表明赫尔布兰德析取的大小无计算上界（这是已知事实），还表明其复杂性无界，即仅根据公式长度无法限制全序树的类型。
英文摘要
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~$φ$ 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 Student-Teacher game for~$φ$ 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.
