Using Ramsey's theorem once (Q2274133)

The paper studies the question of how many applications of one principle are needed to prove another in the context of higher-order reverse mathematics, and its connections to Weihrauch reducibility. The base theory is taken to be \(i\mathsf{RCA}^\omega_0\), consisting of Feferman's system \(\widehat{\mathsf{E\text-HA}}^\omega_\restriction\) of intuitionistic arithmetic of all finite types and the quantifier-free choice schema \(\mathsf{QF\text-AC}^{1,0}\); the extension of this theory to classical logic is the theory \(\mathsf{RCA}^\omega_0\) of \textit{U. Kohlenbach} [Lect. Notes Log. 21, 281--295 (2005; Zbl 1097.03053)]. Considering problems \(P\) of the form \(\forall x\,(p_1(x)\to\exists y\,p_2(x,y))\), the authors define a natural notion that a theory \(T\supseteq i\mathsf{RCA}^\omega_0\) proves a problem \(Q\) with ``one typical use'' of \(P\). They also consider a formal version \(T\vdash Q\le_WP\) of Weihrauch reducibility between such problems (which differs from actual Weihrauch reducibility \(Q\le_WP\) in that the reduction functionals are not a priori required to be computable). The main general results are that under suitable syntactic restrictions on \(P\) and \(Q\), \(i\mathsf{RCA}^\omega_0\) proves \(Q\) with one typical use of \(P\) iff \(i\mathsf{RCA}^\omega_0\vdash Q\le_WP\), and that this implies \(Q\le_WP\). As an application, the paper looks on dependencies between the Ramsey principles \(\mathsf{RT}(n,k)\), asserting that any \(k\)-colouring of \([\mathbb N]^n\) has an infinite monochromatic set. They show that even though \(i\mathsf{RCA}^\omega_0\vdash\mathsf{RT}(2,2)\to\mathsf{RT}(2,4)\), \(i\mathsf{RCA}^\omega_0\) cannot prove \(\mathsf{RT}(2,4)\) with only one typical use of \(\mathsf{RT}(2,2)\), using known results on Weihrauch reducibility between these problems. More generally, for any \(n\ge1\) and \(k>j\ge2\), \(i\mathsf{RCA}^\omega_0\) does not prove \(\mathsf{RT}(n,k)\) with only one typical use of \(\mathsf{RT}(n,j)\). Surprisingly, the classical theory \(\mathsf{RCA}^\omega_0\) \textit{does} prove \(\mathsf{RT}(2,4)\) with one typical use of \(\mathsf{RT}(2,2)\): the authors show this by a clever use of excluded middle to distinguish whether there exists an infinite bichromatic set or not. More generally, \(\mathsf{RCA}^\omega_0\) proves \(\mathsf{RT}(n,k)\) with one typical use of \(\mathsf{RT}(n,2)\).