Using Ramsey's theorem once
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)\).
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Classical consequences of continuous choice principles from intuitionistic analysis
- Effective Choice and Boundedness Principles in Computable Analysis
- scientific article; zbMATH DE number 2236640 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- On notions of computability-theoretic reduction between Π21 principles
- On the uniform computational content of Ramsey's theorem
- On uniform relationships between combinatorial problems
- On Weihrauch reducibility and intuitionistic reverse mathematics
- Reverse mathematics and uniformity in proofs without excluded middle
- Subsystems of second order arithmetic
- THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
- The weakness of being cohesive, thin or free in reverse mathematics
- Parallelizations in Weihrauch reducibility and constructive reverse mathematics
- Splittings and disjunctions in reverse mathematics
- Reverse mathematics and infinite traceable graphs
- Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics
- COH, SRT 2 2 , and multiple functionals
- THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
- Reverse mathematics and Weihrauch analysis motivated by finite complexity theory
- Reduction games, provability and compactness
- Compositions of multivalued functions
This page was built for publication: Using Ramsey's theorem once
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2274133)
