Ramsey's theorem for pairs and provably recursive functions
type: Item
instance of: scholarly article
title: Ramsey's theorem for pairs and provably recursive functions
zbMATH Open document ID: 1221.03059
DOI: 10.1215/00294527-2009-019
author: Ulrich Kohlenbach
author: Alexander P. Kreuzer
published in: Notre Dame Journal of Formal Logic
publication date: 2010-09-02T00:00:00Z
review text: The paper under review adresses the strength of \textit{F. P. Ramsey}'s theorem for pairs [Proc. Lond. Math. Soc. (2) 30, 264--286 (1929; JFM 55.0032.04)] over a weak base theory applying methods of `proof mining'. The authors work in a weak base theory \({\mathcal T}\), based on fragments E-G\(_n\)A\(^\omega\) of extensional arithmetic in the language of functionals of all finite types, introduced by the second author [Arch. Math. Logic 36, No.~1, 31--71 (1996; Zbl 0882.03050)]. Thus, \({\mathcal T}\) is obtained by considering the union E-G\(_\infty\)A\(^\omega\) of these systems and adding QF-AC (quantifier-free axiom of choice from functions to numbers and from numbers to functions) as well as WKL (weak König's Lemma). For \(n\geq 1\), let RT\(_n^2\) denote Ramsey's theorem for \(n\)-colorings of \([{\mathbb N}]^2\) and, given an \(n\)-coloring \(c:[{\mathbb N}]^2\to \{0,1,\ldots,n-1\}\), let RT\(_n^2(c)\) be the statement expressing the fact that Ramsey's theorem holds for \(c\). The main technical result of the paper establishes that over \({\mathcal T}\) one can prove RT\(_n^2(c)\) from a suitable instance \(\Pi_0^1\text{-CA}(\tilde{\varphi}(c))\) of \(\Pi_0^1\)-comprehension. The authors obtain this result by a logical analysis of the proof of Ramsey's theorem for pairs due to Erdős and Rado. Combining this with previous results of \textit{U. Kohlenbach} [Ann. Pure Appl. Logic 95, No. 1--3, 257--285 (1998; Zbl 0945.03088)] on the arithmetical content of restricted forms of comprehension and choice, the authors obtain the second main result of the paper: If \[ {\mathcal T}\vdash \forall f\in{\mathbb N}^{\mathbb N} (\Pi_0^1\text{-CA}(\varphi(f))\wedge \forall k\in{\mathbb N} (\text{RT}_2^2(\psi(f,k)))\to \exists n\in{\mathbb N} A_{qf}(f,n)), \] where \(\varphi\), \(\psi\) are closed terms of \({\mathcal T}\) of suitable types, then there exists a primitive recursive (in the sense of Kleene) functional \(\Phi\) such that \[ \widehat{\text{E-PA}}^\omega\!\!\!\up…
reviewed by: Laurenţiu Leuştean
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 05D10
zbMATH DE Number: 5778809
zbMATH Keywords: Ramsey's theorem for pairs
zbMATH Keywords: provably recursive functions
zbMATH Keywords: proof mining
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1215/00294527-2009-019
OpenAlex ID: W2130233653
Recommended article: On the strength of Ramsey's theorem
Recommended article: Proof mining and combinatorics. Program extraction for Ramsey's theorem for pairs
Recommended article: The inductive strength of Ramsey's theorem for pairs
Recommended article: The metamathematics of Stable Ramsey’s Theorem for Pairs
Recommended article: On the strength of Ramsey's theorem without Σ1‐induction
Recommended article: RAMSEY’S THEOREM FOR PAIRS ANDKCOLORS AS A SUB-CLASSICAL PRINCIPLE OF ARITHMETIC
Recommended article: Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic
Recommended article: Coloring trees in reverse mathematics
Recommended article: On the strength of Ramsey's theorem for pairs
Recommended article: Term extraction and Ramsey's theorem for pairs
description: scientific article; zbMATH DE number 5778809