Weak axioms of determinacy and subsystems of analysis. II \((\Sigma ^ 0_ 2\) games) (Q805613)

[Part I is reviewed above (see Zbl 0729.03032).] Proof-theoretic strength of \(\Sigma^ 0_ 2\)-determinacy is investigated with respect to the well-known calibration subsystems \(\mathbf{ACA}_ 0\), \(\mathbf{ATR}_ 0\), \(\pmb\Pi^ 1_ 1\)-\(\mathbf{CA}\) of second-order arithmetic. Recall that a mapping \(\Gamma\) : P(\(\omega\))\(\to P(\omega)\) is called a monotone operator (over \(\omega\)) if \(\Gamma\) (X)\(\subset \Gamma (Y)\) whenever \(X\subset Y\subset \omega\). \(\Gamma\) is a \(\Sigma^ 1_ 1\)- operator if its graph \(\{\) (x,X): \(x\in \Gamma (X)\}\) is \(\Sigma^ 1_ 1\) without second-order parameters. The axiom of \(\Sigma^ 1_ 1\)- monotone inductive definition \((\Sigma^ 1_ 1\)-MI) asserts that for each \(\Sigma^ 1_ 1\)-monotone operator \(\Gamma\) there exists a transfinite sequence \(<\Gamma_{\alpha},\alpha <\sigma >\), \(\sigma\in Ord\), such that \(\Gamma_{\alpha}=\Gamma (\cup \{\Gamma_{\beta}:\beta <\alpha \})\) for all \(\alpha <\sigma\) and such that \(\Gamma_{\infty}=\Gamma (\Gamma_{\infty})\) with \(\Gamma_{\infty}=\cup \{\Gamma_{\alpha}:\alpha <\sigma \}.\) For any formula \(\phi\) with a variable ranging over \(\omega^{\omega}\), a two-player infinite game \(G_{\phi}\) is associated, in which players I and II alternately choose natural numbers. Player I wins if the resulting infinite sequence of natural numbers satisfies \(\phi\). The game \(G_{\phi}\) is determinate if either I or II has a winning strategy. For a class C of formulas, the axiom (C-Det) asserts that any game associated with a formula in C is determinate. It is proved that \[ \mathbf{ACA}_ {\mathbf{0}}\vdash (\Sigma^ 0_ 2-Det)\to (\Sigma^ 1_ 1-MI),\quad \mathbf{ATR}_ {\mathbf{0}}\vdash (\Sigma^ 1_ 1- MI)\to (\Sigma^ 0_ 2-Det). \] It is stated as a conjecture that \(\mathbf{ACA}_ 0\nvdash (\Sigma^ 1_ 1\)-MI)\(\to (\Sigma^ 0_ 2\)-Det).