Galvin's ``racing pawns'' game, internal hyperarithmetic comprehension, and the law of excluded middle (Q1949169)

In Galvin's racing pawns game, players White and Black take turns moving either of two pawns, one white and one black, on a well-founded tree. White moves first and play continues until some pawn is placed on a leaf of the tree. The color of that pawn determines the winner of the game. Galvin proved that White has a winning strategy; see the memoir of \textit{S. B. Grantham} [Mem. Am. Math. Soc. 316, 63 p. (1985; Zbl 0559.90097)]. In this paper, the authors prove that Galvin's theorem for well-founded subsets of \(\omega^\omega\) is equivalent to ATR\(_0\), the subsystem of arithmetical transfinite recursion from reverse mathematics. Thus, this restriction of Galvin's theorem has the same logical strength as determinacy of open games, as discussed in [\textit{S. G. Simpson}, Subsystems of second order arithmetic. 2nd ed. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Logic (2009; Zbl 1181.03001)]. A formulation of the law of the excluded middle in infinitary propositional calculus and a principle of internal hyperarithmetic comprehension are also shown to be equivalent to ATR\(_0\).