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?

4more comments