pith. sign in

arxiv: 2404.18974 · v3 · submitted 2024-04-29 · 🧮 math.LO

Pi⁰₄ conservation of Ramsey's theorem for pairs

Quentin Le Hou\'erou , Ludovic Levy Patey , Keita Yokoyama This is my paper

Pith reviewed 2026-05-24 02:17 UTC · model grok-4.3

classification 🧮 math.LO
keywords Ramsey's theoremconservationreverse mathematicsRCA0B Sigma 2Pi04 formulasfirst-order part
0
0 comments X

The pith

Ramsey's theorem for pairs and two colors is a ∀Π⁰₄ conservative extension of RCA₀ + BΣ⁰₂.

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

The paper shows that Ramsey's theorem for pairs with two colors adds no new ∀Π⁰₄ sentences beyond those already provable in RCA₀ plus BΣ⁰₂. A ∀Π⁰₄ sentence begins with a universal set quantifier and continues with a Π⁰₄ formula. This strengthens an earlier conservation result by the same authors and advances the project of pinning down the exact first-order arithmetic consequences of the theorem. The argument refines existing combinatorial constructions to preserve the required logical complexity.

Core claim

Ramsey's theorem for pairs and two colors is a ∀Π⁰₄ conservative extension of RCA₀ + BΣ⁰₂, where a ∀Π⁰₄ formula consists of a universal quantifier over sets followed by a Π⁰₄ formula. The proof is an improvement of a result by Patey and Yokoyama and a step towards the resolution of the longstanding question of the first-order part of Ramsey's theorem for pairs.

What carries the argument

Strengthened version of the Patey-Yokoyama forcing or combinatorial construction that controls the complexity of preserved statements up to the ∀Π⁰₄ level.

If this is right

  • Every ∀Π⁰₄ sentence provable from RCA₀ + BΣ⁰₂ + RT²₂ is already provable from RCA₀ + BΣ⁰₂.
  • The first-order consequences of RT²₂ remain those already derivable in the base theory at this level of complexity.
  • The result narrows the possible gap between the first-order part of RT²₂ and the axioms of RCA₀ + BΣ⁰₂.

Where Pith is reading between the lines

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

  • Similar strengthening may apply to other Ramsey-type statements whose conservation was previously established only up to lower complexity.
  • The technique could be tested on variants such as Ramsey's theorem for pairs with more colors or on stable Ramsey's theorem.
  • If the pattern continues, the full first-order part of RT²₂ might coincide exactly with the first-order consequences of BΣ⁰₂.

Load-bearing premise

The combinatorial or model-theoretic techniques from the prior weaker conservation proof can be extended to handle the full ∀Π⁰₄ level without creating new consequences.

What would settle it

An explicit ∀Π⁰₄ sentence that RCA₀ + BΣ⁰₂ + RT²₂ proves but RCA₀ + BΣ⁰₂ alone does not prove.

read the original abstract

In this article, we prove that Ramsey's theorem for pairs and two colors is a $\forall \Pi^0_4$ conservative extension of $\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$, where a $\forall \Pi^0_4$ formula consists of a universal quantifier over sets followed by a $\Pi^0_4$ formula. The proof is an improvement of a result by Patey and Yokoyama and a step towards the resolution of the longstanding question of the first-order part of Ramsey's theorem for pairs.

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

0 major / 1 minor

Summary. The manuscript proves that Ramsey's theorem for pairs and two colors (RT²₂) is a ∀Π⁰₄ conservative extension of RCA₀ + BΣ⁰₂. The proof strengthens the argument of Patey and Yokoyama to obtain the full ∀Π⁰₄ conservation statement rather than a weaker form, as a step toward determining the first-order consequences of RT²₂.

Significance. The result strengthens existing conservation theorems in reverse mathematics for a central combinatorial principle. By achieving ∀Π⁰₄ conservation, it improves on the prior Patey–Yokoyama bound and supplies a concrete technical increment toward resolving the open question of the first-order part of RT²₂. The manuscript builds explicitly on independent prior work without reducing to fitted parameters or self-referential definitions.

minor comments (1)
  1. The abstract states the target conservation statement clearly but does not indicate the length or structure of the proof; a brief outline of the main lemmas in the introduction would help readers locate the strengthening of the Patey–Yokoyama argument.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment and recommendation to accept the manuscript. The report accurately summarizes the contribution as strengthening the Patey–Yokoyama result to full ∀Π⁰₄ conservation.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper establishes a new ∀Π⁰₄-conservation result for RT²₂ over RCA₀ + BΣ⁰₂ via an explicit proof that strengthens the techniques of the cited Patey–Yokoyama theorem. No step in the derivation reduces by the paper's own equations or definitions to a fitted parameter, self-referential renaming, or unverified self-citation chain; the prior result functions as an independent base that is extended rather than presupposed as the entire justification. The conservation statement is proved directly and remains externally falsifiable in the standard sense of reverse mathematics.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The result is a proof in second-order arithmetic relying on standard background axioms of RCA₀ and BΣ⁰₂; no free parameters, ad-hoc axioms, or new entities are introduced in the abstract statement.

pith-pipeline@v0.9.0 · 5627 in / 1061 out tokens · 27478 ms · 2026-05-24T02:17:47.010233+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

27 extracted references · 27 canonical work pages

  1. [1]

    The strength of infinita ry ram- seyan principles can be accessed by their densities

    Andrey Bovykin and Andreas Weiermann. The strength of infinita ry ram- seyan principles can be accessed by their densities. Annals of Pure and Applied Logic, 168(9):1700–1709, 2017

    work page 2017

  2. [2]

    Buss, editor

    Samuel R. Buss, editor. Handbook of proof theory , volume 137 of Studies in Logic and the Foundations of Mathematics . North-Holland Publishing Co., Amsterdam, 1998. 34

    work page 1998

  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. Symbolic Logic , 66(1):1–55, 2001

    work page 2001

  4. [4]

    C. T. Chong, Theodore A. Slaman, and Yue Yang. Π 1 1-conservation of combinatorial principles weaker than Ramsey’s theorem for pairs. Adv. Math., 230(3):1060–1077, 2012

    work page 2012

  5. [5]

    C. T. Chong, Theodore A. Slaman, and Yue Yang. The inductive st rength of Ramsey’s Theorem for Pairs. Adv. Math., 308:121–141, 2017

    work page 2017

  6. [6]

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

    Marta Fiori-Carones, Leszek Aleksander Ko/suppress lodziejczyk, Tin Lok Wong, and Keita Yokoyama. An isomorphism theorem for models of Weak K¨ onig’s Lemma without primitive recursion. Journal of the European Mathematical Society, 2021. To appear

    work page 2021

  7. [7]

    Some systems of second order arithmetic and their use

    Harvey Friedman. Some systems of second order arithmetic and their use. In Proceedings of the International Congress of Mathematicia ns (Vancou- ver, B.C., 1974), Vol. 1 , pages 235–242. Canad. Math. Congr., Montreal, QC, 1975

    work page 1974

  8. [8]

    Interpretability and fragments of arithmetic

    Petr H´ ajek. Interpretability and fragments of arithmetic. In P. Clote and J. Kraj ´ ıˇ cek, editors,Arithmetic, Proof Theory and Computational Com- plexity, pages 185–196. Oxford, Clarendon Press, 1993

    work page 1993

  9. [9]

    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

    work page 1998

  10. [10]

    Hirschfeldt

    Denis R. Hirschfeldt. Slicing the truth , volume 28 of Lecture Notes Se- ries. Institute for Mathematical Sciences. National Unive rsity of Singapore. World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2015. On t he computable and reverse mathematics of combinatorial principles, E dited and with a foreword by Chitat Chong, Qi Feng, Theodore A. Slam...

    work page 2015

  11. [11]

    COMBINATORICS IN SUBSYSTEMS OF SECOND ORDER ARITHMETIC

    Jeffry Lynn Hirst. COMBINATORICS IN SUBSYSTEMS OF SECOND ORDER ARITHMETIC . ProQuest LLC, Ann Arbor, MI, 1987. Thesis (Ph.D.)–The Pennsylvania State University

    work page 1987

  12. [12]

    Models of Peano arithmetic , volume 15 of Oxford Logic Guides

    Richard Kaye. Models of Peano arithmetic , volume 15 of Oxford Logic Guides. The Clarendon Press, Oxford University Press, New York, 1991. Oxford Science Publications

    work page 1991

  13. [13]

    Rapidly growing Ramsey fun ctions

    Jussi Ketonen and Robert Solovay. Rapidly growing Ramsey fun ctions. Ann. of Math. (2) , 113(2):267–314, 1981

    work page 1981

  14. [14]

    L. A. S. Kirby and J. B. Paris. Initial segments of models of Pean o’s axioms. In Set theory and hierarchy theory, V (Proc. Third Conf., Bieru towice, 1976), Lecture Notes in Math., Vol. 619, pages 211–226. Springer, Berlin , 1977. 35

    work page 1976

  15. [15]

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

    Leszek Aleksander Ko/suppress lodziejczyk, Tin Lok Wong, and Keita Yokoyama. Ramsey’s theorem for pairs, collection, and proof size. Journal of Mathe- matical Logic, page 2350007, 2023

    work page 2023

  16. [16]

    Some upper bounds on ordinal-valued Ramsey numbers for colourings of pairs

    Leszek Aleksander Ko/suppress lodziejczyk and Keita Yokoyama. Some upper bounds on ordinal-valued Ramsey numbers for colourings of pairs. Selecta Math. (N.S.), 26(4):Paper No. 56, 18, 2020

    work page 2020

  17. [17]

    In search of the first-order part of Ramsey’s theorem for pairs

    Leszek Aleksander Ko/suppress lodziejczyk and Keita Yokoyama. In search of the first-order part of Ramsey’s theorem for pairs. In Connecting with com- putability, volume 12813 of Lecture Notes in Comput. Sci. , pages 297–307. Springer, Cham, [2021] ©2021

    work page 2021

  18. [18]

    RT22 does not imply WKL0

    Jiayi Liu. RT22 does not imply WKL0. The Journal of Symbolic Logic , 77(2):609–620, 2012

    work page 2012

  19. [19]

    SRT2 2 does not imply RT2 2 in ω -models

    Benoit Monin and Ludovic Patey. SRT2 2 does not imply RT2 2 in ω -models. Adv. Math. , 389:Paper No. 107903, 32, 2021

    work page 2021

  20. [20]

    J. B. Paris. A hierarchy of cuts in models of arithmetic. In Model theory of algebra and arithmetic (Proc. Conf., Karpacz, 1979) , volume 834 of Lecture Notes in Math. , pages 312–337. Springer, Berlin, 1980

    work page 1979

  21. [21]

    Ramsey-like theorems and moduli of computatio n

    Ludovic Patey. Ramsey-like theorems and moduli of computatio n. J. Symb. Log., 87(1):72–108, 2022

    work page 2022

  22. [22]

    The proof-theoretic stre ngth of Ram- sey’s theorem for pairs and two colors

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

    work page 2018

  23. [23]

    Algebras of sets binumerable in complete extension s of arith- metic

    Dana Scott. Algebras of sets binumerable in complete extension s of arith- metic. In Proc. Sympos. Pure Math., Vol. V , pages 117–121. Amer. Math. Soc., Providence, RI, 1962

    work page 1962

  24. [24]

    David Seetapun and Theodore A. Slaman. On the strength of Ra msey’s theorem. volume 36, pages 570–582. 1995. Special Issue: Models of arith- metic

    work page 1995

  25. [25]

    On Π 1 1 conservativity of Π 1 2 theories in second order arithmetic

    Keita Yokoyama. On Π 1 1 conservativity of Π 1 2 theories in second order arithmetic. In C. T. Chong et al., editor, Proceedings of the 10th Asian Logic Conference, pages 375–386. World Scientific, 2009

    work page 2009

  26. [26]

    On conservativity for theories in second orde r arithmetic

    Keita Yokoyama. On conservativity for theories in second orde r arithmetic. In Proceedings of the 10th Asian Logic Conference , pages 375–386. World Scientific, 2010

    work page 2010

  27. [27]

    Notes on the first-order part of Ramsey’s th eorem for pairs (proof theory and complexity)

    Keita Yokoyama. Notes on the first-order part of Ramsey’s th eorem for pairs (proof theory and complexity). 2013. 36

    work page 2013