[FOM] ZF versus subsystems of Z_2

[Alberto Marcone]

Timothy Y. Chow ha scritto:
> 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.
> 

Something is indeed going on.
One should keep in mind that in the language of second order arithmetic 
one speaks only of subsets of the natural numbers.
This implies that Konig's Lemma applies only to trees of (appropriately 
coded) finite sequences of natural numbers.
Therefore in ACA_0 (or any other subsystem of second order arithmetic) 
from Konig's Lemma one can only prove "a countable union of finite sets 
of natural numbers is countable", which is surely provable in ZF.

Something similar happens also with the choice principles provable in 
second order arithmetic of its subsystems: one should always keep in 
mind that when these statements are translated into the language of set 
theory all set quantifiers should be restricted to subsets of the 
natural numbers.

I hope this helps.

Best,
Alberto
-- 
Alberto Marcone                            alberto.marcone at dimi.uniud.it
Dip. di Matematica e Informatica
Universita' di Udine                                tel: +39-0432-558482
via delle Scienze 206                               fax: +39-0432-558499
33100 Udine
Italy                       http://users.dimi.uniud.it/~alberto.marcone/