The ethics of Borel determinacy

Question

I was speaking with a friend the other day, and I happened to say "morally, Borel determinacy is as strong as ZF." I was riffing on the well-known result of Harvey Friedman, that we need $\omega_1$-many iterates of the powerset operation to prove full Borel determinacy (formally: ???), and the philosophical point that this amounts to basically all the replacement we could ever need in day-to-day mathematics (and then some!).

Now, though, I'm wondering about my statement. My question is whether there is a reasonable sense in which Borel determinacy is as strong as I naively think that it is. Precisely:

Is there a "reasonably natural" theory $T$ - substantially weaker than $ZF$ - such that Borel determinacy + $T$ has consistency strength (greater than or) equal to that of $ZF$?

If so, can we in fact find such a $T$ with Borel determinacy $+$ $T$ $\models ZF$? I suspect the answer to this second question is false: Borel determinacy doesn't seem to let us iterate the powerset function $\omega_2$ times, say, and I doubt there's a natural theory that says something like "if you can iterate powerset $\omega_1$-many times, you can iterate it $\alpha$-many times for all $\alpha$." But I could be wrong!

By "reasonably natural" theory, I mean a theory that has already been studied quite a bit in logic. Some candidates that come to mind include $KP$, $Z_\omega$, $Z_2$, and $RCA_0$.

NOTE: I have tagged "computability theory" because of the possible connection with reverse mathematics.

Answer 1

I don't know about consistency strength.

But certainly, the stronger question of adding Borel determinacy to a "natural, weak" theory $T$ and getting ZF must have a negative answer. Borel determinacy may be hard to prove, but it is a statement in the language of second-order arithmetic. So it would be down to $T$ to know about larger cardinalities (but not too much), and to be able to relate what is happening for larger cardinalities down to the continuum, where it then needs the help of Borel determinacy to draw some conclusions, which it can then lift up again. That feels very unnatural to me.

Instead, I think the formal question to ask is:

If $\varphi$ is a statement in the language of second-order arithmetic such that $\mathrm{ZF}$ proves $\varphi$. Does it already hold that $\mathrm{ATR}_0 + \text{Borel determinacy}$ proves $\varphi$?

The reason why I am going for $\mathrm{ATR}_0$ as base theory here is that $\mathrm{ATR}_0$ is making Borel codes work properly (eg, it ensures that if $x$ is a point and $A$ a Borel set, then either $x \in A$ or $x \notin A$). There may be a way to get some boot-strapping done, and use determinacy for very simple games to get to $\mathrm{ATR}_0$, but answering the question above really seems to cover the gist of the intuitive claim.