# How much Dependent Choice is provable in $Z_2$? And what about Projective Determinacy?

So, second order arithmetic, $$Z_2$$, is capable of proving quite a few things. One thing which would be of use is dependent choice for $$\mathbb{R}$$.

Basically, dependent choice on $$\mathbb{R}$$ says that if we have a game where we pick a sequence of real numbers/moves, and the available set of moves can depend on past choices but is always nonempty, then there's an infinite sequence of legal moves.

A finite sequence of moves can be formalized by some function $$f:\mathbb{N}\to\mathbb{R}\cup\{\bot\}$$ where there's some number where $$f$$ before that point always spits out a real number, and $$f$$ after that point always spits out $$\bot$$. Given a function $$g:\mathbb{N}\to\mathbb{R}$$ (an infinite sequence of moves), let $$g_{\downarrow n}$$ (the first n moves) denote the function that matches $$g$$ but after $$n$$ always returns $$\bot$$.

"$$Z_2$$ proves Dependent Choice for $$\mathbb{R}$$" would be the statement that for all sentences $$\phi$$ definable in second-order arithmetic, $$Z_2$$ proves the statement $$(\forall f\exists r:\phi(f,r))\to\exists g\forall n:\phi(g_{\downarrow n},g(n+1))$$ Dependent Choice for $$\mathbb{R}$$ is true of $$Z_2$$ if, for all $$\phi$$ definable in second-order arithmetic, if $$Z_2$$ proves $$\forall f\exists r:\phi(f,r)$$ then $$Z_2$$ proves $$\exists g\forall n:\phi(g_{\downarrow n},g(n+1))$$

So first question: Is there any better way to formalize the axiom of dependent choice in second-order arithmetic? This might be too narrow.

Now, I'm pretty sure that $$Z_2$$ doesn't prove dependent choice for $$\mathbb{R}$$. And also pretty sure that dependent choice for $$\mathbb{R}$$ isn't true of $$Z_2$$ either. However, there are definitely some formulas where it holds. For instance, $$Z_2$$ proves Weak Konig's Lemma, so if we can prove that $$\phi(f,r)$$ can only be true if $$r=0$$ or $$r=1$$, and we show the nonemptiness property, then that'd show that there's a choice function.

So, second question: How much of Dependent Choice for $$\mathbb{R}$$ can $$Z_2$$ prove? And how much of dependent choice is true of $$Z_2$$?

And, the third question: Projective determinacy is a statement about one player or the other having a winning strategy in games. This seems highly relevant to the axiom of dependent choice. So, if we consider $$Z_2+PD$$, then how much dependent choice do we get?

• Instead of "for all sentences $\phi$ definable in second-order arithmetic" I suggest saying "for all formulas $\phi(f,r)$ expressible in second-order arithmetic", since in the principal case you want $\phi$ to have the free variables $f,r$ and so it is not a sentence but a formula; and also you are expressing it not defining it. Another issue is that your coding of finite sequences of reals is a bit odd, since we can easily code finite tuples of reals (actually subsets of $\mathbb{N}$ in $Z_2$) and even $\omega$-tuples with reals by the usual pairing function methods. Commented Dec 23, 2023 at 23:33
• @JoelDavidHamkins I think the question about PD is answered positively in the final section of Kechris's paper "The Axiom of Determinacy Implies Dependent Choices in $L(\mathbb R)$." Commented Dec 24, 2023 at 0:10
• Alex, I suggest that you call your principle "projective DC". Commented Dec 24, 2023 at 0:12
• @JoelDavidHamkins Sure! Commented Dec 24, 2023 at 0:47
• Aren't your two formulations of a theory $T$ having DC equivalent? If DC is "true of $T,$" then $T$ proves $\phi$-DC by substituting $\psi(f, r):= (\forall g \exists s \phi(g, s)) \rightarrow \phi(f, r).$ This distinction only matters if we restrict DC to a fixed complexity of projective formulas, since $\psi$ has higher complexity than $\phi.$ Commented Dec 24, 2023 at 1:31

The answer to the third question is yes. This is due to Kechris, who showed that $$\text{ACA}_0$$ plus schematic PD implies schematic DC. This appears in the last section of "The Axiom of Determinacy implies Dependent Choice in $$L(\mathbb R)$$."

The idea of the proof is to run Moschovakis's Second Periodicity Theorem (propagation of scales) in the DC-less context. One might hope to prove in this way that every projective set has a projective scale, but in fact this approach does not work directly since one cannot show that the comparison games lead to prewellorders, only that the resulting preorder contains no infinite descending sequences. So instead Kechris proves (roughly by Moschovakis's argument although some extra work is required for the existential case of the induction) that every projective set has a projective quasi-scale, which is like a scale except that prewellorders are replaced by preorders with no infinite descending sequences (see Section 2.5 of the paper). Finally, Kechris proves that any set that carries a definable quasi-scale also contains a definable element (this is the Lemma in Section 2.3), which is different from the corresponding argument for scales! Using this "basis" result, one obtains a constructive way to choose an element from a quasi-scaled set given a projective definition of such a quasi-scale, which lets you prove DC for projective sets.

