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

Question

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?

Answer 1

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.

Answer 2

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}^*)}$.

Answer 3

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.