vix.ing · top · new · best · stats

Reduction games, provability, and compactness

2020/08/03 by Damir D. Dzhafarov, Dzhafarov, Damir D., Denis R. Hirschfeldt +3
Computer Science · Mathematics · #Benford’s Law and Fraud Detection #Complexity and Algorithms in Graphs #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #math.LO

paper · pdf · doi:10.48550/arxiv.2008.00907

Accepted for publication in Journal of Mathematical Logic

openalex publication_date 2020/08/03 · arxiv created 2021/12/01 · arxiv updated 2021/12/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01

Abstract

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 Π12 principles over ω-models of RCA0. They also introduced a version of this game that similarly captures provability over RCA0. We generalize and extend this game-theoretic framework to other formal systems, and establish a certain compactness result that shows that if an implication Q → 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 Π12 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 BΣ02, uncovering new differences between their logical strengths.

Related