Some logically weak Ramseyan theorems (Q2453567)

The main aim of the paper is to show that some Ramsey-like theorems are weak in the sense that (unlike the usual Ramsey theorem) they do not imply \(\mathrm{ACA}_0\) even if they are stated for arbitrarily large fixed exponents. The theorems studied include: -- the achromatic Ramsey theorem for exponent \(r\) and bound \(d\), \(\mathrm{ART}^r_{<\infty, d}\): for every colouring \(f\) of \([\omega]^r\) by finitely many colours, there exists an infinite \(H\) such that \(f([H]^r)\) has fewer than \(d\) elements, -- Friedman's thin set theorem and free set theorem for exponent \(r\), \(\mathrm{TS}^r\) and \(\mathrm{FS}^r\): for every \(f : [\omega]^r \to \omega\), there exists an infinite set \(S\) such that \(f([S]^r) \neq \omega\) and an infinite set \(H\) such that for all \(\bar x \in [H]^r\), \(f(\bar x) \notin H \setminus \{\bar x\}\), respectively, -- the rainbow Ramsey theorem for exponent \(r\) and bound \(b\), \(\mathrm{RRT}^r_b\): for every colouring \(f : [\omega]^r \to \omega\), if not more than \(b\) tuples are mapped to any single colour, then there is an infinite set \(H\) such that \(f\) is injective on \([H]^r\). The author proves that none of \(\mathrm{TS}^r\), \(\mathrm{FS}^r\) and \(\mathrm{RRT}^r_2\) imply \(\mathrm{ACA}_0\) over \(\mathrm{RCA}_0\), and neither does \(\mathrm{ART}^r_{<\infty,d_r}\) for a sufficiently large number \(d_r\) which depends on \(r\) but can be effectively bounded in \(r\). This is a significant strengthening of earlier results by the author such as the unprovability of \(\mathrm{ACA}_0\) from \(\mathrm{RCA}_0 + \mathrm{RRT}^3_2\) [J. Symb. Log. 78, No. 3, 824--836 (2013; Zbl 1300.03013)]. To prove the weakness of the above theorems, the author shows that the computational problems associated with the theorems have the strong cone avoidance property. Here, a problem associated with a statement \(\forall X \exists Y \varphi(X,Y)\) has strong cone avoidance if for any set \(A\), any \(B\) that does not compute \(A\), and any \(X\) (regardless of the complexity of \(X\)) there exists a solution \(Y\) to \(\varphi(X,Y)\) such that \(B \oplus Y\) still does not compute \(A\). Strong cone avoidance for \(\mathrm{ART}^r_{<\infty,d_r}\) and \(\mathrm{FS}^r\) is established by induction on \(r\); the inductive steps are relatively involved arguments employing, among other things, standard tools in this area such as cohesive-stable decomposition and Mathias forcing. Strong cone avoidance for \(\mathrm{TS}^r\) and \(\mathrm{RRT}^r_2\) follows easily.