[FOM] ZF versus subsystems of Z_2
ali.enayat at gmail.com
Mon Sep 8 19:52:40 EDT 2008
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
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.
More information about the FOM