Galvin’s “Racing Pawns” Game, Internal Hyperarithmetic Comprehension, and the Law of Excluded Middle
Chris J. Conidis, Noam Greenberg, Daniel D. Turetsky · Notre Dame Journal of Formal Logic · 2013
We show that the fact that the first player (“white”) wins every instance of Galvin’s “racing pawns” game (for countable trees) is equivalent to arithmetic transfinite recursion. Along the way we analyze the satisfaction relation for infinitary formulas, of “internal” hyperarithmetic comprehension, and of the law of excluded middle for such formulas.