How much of second-order arithmetic do you need for $\mathbf{\Sigma}^1_1$-determinacy to give you countable transitive models of $\mathsf{ZFC}$?

Question

This is in some sense a follow-up to this question.

The answer there says that over $\mathsf{Z}_2$ (second-order arithmetic), (boldface) $\mathbf{\Sigma}^1_1$-determinacy is enough to entail the existence of $0^{\sharp}$, which, if I'm understanding correctly, gives you the existence of a countable transitive model of $\mathsf{ZFC}$ (over just $\mathsf{Z}_2$).

Since the existence of a countable transitive model of $\mathsf{ZFC}$ is a single sentence, we know by compactness that only some fragment of $\mathsf{Z}_2 + \mathbf{\Sigma}^1_1\text{-Det}$ is necessary to entail the existence of a countable transitive model of $\mathsf{ZFC}$, so I'm wondering whether one of the standard subsystems of second-order arithmetic is actually sufficient.

It's a classic result of Steel that open determinacy is equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$, so if we restrict attention to the big five, there's only really two options.

Question. Does $\mathsf{RCA}_0 + \mathbf{\Sigma}^1_1\text{-Det}$ (equivalently $\mathsf{ATR}_0 + \mathbf{\Sigma}^1_1\text{-Det}$) entail the existence of a countable transitive model of $\mathsf{ZFC}$? If not does $\mathbf{\Pi}^1_1\text{-}\mathsf{CA}_0+\mathbf{\Sigma}^1_1\text{-Det}$ suffice?

I'm also curious about analogous questions regarding just consistency strength and possibly only considering (lightface) $\Sigma^1_1$-determinacy.

Answer 1

$\mathsf{RCA}_0 + \mathbf{\Sigma}^1_1\text{-Det}$ suffices to get sharps for all reals (and thus ctm of ZFC and more).

With boldface determinacy principles, we can bootstrap the background theory. $\mathbf{\Sigma}^1_1\text{-Det}$ or just $\mathbf{\Sigma}^0_1 \setminus \mathbf{\Sigma}^0_1 \text{-Det}$ gives $\mathbf{\Pi}^1_1\text{-}\mathsf{CA}_0$.

If we need more, over $\mathbf{\Pi}^1_1\text{-}\mathsf{CA}_0$, for every real $r$, $\Delta^1_1(r)$ determinacy is equivalent to existence for every $r$-recursive ordinal $α$ of a countable transitive model containing $r$ of KP + "$ω_α$ exists". A detailed level-by-level correspondence can be found in "Calibrating Determinacy Strength in Borel Hierarchies" (pdf) by Sherwood Julius Hachtman (2015).

One then uses $\mathbf{\Sigma}^1_1\text{-Det}$ to get Harrington's principle (HP) for every real $r$ (i.e. for some real $r'$ (dependent on $r$), every $r'$-admissible ordinal is an $L[r]$ cardinal). See for example "Analytic determinacy and 0^#. A forcing-free proof of Harrington’s theorem" (link) by Ramez Sami (1999). For more on HP, see the question you linked and also Harrington's principle over higher order arithmetic by Cheng and Schindler (2015).

Finally, given a real $r$, choose $r'$ witnessing HP for $r$. Next, using HP for $r'$, $L_{ω_1}[r']$ satisfies power set, and thus $r^\#$ exists in $L_{ω_1}[r']$ and hence in $V$.

By contrast, for lightface determinacy, we cannot just boostrap the background theory, raising interesting questions on how much background closure is needed and what happens without it.