[FOM] ZF versus subsystems of Z_2

[Ali Enayat]

This is a reply to the following comment/question by Timothy Y. Chow
(Sep 10, 2008)

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

Tim is referring to the following paradox: on one hand, we know that
Konig's Lemma is not provable with ZF alone (since its proof provably
needs a modicum of Choice that is unavailable in ZF, and on the other
hand, ZF proves that the standard model of second order arithmetic
satisfies Z_2, and a fortiori ACA_0, which is known to be sufficient
(as well as necessary) to prove Konig's Lemma.

The paradox is resolved, as Tim suspected, by noting that there are
really two formulations of Konig's lemma at work, one independent of
ZF, and the other provable in ZF:

(KL1) The usual set-theoretic formulation, that says that if (T,<) is
a well-founded infinite tree of height omega, each level of which is
finite, then T has an infinite branch.

(KL2) The formulation in second order arithmetic (p.121 of Simpson's
book) that stipulates that T is a subtree of the tree N^(<N), i.e.,
the tree of all finite sequences of natural numbers (ordered with its
natural ordering).

So the formulation in (KL2) ends up having the aforementioned "modicum
of Choice" built into it, which makes it provable already in ACA_0,
let alone stronger systems such as Z_2 or ZF.

By the way, the precise amount of Choice needed to prove (KL1) is known to be:

(*) Every countably infinite family of finite nonempty sets of has a
choice function.

See the following paper of Forster and Truss for the proof of
equivalence of (KL1) and (*) within ZF (among other things):

Ramsey's theorem and König's lemma.  Arch. Math. Logic  46  (2007),
no. 1, 37--42.

Best regards,

Ali Enayat