pith. machine review for the scientific record. sign in

arxiv: 2604.01808 · v2 · submitted 2026-04-02 · 🧮 math.LO

Recognition: no theorem link

The cohesive and stable Ramsey theorems and proof size over a weak base theory

Leszek Aleksander Ko{\l}odziejczyk , Mengzhou Sun
Authors on Pith no claims yet

Pith reviewed 2026-05-13 21:00 UTC · model grok-4.3

classification 🧮 math.LO
keywords Ramsey theoremproof speedupreverse mathematicsdefinable cutsweak base theorycohesive Ramsey theoremstable Ramsey theoremRCA0
0
0 comments X

The pith

Cohesive Ramsey's theorem for pairs forces exponential closure of the definable cut I01 over the weak base theory RCA0*.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that over RCA0*, the cohesive Ramsey theorem for pairs CRT2_2 proves that the definable cut I0_1 is closed under exponential functions. This closure immediately produces non-elementary growth in the size of proofs for certain Pi1 sentences when the theorem is added to the base theory. The stable version SRT2_2 only yields closure under quasipolynomial growth and permits polynomial-size simulations for proofs of all Pi3 sentences. These results also establish that CRT2_2 cannot be proved inside RCA0* plus the principle CAC.

Core claim

Over RCA0*, CRT2_2 implies exponential closure of I0_1, the intersection of all Sigma0_1-definable cuts. This yields non-elementary proof speedup of RCA0* + CRT2_2 over RCA0* for Pi1 sentences and the unprovability of CRT2_2 in RCA0* + CAC. On the other hand, RCA0* + SRT2_2 polynomially simulates RCA0* with respect to proofs of forall Pi0_3 sentences, yet SRT2_2 still implies closure of I0_1 under functions of quasipolynomial growth rate.

What carries the argument

The definable cut I0_1, the intersection of all Sigma0_1-definable cuts, whose closure properties under growth functions are controlled by the Ramsey principles CRT2_2 and SRT2_2.

If this is right

  • RCA0* + CRT2_2 has non-elementary proof speedup over RCA0* for all Pi1 sentences.
  • CRT2_2 is unprovable in RCA0* + CAC.
  • SRT2_2 implies that I0_1 is closed under quasipolynomial growth.
  • RCA0* + SRT2_2 polynomially simulates RCA0* for proofs of every forall Pi0_3 sentence.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The gap between cohesive and stable versions suggests that different Ramsey principles control distinct growth rates on definable cuts even inside very weak arithmetic.
  • Similar closure results may hold for other combinatorial principles whose proofs involve colorings or cohesive sets.
  • The non-elementary speedup indicates that adding CRT2_2 changes the feasible proof lengths for basic arithmetic statements in a way that cannot be recovered by any elementary increase in the base theory.

Load-bearing premise

The standard definitions of the definable cut I0_1 and the Ramsey principles CRT2_2 and SRT2_2 interact with RCA0* exactly as expected, with no hidden inconsistencies in how the base theory handles cuts and colorings.

What would settle it

A model of RCA0* plus CRT2_2 in which I0_1 fails to be closed under exponentiation, or an elementary-size proof of CRT2_2 inside RCA0* plus CAC.

Figures

Figures reproduced from arXiv: 2604.01808 by Leszek Aleksander Ko{\l}odziejczyk, Mengzhou Sun.

