[FOM] Determinacy and WKL_0

[Dmytro Taranovsky]

There is an impressive hierarchy of determinacy hypotheses, each
equivalent to a set existence axiom.  A new addition is
Theorem:  Determinacy of open games on {0, 1} is equivalent to the Weak
Konig Lemma over RCA_0.

By contrast, determinacy of open (or just clopen) games on integers
(arbitrary integers rather than just zeroes and ones allowed as moves)
is equivalent to ATR_0, a much stronger hypothesis.

The proof of the theorem illustrates determinacy and reverse
mathematics.

If the second or closed player does not have a winning strategy, then
his tree of partial strategies (at level n of the tree are complete and
non-losing strategies for the first n moves) does not have an infinite
path.  By WKL_0, the tree is finite, which implies a winning strategy
for the first player.

To get the reversal, let x be a real number, and g code a partial
recursive-in-x function with range {0, 1}.  It suffices to show that g
can be extended to a total function f with range {0, 1}.

If we require the second player to play such an f, then a winning
strategy for him implies the required separation.  By modifying the
game, we can prevent the first player from having a winning strategy:
Both players play a candidate f, the nth move being f(n).
Simultaneously g is being simulated.  The first player wins if for some
n, the second player's moves are inconsistent with g as witnessed by n
stages of the simulation, but the first player's moves are consistent
with g below n stages of the simulation.

A candidate winning strategy for the first player can be "stolen":  The
second player duplicates the moves of the first player until a false
move is played, then (if that happens) plays consistently until the
falsehood is witnessed by the simulation, and plays arbitrarily after
that, winning the game.

On the other hand, the required f can be extracted from a winning
strategy for the second player.  By induction on n, build the maximal
tree of binary sequences such that an n-tuple t is in the tree iff there
is s in the tree such that t is the response to s played under the
strategy.  Finally, pick an arbitrary branch through the tree.

>From the proof, note that WKL_0 is also equivalent to determinacy of
just clopen games on {0, 1}, that is games where for each infinite play,
a winning condition is triggered at a finite stage.   Without the Weak
Konig Lemma, one cannot show that all clopen games on {0, 1} are finite.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm