Effectiveness for the dual Ramsey theorem (Q2075273)

This paper is a contribution to the reverse mathematics of the dual Ramsey theorem (DRT). While in the standard Ramsey theorem the \(k\)-element subsets of \(\omega\) are colored, which correspond to injective functions of type \(k \to \omega\), in DRT surjective functions of type \(\omega \to k\) are colored. DRT was first proved for Borel colorings by \textit{T. J. Carlson} and \textit{S. G. Simpson} [Adv. Math. 53, 265--290 (1984; Zbl 0564.05005)] and it was extended to colorings with the Baire property by \textit{H. J. Prömel} and \textit{B. Voigt} [Trans. Am. Math. Soc. 291, 189--201 (1985; Zbl 0577.05008)]. In the Introduction, the authors discuss the two variants of DRT studied in their work: the Borel dual Ramsey theorem (Borel-DRT) and the Baire dual Ramsey theorem (Baire-DRT). The authors provide information on previous work in the literature and they include several implications over RCA\(_0\) between variants of DRT considered in their paper and some related principles. They also give an overview of their results. In Section 2, the notation used throughout their paper is fixed. In Section 3, a purely combinatorial version of DRT (CDRT\(^k_l\)), which precisely captures the strength of Baire-DRT, is given. Hindman's theorem for \(l\)-colorings is shown to imply CDRT\(^3_l\) and the Carlson-Simpson lemma CSL\((m, l)\) is shown to be a special case of CDRT\(^{m+1}_l\). Moreover, a proof of CDRT\(^k_l\), for every \(l\) and \(k \geq 2\), is given. In Section 4, Borel-DRT for \(k \geq 3\) is studied from the perspective of effective mathematics. In Section 5, Borel-DRT for \(k = 2\) is studied. Moreover, problems motivated by the reverse mathematics of Borel-DRT\(^2_2\) are considered. Specifically, Borel-DRT\(^2_2\) is considered as an instance-solution problem. In Section 6, it is shown that over ATR\(_0\) Borel-DRT\(^k_l\) and Baire-DRT\(^k_l\) are equivalent. It is also shown that over ACA\(_0\) the statement ``every trivial Borel code has an evaluation map'' implies ATR\(_0\). In Section 7, four related open questions are listed.