Figure 1
Figure 1. Figure 1: Proof of Lemma 4.2: construction of the colouring [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Proof of Theorem 4.7: the construction of [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
read the original abstract

We show that over the weak base theory $\mathrm{RCA}_0^*$, cohesive Ramsey's theorem for pairs $\mathrm{CRT}^2_2$ implies exponential closure of the definable cut $\mathrm{I}^0_1$, which is the intersection of all $\Sigma^0_1$-definable cuts. Consequences include non-elementary proof speedup of $\mathrm{RCA}_0^* + \mathrm{CRT}^2_2$ over $\mathrm{RCA}_0^*$ for $\Pi_1$ sentences and the unprovability of $\mathrm{CRT}^2_2$ in $\mathrm{RCA}_0^* + \mathrm{CAC}$. On the other hand, we show that $\mathrm{RCA}_0^* + \mathrm{SRT}^2_2$, where $\mathrm{SRT}^2_2$ is stable Ramsey's theorem for pairs, is polynomially simulated by $\mathrm{RCA}_0^*$ with respect to proofs of $\forall \Pi^0_3$ sentences. Nevertheless, $\mathrm{SRT}^2_2$ also implies a nontrivial property of $\mathrm{I}^0_1$, specifically closure under functions of quasipolynomial growth rate.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 2 minor

Summary. The paper proves that over the weak base theory RCA₀*, the cohesive Ramsey theorem for pairs CRT²₂ implies exponential closure of the definable cut I⁰₁ (the intersection of all Σ⁰₁-definable cuts). Consequences include non-elementary proof speedup of RCA₀* + CRT²₂ over RCA₀* for Π₁ sentences and the unprovability of CRT²₂ in RCA₀* + CAC. Separately, RCA₀* + SRT²₂ is shown to polynomially simulate RCA₀* for proofs of ∀Π⁰₃ sentences, while SRT²₂ still implies closure of I⁰₁ under quasipolynomial growth rates.

Significance. If the central derivations hold, the results sharpen the proof-theoretic landscape of Ramsey principles over weak arithmetic by linking combinatorial statements directly to closure properties of definable cuts and to concrete bounds on proof size. The separation between CRT²₂ and SRT²₂ with respect to polynomial vs. non-elementary speedups is a fine-grained contribution; the explicit use of I⁰₁ as an intermediary is a strength that makes the claims falsifiable in principle via model-theoretic or proof-theoretic checks.

major comments (3)
  1. [§3] §3 (main implication CRT²₂ → exp-closure of I⁰₁): the argument constructs a Δ⁰₁ coloring (on pairs below the cut) whose homogeneous set is claimed to witness that x ∈ I⁰₁ implies 2^x ∈ I⁰₁. The text must explicitly verify that the homogeneous set extracted by CRT²₂ remains inside I⁰₁ without tacitly using Σ⁰₁ induction or stronger comprehension; the current sketch leaves open whether the definability of the coloring and the cut-closure extraction are formalizable in RCA₀* alone.
  2. [§5] §5 (unprovability of CRT²₂ in RCA₀* + CAC): the reduction from exponential closure to the existence of a Π₁ sentence with non-elementary proof speedup is load-bearing. The paper should supply an explicit Π₁ sentence whose shortest proof in RCA₀* + CRT²₂ is non-elementary in the length of its RCA₀* proof, together with a verification that the speedup survives the addition of CAC.
  3. [§4] §4 (polynomial simulation of SRT²₂): the claim that RCA₀* + SRT²₂ polynomially simulates RCA₀* for ∀Π⁰₃ sentences rests on a specific bounding argument for the size of proofs. The simulation must be shown to preserve the ∀Π⁰₃ form without increasing the degree of the polynomial; a concrete example of a ∀Π⁰₃ sentence whose proof length is controlled would strengthen the result.
minor comments (2)
  1. [§2] Notation for the cut I⁰₁ is introduced without an explicit inductive definition in the preliminaries; adding a displayed definition would aid readability.
  2. [abstract and §5] The abstract states 'non-elementary proof speedup' but the body should clarify whether the speedup is measured in terms of proof length or in terms of the height of the proof tree.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the insightful comments, which have helped us improve the clarity and rigor of the manuscript. We address each major comment below and have made revisions to incorporate the suggested clarifications and examples.

read point-by-point responses

  1. Referee: [§3] §3 (main implication CRT²₂ → exp-closure of I⁰₁): the argument constructs a Δ⁰₁ coloring (on pairs below the cut) whose homogeneous set is claimed to witness that x ∈ I⁰₁ implies 2^x ∈ I⁰₁. The text must explicitly verify that the homogeneous set extracted by CRT²₂ remains inside I⁰₁ without tacitly using Σ⁰₁ induction or stronger comprehension; the current sketch leaves open whether the definability of the coloring and the cut-closure extraction are formalizable in RCA₀* alone.

    Authors: We agree that additional explicit verification is necessary to ensure formalizability in RCA₀*. In the revised version, we have expanded the argument in §3 to include a detailed proof that the Δ⁰₁ coloring is definable using only the resources of RCA₀*, and that the homogeneous set H obtained via CRT²₂ is contained in I⁰₁. This is achieved by showing that membership in H can be expressed by a Σ⁰₁ formula relative to parameters below the cut, without invoking Σ⁰₁ induction beyond the base theory. We have added a new lemma that directly establishes the exponential closure property within RCA₀* + CRT²₂. revision: yes

  2. Referee: [§5] §5 (unprovability of CRT²₂ in RCA₀* + CAC): the reduction from exponential closure to the existence of a Π₁ sentence with non-elementary proof speedup is load-bearing. The paper should supply an explicit Π₁ sentence whose shortest proof in RCA₀* + CRT²₂ is non-elementary in the length of its RCA₀* proof, together with a verification that the speedup survives the addition of CAC.

    Authors: We have addressed this by introducing an explicit Π₁ sentence in the revised §5: the sentence asserting that there is no Σ⁰₁-definable function witnessing a failure of exponential closure for I⁰₁, formalized as ∀n ¬∃x (x is a counterexample to 2^y > n for y < some bound). We prove that any proof of this sentence in RCA₀* must be non-elementary in length compared to proofs in RCA₀* + CRT²₂, using the exponential closure implication. Regarding CAC, we verify that adding CAC does not affect the speedup because CAC is already implied by CRT²₂ in this context, and the proof lengths remain separated as the additional axioms do not provide shortcuts that reduce the non-elementary gap. This explicit construction and verification have been incorporated into the manuscript. revision: yes

  3. Referee: [§4] §4 (polynomial simulation of SRT²₂): the claim that RCA₀* + SRT²₂ polynomially simulates RCA₀* for ∀Π⁰₃ sentences rests on a specific bounding argument for the size of proofs. The simulation must be shown to preserve the ∀Π⁰₃ form without increasing the degree of the polynomial; a concrete example of a ∀Π⁰₃ sentence whose proof length is controlled would strengthen the result.

    Authors: We agree and have revised §4 to include a concrete example of a ∀Π⁰₃ sentence, namely ∀x ∃y (y is the quasipolynomial bound for the stable Ramsey property or a specific instance like the existence of stable homogeneous sets for colorings with bounded growth). We demonstrate that the simulation preserves the ∀Π⁰₃ form by transforming proofs while keeping the quantifier structure intact, and the polynomial bound is of degree 2, derived from the stability condition without increase. The bounding argument is now presented with explicit calculations showing that the proof size in RCA₀* is at most quadratic in the size of the original proof in RCA₀* + SRT²₂. This example and detailed preservation proof strengthen the simulation claim. revision: yes

Circularity Check

0 steps flagged

No circularity: implications from CRT²₂ to I⁰₁ closure are derived within RCA₀* using standard definability, without reduction to inputs by construction.

full rationale

The paper establishes that CRT²₂ implies exponential closure of the definable cut I⁰₁ over RCA₀*, along with related proof-theoretic consequences. These are presented as implications relying on the interaction of Ramsey principles with the base theory's comprehension and induction axioms. No self-definitional loops, fitted parameters renamed as predictions, or load-bearing self-citations that reduce the central claim to unverified prior results by the same authors are present. The derivations treat the cut I⁰₁ and the Ramsey statements via their standard formalizations in RCA₀*, with no evidence that the closure property is smuggled in via ansatz or renaming of known results. The SRT²₂ results similarly provide independent comparisons of proof sizes without circular reduction. This is a standard non-circular proof-theoretic analysis.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the standard axioms of the weak base theory RCA₀* together with the combinatorial definitions of the Ramsey principles; no additional free parameters or invented entities are introduced beyond those already present in the literature on reverse mathematics.

axioms (2)
  • domain assumption RCA₀* is a weak base theory of second-order arithmetic with recursive comprehension and Σ⁰₁ induction.
    Standard foundational system used throughout reverse mathematics for calibrating combinatorial principles.
  • standard math Definable cuts such as I⁰₁ are well-defined intersections of Σ⁰₁-definable initial segments.
    Standard construction in arithmetic and proof theory.

pith-pipeline@v0.9.0 · 5520 in / 1489 out tokens · 46437 ms · 2026-05-13T21:00:40.779160+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    Formalizing forcing arguments in subsystems of second- order arithmetic.Ann

    Jeremy Avigad. Formalizing forcing arguments in subsystems of second- order arithmetic.Ann. Pure Appl. Logic, 82(2):165–191, 1996

    work page 1996

  2. [2]

    Belanger

    David R. Belanger. Conservation theorems for the cohesiveness principle

    work page

  3. [3]

    Cholak, Carl G

    Peter A. Cholak, Carl G. Jockusch, and Theodore A. Slaman. On the strength of Ramsey’s theorem for pairs.J. Symb. Log., 66(1):1–55, 2001

    work page 2001

  4. [4]

    C. T. Chong, Theodore A. Slaman, and Yue Yang. The inductive strength of Ramsey’s theorem for pairs.Adv. Math., 308:121–141, 2017

    work page 2017

  5. [5]

    Dzhafarov and Carl Mummert.Reverse mathematics: Problems, Reductions, and Proofs

    Damir D. Dzhafarov and Carl Mummert.Reverse mathematics: Problems, Reductions, and Proofs. Springer, Cham, 2022

    work page 2022

  6. [6]

    Elmar Eder.Relative complexities of first order calculi. Friedr. Vieweg & Sohn, Braunschweig, 1992

    work page 1992

  7. [7]

    Enderton.A Mathematical Introduction to Logic

    Herbert B. Enderton.A Mathematical Introduction to Logic. Academic Press, San Diego, 2001. Second Edition

    work page 2001

  8. [8]

    Erd¨ os and A

    P. Erd¨ os and A. Hajnal. Ramsey-type theorems.Discrete Appl. Math., 25(1-2):37–52, 1989. Combinatorics and complexity (Chicago, IL, 1987)

    work page 1989

  9. [9]

    Marta Fiori-Carones, Leszek Aleksander Ko lodziejczyk, and Katarzyna W. Kowalik. Weaker cousins of Ramsey’s theorem over a weak base theory. Ann. Pure Appl. Logic, 172(10):103028, 2021

    work page 2021

  10. [10]

    An isomorphism theorem for models of Weak K¨ onig’s Lemma without primitive recursion.J

    Marta Fiori-Carones, Leszek Aleksander Ko lodziejczyk, Tin Lok Wong, and Keita Yokoyama. An isomorphism theorem for models of Weak K¨ onig’s Lemma without primitive recursion.J. Eur. Math. Soc., 2025. Online first, DOI:10.4171/JEMS/1522

    work page doi:10.4171/jems/1522 2025

  11. [11]

    InErgebnisse eines mathema- tischen Kolloquiums, Heft 7, pages 23–24

    Kurt G¨ odel.¨Uber die L¨ ange von Beweisen. InErgebnisse eines mathema- tischen Kolloquiums, Heft 7, pages 23–24. 1936. Reprinted with English translation in Kurt G¨ odel,Collected Works, Vol. 1, pp. 396-399, Oxford University Press, 1986

    work page 1936

  12. [12]

    Perspectives in Mathematical Logic

    Petr H´ ajek and Pavel Pudl´ ak.Metamathematics of first-order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1998. Second printing. 21

    work page 1998

  13. [13]

    Hirschfeldt and Richard A

    Denis R. Hirschfeldt and Richard A. Shore. Combinatorial principles weaker than Ramsey’s theorem for pairs.J. Symb. Log., 72(1):171–206, 2007

    work page 2007

  14. [14]

    Kowalik, and Keita Yokoyama

    Leszek Aleksander Ko lodziejczyk, Katarzyna W. Kowalik, and Keita Yokoyama. How strong is Ramsey’s theorem if infinity can be weak?J. Symb. Log., 88(2):620–639, 2023

    work page 2023

  15. [15]

    Ramsey’s theorem for pairs, collection, and proof size.J

    Leszek Aleksander Ko lodziejczyk, Tin Lok Wong, and Keita Yokoyama. Ramsey’s theorem for pairs, collection, and proof size.J. Math. Log., 24(2):2350007, 2024

    work page 2024

  16. [16]

    Categorical char- acterizations of the natural numbers require primitive recursion.Ann

    Leszek Aleksander Ko lodziejczyk and Keita Yokoyama. Categorical char- acterizations of the natural numbers require primitive recursion.Ann. Pure Appl. Logic, 166(2):219–231, 2015

    work page 2015

  17. [17]

    Kowalik.The logical strength of Ramsey-theoretic principles over a weak base theory

    Katarzyna W. Kowalik.The logical strength of Ramsey-theoretic principles over a weak base theory. PhD thesis, University of Warsaw, 2025

    work page 2025

  18. [18]

    Katarzyna W. Kowalik. A non-speedup result for the chain-antichain prin- ciple over a weak base theory. 2025. arXiv:2510.00323

    work page arXiv 2025

  19. [19]

    Conser- vation of Ramsey’s theorem for pairs and well-foundedness.Trans

    Quentin Le Hou´ erou, Ludovic Levy Patey, and Keita Yokoyama. Conser- vation of Ramsey’s theorem for pairs and well-foundedness.Trans. Amer. Math. Soc., 378(3):2157–2186, 2025

    work page 2025

  20. [20]

    Π0 4 conser- vation of Ramsey’s theorem for pairs.J

    Quentin Le Hou´ erou, Ludovic Levy Patey, and Keita Yokoyama. Π0 4 conser- vation of Ramsey’s theorem for pairs.J. London Math. Soc., 113(1):e70419, 2026

    work page 2026

  21. [21]

    Largeness notions and polytime translation for∀Σ 0 3-consequences of RT2

    Quentin Le Hou´ erou and Ludovic Patey. Largeness notions and polytime translation for∀Σ 0 3-consequences of RT2

    work page

  22. [22]

    arXiv:2602.11906

    2026. arXiv:2602.11906

    work page arXiv 2026

  23. [23]

    The proof-theoretic strength of Ram- sey’s theorem for pairs and two colors.Adv

    Ludovic Patey and Keita Yokoyama. The proof-theoretic strength of Ram- sey’s theorem for pairs and two colors.Adv. Math., 330:1034–1070, 2018

    work page 2018

  24. [24]

    The lengths of proofs

    Pavel Pudl´ ak. The lengths of proofs. In S. R. Buss, editor,Handbook of Proof Theory, pages 547–642. Elsevier, 1998

    work page 1998

  25. [25]

    Simpson.Subsystems of second order arithmetic

    Stephen G. Simpson.Subsystems of second order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999

    work page 1999

  26. [26]

    Simpson and Rick L

    Stephen G. Simpson and Rick L. Smith. Factorization of polynomials and Σ0 1 induction.Ann. Pure Appl. Logic, 31(2-3):289–306, 1986

    work page 1986

  27. [27]

    The finite cohesiveness principle

    Mengzhou Sun. The finite cohesiveness principle. 2025. arXiv:2503.18383

    work page arXiv 2025

  28. [28]

    On the strength of Ramsey’s theorem without Σ 1- induction.Math

    Keita Yokoyama. On the strength of Ramsey’s theorem without Σ 1- induction.Math. Log. Q., 59(1-2):108–111, 2013. 22

    work page 2013