归约博弈、可证明性和compactness
Reduction games, provability, and compactness
摘要：
Hirschfeldt和Jockusch（2016）引入了一个两人博弈，其中一个或另一个玩家的获胜策略恰好对应于$Π^1_2$原则对$ω$ -$\mathsf{RCA}_0$模型之间的隐含和非隐含。他们还介绍了这个游戏的一个版本，类似地捕获了$\mathsf{RCA}_0$的可证明性。我们推广和扩展这个博弈论的框架，以其他形式的系统，并建立了一定的紧凑性结果表明，如果两个原则之间的含义$\mathsf{Q} \to \mathsf{P}$持有，那么存在一个获胜的策略，取得胜利的一些动作的数量由一个独立的具体运行的游戏。这个紧性结果推广了H.~ Wang（1981），并应用于组合原理的逆向数学。我们还展示了这个框架如何导致一种新的分析的逻辑强度的数学问题，完善了逆向数学和计算理论的概念，如Weihrauch约简，允许一种精细的结构比较之间的$Π^1_2$原则，具有计算理论和证明理论方面，并可以帮助我们区分这些，例如，通过表明在证明中对原理的某种使用是“纯证明理论的”，而不是依赖于其可计算性理论的强度。我们给出了这种分析的例子，一些原则在$\mathsf{B}Σ^0_2$的水平，揭示他们的逻辑优势之间的新的差异。
英文摘要：
Hirschfeldt and Jockusch (2016) introduced a two-player game in which winning strategies for one or the other player precisely correspond to implications and non-implications between $Π^1_2$ principles over $ω$-models of $\mathsf{RCA}_0$. They also introduced a version of this game that similarly captures provability over $\mathsf{RCA}_0$. We generalize and extend this game-theoretic framework to other formal systems, and establish a certain compactness result that shows that if an implication $\mathsf{Q} \to \mathsf{P}$ between two principles holds, then there exists a winning strategy that achieves victory in a number of moves bounded by a number independent of the specific run of the game. This compactness result generalizes an old proof-theoretic fact noted by H.~Wang (1981), and has applications to the reverse mathematics of combinatorial principles. We also demonstrate how this framework leads to a new kind of analysis of the logical strength of mathematical problems that refines both that of reverse mathematics and that of computability-theoretic notions such as Weihrauch reducibility, allowing for a kind of fine-structural comparison between $Π^1_2$ principles that has both computability-theoretic and proof-theoretic aspects, and can help us distinguish between these, for example by showing that a certain use of a principle in a proof is "purely proof-theoretic", as opposed to relying on its computability-theoretic strength. We give examples of this analysis to a number of principles at the level of $\mathsf{B}Σ^0_2$, uncovering new differences between their logical strengths.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
