Reduction Games, Provability, and Compactness
Status: published in the Journal
of Mathematical Logic 22 (2022) 2250009.
Availability: journal
version and preprint
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.
drh@math.uchicago.edu