  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 $\Pi^1_2$ principles over $\omega$-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
$\Pi^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}\Sigma^0_2$, uncovering new differences between their logical
strengths.
