[FOM] ZF versus subsystems of Z_2

[Ali Enayat]

This is a reply to the following query of Timothy Y. Chow (Sep 5, 2008).

>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 [...].

1. Simpson's standard reference Subsystems of Second Order Arithemtic
(hereafter referred to as SOSOA) does not include any choice schemata
in the axioms of Z_2 (see p.16 of SOSOA). Moreover, Feferman and Levy
used forcing to show that if ZF is consistent, then there is a model
of Z_2 in which the the choice schema fails (p.298 of SOSOA).

2. Going back to the query, since ZF and Z_2 are couched in different
vocabularies, the query can be formulated (and answered) in the
following ways:

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

Question (b) Can ZF prove that the "standard model of second order
arithmetic" satisfies all the axioms of Z_2 plus the choice scheme?

ANSWER: No, because of the Feferman-Levy result mentioned earlier.

Question (c) Can ZF prove that there is a model M that satisfies all
of the axioms of Z_2 plus the choice scheme?

ANSWER: Yes, because within Godel's constructible universe L, there is
a second order definable well-ordering of the reals (indeed, a
Sigma^1_2 one). So the desired model M is the standard model of second
order arithmetic in the sense of L.

Best regards,

Ali Enayat