The determinacy strength of \(\Pi_2^1\)-comprehension (Q636381)

This paper characterizes the strength of \(\Pi^1_2\)-comprehension in second-order arithmetic in terms of determinacy. Let \({<}\omega\text{-}\Sigma^0_2\) be the union of the finite levels of the difference hierarchy over \(\Sigma^0_2\) and let \({<}\omega\text{-}\Sigma^0_2\text{-Det}\) be the statement that \({<}\omega\text{-}\Sigma^0_2\)-games are determined. The main result of this paper is that \(\Pi^1_2\text{-CA}_0\) and \(\text{ACA}_0+{<}\omega\text{-}\Sigma^0_2\text{-Det}\) prove the same \(\Pi^1_1\)-sentences. The proof of this statement makes use of the so-called \(\mu\)-calculus. Roughly, this is \(\text{ACA}_0\) together with a least fixed-point operator \(\mu\). In [Generalized inductive definitions. The \(\mu\)-calculus and \(\Pi^1_2\)-comprehension. Münster: Univ. Münster, Fachbereich Mathematik und Informatik (2002; Zbl 1050.03040)], the second author shows that the \(\mu\)-calculus and \(\Pi^1_2\text{-CA}_0\) prove the same \(\Pi^1_1\)-sentences. The main result is then established by showing that the \(\mu\)-calculus proves \({<}\omega\text{-}\Sigma^0_2\text{-Det}\) and that (a characterization of) the \(\mu\)-calculus can be interpreted in \({<}\omega\text{-}\Sigma^0_2\text{-Det}\).