[FOM] ZF versus subsystems of Z_2

[Timothy Y. Chow]

Does ZF prove everything that Z_2 does?  I would think not, because 
various choice principles are provable in Z_2, whereas I believe that ZF 
does not even prove Koenig's lemma.  On the other hand, I didn't think 
Brouwer's fixed-point theorem required AC, so clearly I'm confused about 
something.

This question occurred to me when reading Tim Gowers's blog (which I just 
discovered), where he asks (roughly speaking) what we would lose if we 
dropped even countable choice and insisted that allegedly countable sets 
always come equipped with a bijection with N.

http://gowers.wordpress.com/2008/08/10/a-small-countability-question/

Tim