[FOM] ZF versus subsystems of Z_2

[friedman@math.ohio-state.edu]

In the context of subsystems of second order arithmetic, generally
speaking, formulations are made in terms of natural numbers and sets of
natural numbers - or what is essentially equivalent, using Goedel
numberings.

So Konig's Lemma and weak Konig's Lemma is formulated in terms of sets of
finite sequences of natural numbers, or, equivalently, sets of natural
numbers (finite sequence numbers). There cannot be any axiom of choice
involved in such formulations, as one can normally pick least examples.

Z_2 has has a canonical interpretation in ZF, where integers in Z_2 go to
omega in ZF and sets in Z_2 go to subsets of omega in ZF and epsilon is
preserved.

Harvey Friedman

>
> 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