Weak Infinitary Comprehension versus Weak Choice

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work over $\mathsf{RCA}_0$, the subsystem of second-order arithmetic with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction; all structures and orders are countable and coded by sets of integers. $\mathsf{ACA}_0$ adds comprehension for every arithmetical formula (set parameters allowed), and $\mathsf{ATR}_0$ adds arithmetical transfinite recursion along every coded well-order. Reverse-mathematical equivalence means provability of both implications over this base. An $L_{\omega_1,\omega}$ sentence of arithmetic is coded by a well-founded syntax tree allowing countable conjunctions and disjunctions, alongside ordinary finite first-order operations. A valuation assigns truth values to all subformulas (and assignments to free number variables) satisfying their logical rules. Weak infinitary comprehension asserts: if $(\varphi_n)_{n\ge0}$ is a sequence of these sentences, each individually admitting a valuation, there is a set $X$ with $n\in X$ exactly when $\varphi_n$ evaluates true. Weak $\Sigma^1_1$ choice is the scheme \[\forall n\,\exists!X\,\psi(n,X)\ \Longrightarrow\ \exists Y\,\forall n\,\psi(n,Y^{[n]}),\] for every arithmetical $\psi$ with parameters, where $Y^{[n]}=\{k:\langle n,k\rangle\in Y\}$ using a fixed integer pairing function.

Statement recorded in the supplied source.

Are weak $L_{\omega_1,\omega}$ comprehension and weak $\Sigma^1_1$ choice equivalent over $\mathsf{RCA}_0$? [S3] [S2]

Short English statement

Does collecting truth values of an individually evaluable sequence of infinitary arithmetic sentences require exactly weak unique-set choice?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500131 (AMR-074-0131). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint (17 August 2010), Question 31, Section 5, p. 12. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.
• S3 Antonio Montalbán, Indecomposable Linear Orderings and Hyperarithmetic Analysis (2006), Section 1.6, definition of weak $\Sigma^1_1$ choice. https://math.berkeley.edu/~antonio/papers/indec.pdf.