[FOM] Conway's Angel and Devil problem

[Timothy Y. Chow]

Conway's angel/devil problem was first published, I believe, in Winning 
Ways some 25 years ago.  A nice description of the problem may be found in 
Wikipedia.

http://en.wikipedia.org/wiki/Angel_problem

The problem remained unsolved until recently, when four (!) independent 
and almost simultaneous solutions appeared, showing that the angel wins.

I have a reverse mathematics question related to this problem.  Say that 
the devil wins if for some n, the devil wins in at most n steps.  Say that 
the angel wins if it has a strategy that allows it to survive infinitely 
many steps.  What is needed to prove the following?

  (*) Either the angel or the devil has a winning strategy.

Now that the angel/devil problem has been solved, the solutions can 
probably be used to prove (*) in RCA_0 or even something weaker, by 
"cheating" and proving the appropriate disjunct directly.  So I guess my 
question is not a "pure" reverse mathematics question in the sense that we 
don't expect (*) to reverse over an interesting base theory to an 
interesting axiom.  However, I think it's clear what my intended question 
is---what do we need to give a simple proof of (*), or what do we need to 
prove a suitable generalization of (*) to arbitrary games similar to this 
one, etc.?

My first thought was the weak Koenig lemma, but Jeff Hirst convinced me 
that because the devil's possible moves are unbounded, WKL_0 may not 
suffice.

Tim