[FOM] ZF versus subsystems of Z_2

[Timothy Y. Chow]

Ali Enayat wrote:
> Question (a) Can ZF prove that the "standard model of second order
> arithmetic" satisfies all the axioms of Z_2?
> 
> ANSWER: Yes, because the comprehension schema is provable in ZF;
> indeed ZF here can be replaced by Z (Zermelo set theory).

Thanks for your reply!

But now I'm confused about something very elementary.  In Simpson's book 
he says that Konig's lemma is provable in ACA_0.  But I thought Konig's 
lemma was equivalent to "a countable union of finite sets is countable," 
which is certainly not provable in ZF.  Why doesn't this contradict what 
you say above?

Something subtle must be going on in the translation between the language 
of arithmetic and the language of set theory.

Tim