How much determinacy do you need for second order arithmetic to be as strong as ZFC?

Question

From Wikipedia (I couldn't find the original source):

$\text{ZFC} + \{\text{there are $n$ Woodin cardinals: $n$ is a natural number}\}$ is conservative over $\text{Z}_2$ with projective determinacy.

(where projective determinacy is interpreted as a schema in the language of second order arithmetic).

How much determinacy do we actually need if we want to get up to ZFC level? Or more precisely, for which pointclasses $\mathbf{S}$ in the projective hierarchy is $\mathbf{\text{ZFC} + S\text{-determinacy}}$ conservative over $\mathbf{\text{Z}_2 + S\text{-determinacy}}$? (This is equivalent to saying that if a statement in the language of second order arithmetic is also a theorem of ZFC, it is a theorem of $\text{Z}_2 + S\text{-determinacy}$.)

$S$ is at least borel (since ZFC proves borel determinacy).

Answer 1

Because ZFC proves soundness of $\text{Z}_2$, no consistent finite extension of $\text{Z}_2$ proves all second order arithmetic statements that are provable in ZFC (for example, the statement "the conjunction of the new axioms implies their own consistency with $\text{Z}_2$"). Moreover, for each fixed $n$, $Σ^1_n$ soundness can be expressed by a single sentence in $\text{Z}_2$, so infinite extensions with $Σ^1_n$ sentences (fixed $n$) would not work either. I suspect that $\text{Z}_2 + \mathbf{Σ^1_n}$ determinacy (fixed $n$) does not even prove the countable choice schema. It is only by using statements of unbounded quantifier alternation depth that we get the quoted conservation result.

With regard to consistency strength, $\text{Z}_2 + Σ^1_1-\text{Det}$ is at a least a strong as ZFC. Going further, over $\text{Z}_2$, $\mathbf{Σ^1_1}-\text{Det}$ (note the boldface) is equivalent to every real having a sharp.

I suspect that $\text{Z}_2 ⊢ Σ^1_1-\text{Det} ⇔ 0^\#$. Now, $\text{Z}_2+ 0^\#$ proves $Σ^1_1-\text{Det}$ and $\operatorname{Con}(\text{ZFC} + ∀α < ω_1 \, α-\text{Erdős cardinal})$. However, the current proof of $Σ^1_1-\text{Det} ⇒ 0^\#$ does not work in $\text{Z}_2$. That proof yields a real $x$ such that every $x$-admissible ordinal is an $L$-cardinal, which makes $ω_1$ inaccessible in $L$. However, getting $0^\#$ from such an $x$ requires going beyond $\text{Z}_2$ (and even third order arithmetic), and over $\text{Z}_2$ such an $x$ is merely equiconsistent with ZFC (see Harrington's principle over higher order arithmetic by Cheng and Schindler). For $\mathbf{Σ^1_1}-\text{Det}$, we get ZFC in $L[r]$ for every real $r$, so we get the sharps.