Here is a natural model $$M$$ of $$Z_2$$ where projective DC fails. Starting with a model of ZFC + $$V=L$$, force over $$L$$ with the Levy collapse $$\mathrm{Coll}(\omega,{<\aleph_\omega})$$ collapsing all ordinals $$<\aleph_\omega$$ to become countable. Let $$G$$ be $$V$$-generic for this forcing. (Of course also $$\aleph_\omega$$ is countable in $$V[G]$$.) Let $$\mathbb{R}^*=\bigcup_{\alpha<\aleph_\omega^V}\mathbb{R}\cap L[G\upharpoonright\alpha]$$. Then $$L(\mathbb{R}^*)$$ is a model of ZF, and $$\mathbb{R}^*$$ is its set of reals, so $$\aleph_\omega=\omega_1^{L(\mathbb{R}^*)}$$. So $$M=\mathcal{P}(\omega)^{L(\mathbb{R}^*)}$$ models second order arithmetic.

Let $$\varphi(x,y)$$ be the projective formula asserting "$$y$$ codes a wellorder of length $$\omega_1^{L[x]}$$". For all $$x\in\mathbb{R}^*$$, there is $$y\in\mathbb{R}^*$$ such that $$\varphi(x,y)$$ holds, but note that there is no length $$\omega$$ sequence through this relation in $$\mathbb{R}^*$$, since such a sequence would collapse $$\omega_1^{L(\mathbb{R}^*)}$$.

• The model you described is due to Truss, by the way. Commented Dec 24, 2023 at 8:55
• Sure. John Truss, Models of set theory containing many perfect sets. Ann. Math. Logic 7, 197-219 (1974) (ZBL0302.02024). Commented Dec 24, 2023 at 19:40
• @Ali: That's a misconception I had for year. But I've realised the key difference is that Truss takes all the bounded reals, and in that model the reals are not a countable union of countable sets, whereas the Feferman–Levy model has the decomposition of the reals in the model. They are very close and fairly similar, but they are different. Commented Jan 3 at 6:59
• @Ali: The Truss model is of the form $L(\Bbb R)$, whereas the Feferman–Levy is not, in short. Commented Jan 3 at 7:01
• @AsafKaragila Thanks for the clarification and correction, I have accordingly modified my answer. Commented Jan 3 at 13:28

As explained below, the "amount" of Dependent choice provable in Second Order Arithmetic is precisely $$\Sigma^1_{2}$$.

$$\mathrm{Z}_2$$ (second order arithmetic) proves $$\Sigma^1_{2}$$-DC (where DC = Dependent Choice),i.e., $$\mathrm{Z}_2$$ proves each instance of the DC scheme in which the $$\phi$$ at work is of complexity at most $$\Sigma^1_{2}$$. This is established in Theorem VII.9.2 of Simpson's book Subsytems of Second Order Arithmetic; the proof employs an adaptation of the Shoenfield absoluteness theorem to the context of second arithmetic.

On the other hand, it is known that the reals of the so-called Feferman-Levy model in which $$\aleph_1$$ is a countable union of countable sets, is a model of $$\mathsf{Z}_2$$ in which $$\Pi^1_2$$-DC fails, indeed, in the Feferman-Levy model, the weaker form of $$\Pi^1_2$$-DC known as $$\Pi^1_2$$-AC fails. In an earlier version of this answer I incorectly asserted that the model described in the answer by Farmer S is the same as the Feferman-Levy model; but that is not the case, as pointed out in Asaf Karagila's comment below.

The Feferman-Levy model (and the aforementioned failure of DC) appear in Theorem 8 in the following paper of Azriel Levy:

Definability in axiomatic set theory. II , Mathematical Logic and Foundations of Set Theory, Proc. Internat. Colloq., Jerusalem, 1968, pp. 129–145, Stud. Logic Found. Math. North-Holland, 1970.

It is worth emphasizing that $$\Pi^1_2$$-DC is unprovable even in the much stronger theory $$\mathrm{Z}_{2}+\Pi^{1}_{\infty}$$-AC. This result appeared in this preprint of Friedman, Gitman, and Kanovei (and published a year later in the Journal of Mathematical Logic). As the authors indicate in the abstract, their work is a rediscovery by the first two authors of a result obtained by the third author in a 1979 paper. The forcing notion employed in the paper is a tree iteration of Jensen’s forcing for building a $$\Pi^1_2$$-definable non-constructible real singleton.

• The Feferman–Levy model does not satisfy $V=L(\Bbb R)$, whereas the model in Farmer's answer does. Truss' model, mentioned in Farmer's answer, is $L(\Bbb R)$ of the Feferman–Levy model, but it is distinct from it. In both $\omega_1$ is singular, but only in one of them (the Feferman–Levy model) the reals are a countable union of countable sets. Commented Jan 3 at 11:53
• @AsafKaragila Thank you Asaf for the correction, I will modify my answer in light of your comment. Commented Jan 3 at 13:21
• Thanks, Ali! I've fixed the link to the preprint in the last paragraph, it somehow ended up mangled. Commented Jan 3 at 13:41