pith. sign in

arxiv: 2606.12962 · v2 · pith:S7NFKCNGnew · submitted 2026-06-11 · 🧮 math.LO

The reverse mathematics of the Ordered Variable Word theorem

Lu Liu , Ludovic Patey This is my paper

Pith reviewed 2026-07-04 00:01 UTC · model grok-4.3

classification 🧮 math.LO
keywords reverse mathematicsordered variable word theoremRamsey theorem for pairsCarlson-Simpson lemmadual Ramsey theoremACA0low2 degreecomputability
0
0 comments X

The pith

The Ordered Variable Word theorem does not imply Ramsey's theorem for pairs.

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

The paper establishes that the Ordered Variable Word theorem fails to imply Ramsey's theorem for pairs when both are formalized in second-order arithmetic. It further shows that every computable instance of the Ordered Variable Word theorem has a solution of low2 degree. These two facts together allow the Carlson-Simpson Lemma and the Open Dual Ramsey theorem to be proved inside the system ACA0. The work thereby settles questions that remained open for roughly forty years and yields further consequences for the reverse mathematics of structural Ramsey theory.

Core claim

The Ordered Variable Word theorem does not imply Ramsey's theorem for pairs, and every computable instance admits a solution of low2 degree. This is used to prove the Carlson-Simpson Lemma and the Open Dual Ramsey theorem over ACA0.

What carries the argument

The Ordered Variable Word theorem, a combinatorial principle asserting the existence of variable words satisfying certain homogeneity conditions in colorings, whose logical strength is measured by non-implication and computability results.

If this is right

  • The Carlson-Simpson Lemma holds over ACA0.
  • The Open Dual Ramsey theorem holds over ACA0.
  • Certain statements in structural Ramsey theory become provable in ACA0 rather than requiring stronger systems.

Where Pith is reading between the lines

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

  • The separation shows that some combinatorial principles used to prove Dual Ramsey theorems can be strictly weaker than Ramsey's theorem for pairs.
  • Low2 solutions for computable instances provide a uniform way to obtain solutions without increasing the Turing degree beyond the arithmetic hierarchy.
  • Similar degree analyses may apply to other variable-word or partition principles in the same family.

Load-bearing premise

The Ordered Variable Word theorem and the related statements are correctly formalized inside second-order arithmetic so that the non-implication and computability results transfer to the stated consequences for ACA0.

What would settle it

A computable instance of the Ordered Variable Word theorem whose every solution has Turing degree strictly above low2 would falsify the computability claim.

Figures

Figures reproduced from arXiv: 2606.12962 by Ludovic Patey, Lu Liu.

Figure 1
Figure 1. Figure 1: Summary diagram of implications and separations over [PITH_FULL_IMAGE:figures/full_fig_p054_1.png] view at source ↗
read the original abstract

In this article, we study the reverse mathematics of variable word theorems used in the proof of the Dual Ramsey theorem. We prove that the Ordered Variable Word theorem does not imply Ramsey's theorem for pairs and that every computable instance admits a solution of low${}_2$ degree. This is used to prove the Carlson-Simpson Lemma and the Open Dual Ramsey theorem over~$\mathsf{ACA}_0$, thereby answering some 40-years old open questions. These results have consequences in the reverse mathematics of structural Ramsey theory.

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

2 major / 2 minor

Summary. The paper studies the reverse mathematics of variable word theorems appearing in proofs of the Dual Ramsey theorem. It proves that the Ordered Variable Word theorem does not imply Ramsey's theorem for pairs and that every computable instance admits a low₂ solution; these facts are then used to derive the Carlson-Simpson Lemma and the Open Dual Ramsey theorem over ACA₀, thereby settling questions open for roughly forty years, with further consequences for the reverse mathematics of structural Ramsey theory.

Significance. If the formalizations are correct, the separation from RT²₂ together with the low₂ bound supply the missing ingredients needed to place the Carlson-Simpson Lemma and Open Dual Ramsey theorem inside ACA₀. The work therefore resolves long-standing questions about the logical strength of these combinatorial statements and supplies concrete computability information that can be reused in other parts of structural Ramsey theory.

major comments (2)
  1. [§2] The central non-implication and low₂ claims rest on the assumption that the Ordered Variable Word theorem has been correctly formalized as a sentence of second-order arithmetic so that the computability and implication results transfer to the stated ACA₀ derivations; this formalization step is load-bearing for every subsequent application and must be verified explicitly.
  2. [§4] The derivations of the Carlson-Simpson Lemma and Open Dual Ramsey theorem over ACA₀ (presumably in §4 or §5) rely on the low₂ solutions; any gap in the reduction from the variable-word statement to these lemmas would undermine the claim that the questions are settled in ACA₀.
minor comments (2)
  1. [Abstract] The abstract refers to “some 40-years old open questions” without naming them; a brief enumeration in the introduction would improve readability.
  2. Notation for the various variable-word statements should be introduced once and used consistently; occasional shifts between “Ordered Variable Word theorem” and its acronym can be clarified.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the recommendation for minor revision. The comments correctly identify the formalization and the reductions as central to the results; we address both points explicitly below and will strengthen the manuscript accordingly.

read point-by-point responses

  1. Referee: [§2] The central non-implication and low₂ claims rest on the assumption that the Ordered Variable Word theorem has been correctly formalized as a sentence of second-order arithmetic so that the computability and implication results transfer to the stated ACA₀ derivations; this formalization step is load-bearing for every subsequent application and must be verified explicitly.

    Authors: We agree that explicit verification of the formalization is necessary. In §2 we define OVWT as the Π¹₁ sentence asserting that every computable coloring c : [ω]<ω → 2 admits an infinite variable word w such that the set of finite variable substitutions is monochromatic. The non-implication and low₂ results are proved directly in the standard model of second-order arithmetic; because the constructions are effective (using only recursive approximations and finite injury), they relativize and therefore hold in any model of ACA₀. In the revision we will add a short subsection (new §2.4) that records the precise sentence of L₂ and confirms that the computability proofs remain valid inside ACA₀. revision: yes

  2. Referee: [§4] The derivations of the Carlson-Simpson Lemma and Open Dual Ramsey theorem over ACA₀ (presumably in §4 or §5) rely on the low₂ solutions; any gap in the reduction from the variable-word statement to these lemmas would undermine the claim that the questions are settled in ACA₀.

    Authors: The reductions appear in Theorems 4.2 and 4.4. Given a low₂ solution H to an OVWT instance, we construct (inside ACA₀) a homogeneous set for the corresponding Carlson-Simpson or Open Dual Ramsey instance by a single application of the low₂ set’s jump and the arithmetic comprehension already available in ACA₀. The argument uses only the fact that low₂ sets are closed under Turing join with 0′ and that the variable-word homogeneity can be decoded arithmetically from H. We will insert an additional paragraph after each theorem spelling out the arithmetic comprehension steps to eliminate any possible ambiguity. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper establishes non-implications (OVWT does not imply RT^2_2) and computability bounds (low2 solutions for computable instances) via direct constructions in second-order arithmetic, then derives consequences for the Carlson-Simpson Lemma and Open Dual Ramsey theorem over ACA0. No step reduces a claimed result to a fitted parameter, self-defined quantity, or load-bearing self-citation chain; the formalization of OVWT as a sentence in the language of second-order arithmetic is a standard prerequisite rather than a circular dependency, and the proofs remain independent of the target conclusions.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard background axioms and definitions from reverse mathematics and Ramsey theory; no free parameters, ad-hoc axioms, or new entities are indicated in the abstract.

axioms (1)
  • standard math Axioms of second-order arithmetic (RCA0, ACA0)
    Base theories in which the non-implications and derivations are carried out.

pith-pipeline@v0.9.1-grok · 5601 in / 1064 out tokens · 25590 ms · 2026-07-04T00:01:55.483732+00:00 · methodology

Review history (2 revisions) →

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. The finite big Ramsey degrees of Henson graphs are provable in $\mathrm{ACA}_0$

    math.LO 2026-06 unverdicted novelty 7.0

    The finite big Ramsey degrees of Henson graphs are provable in ACA₀', with equivalence to ACA₀' over RCA₀.

Reference graph

Works this paper leans on

55 extracted references · 5 canonical work pages · cited by 1 Pith paper

  1. [1]

    Carlson-Simpson’s lemma and applications in reverse mathematics.Ann

    Paul-Elliot Angles d’Auriac, Lu Liu, Bastien Mignoty, and Ludovic Patey. Carlson-Simpson’s lemma and applications in reverse mathematics.Ann. Pure Appl. Logic, 174(9):Paper No. 103287, 16, 2023

    2023

  2. [2]

    Exact big ramsey degrees via coding trees.arXiv preprint arXiv:2110.08409, page 97, 2021

    Martin Balko, David Chodounsk` y, Natasha Dobrinen, Jan Hubiˇ cka, Matˇ ej Koneˇ cn` y, Lluis Vena, and Andy Zucker. Exact big ramsey degrees via coding trees.arXiv preprint arXiv:2110.08409, page 97, 2021

    work page arXiv 2021

  3. [3]

    Exact big ramsey degrees for finitely constrained binary free amalgamation classes.Journal of the Eu- ropean Mathematical Society, 53, 2024

    Martin Balko, David Chodounsk` y, Natasha Dobrinen, Jan Hubicka, Matej Konecn` y, Llu´ ıs Vena, and Andy Zucker. Exact big ramsey degrees for finitely constrained binary free amalgamation classes.Journal of the Eu- ropean Mathematical Society, 53, 2024

    2024

  4. [4]

    The reverse mathematics of Carlson’s theorem for located words.arXiv preprint arXiv:2208.03152, 2022

    Tristan Bompard, Lu Liu, and Ludovic Patey. The reverse mathematics of Carlson’s theorem for located words.arXiv preprint arXiv:2208.03152, 2022

    work page arXiv 2022

  5. [5]

    Timothy J. Carlson. Some unifying principles in Ramsey theory.Discrete Math., 68(2-3):117–169, 1988

    1988

  6. [6]

    Carlson and Stephen G

    Timothy J. Carlson and Stephen G. Simpson. A dual form of Ramsey’s theorem.Adv. in Math., 53(3):265–290, 1984

    1984

  7. [7]

    The henson graphs: colorings and codings, 2026

    Peter Cholak, Natasha Dobrinen, and Charlie McCoy. The henson graphs: colorings and codings, 2026

    2026

  8. [8]

    The finite big ram- sey degrees of henson graphs are provable in ACA 0, 2026

    Peter Cholak, Natasha Dobrinen, and Henry Towsner. The finite big ram- sey degrees of henson graphs are provable in ACA 0, 2026

    2026

  9. [9]

    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

    2001

  10. [10]

    ProQuest LLC, Ann Arbor, MI, 1980

    Denis Campau Devlin.SOME PARTITION THEOREMS AND ULTRA- FILTERS ON OMEGA. ProQuest LLC, Ann Arbor, MI, 1980. Thesis (Ph.D.)–Dartmouth College

    1980

  11. [11]

    The Ramsey theory of the universal homogeneous triangle-free graph.Journal of Mathematical Logic, 20(2):2050012, 75,

    Natasha Dobrinen. The Ramsey theory of the universal homogeneous triangle-free graph.Journal of Mathematical Logic, 20(2):2050012, 75,

  12. [12]

    tex.fjournal: Journal of Mathematical Logic tex.mrclass: 03E02 (03C15 03E05 03E40 03E75 05C05 05C55) tex.mrnumber: 4128725 tex.mrreviewer: G.Cherlin

  13. [13]

    The ramsey theory of the universal homogeneous triangle-free graph part ii: exact big ramsey degrees.arXiv preprint arXiv:2009.01985, 2020

    Natasha Dobrinen. The ramsey theory of the universal homogeneous triangle-free graph part ii: exact big ramsey degrees.arXiv preprint arXiv:2009.01985, 2020

    work page arXiv 2009

  14. [14]

    The Ramsey theory of Henson graphs.J

    Natasha Dobrinen. The Ramsey theory of Henson graphs.J. Math. Log., 23(1):Paper No. 2250018, 88, 2023. 55

    2023

  15. [15]

    A den- sity version of the Carlson-Simpson theorem.J

    Pandelis Dodos, Vassilis Kanellopoulos, and Konstantinos Tyros. A den- sity version of the Carlson-Simpson theorem.J. Eur. Math. Soc. (JEMS), 16(10):2097–2164, 2014

    2097

  16. [16]

    Relationships between computability-theoretic proper- ties of problems.J

    Rod Downey, Noam Greenberg, Matthew Harrison-Trainor, Ludovic Patey, and Dan Turetsky. Relationships between computability-theoretic proper- ties of problems.J. Symb. Log., 87(1):47–71, 2022

    2022

  17. [17]

    Effectiveness for the dual Ramsey theorem.Notre Dame J

    Damir Dzhafarov, Stephen Flood, Reed Solomon, and Linda Westrick. Effectiveness for the dual Ramsey theorem.Notre Dame J. Form. Log., 62(3):455–490, 2021

    2021

  18. [18]

    Dzhafarov and Carl G

    Damir D. Dzhafarov and Carl G. Jockusch. Ramsey’s theorem and cone avoidance.Journal of Symbolic Logic, 74(2):557–578, 2009

    2009

  19. [19]

    Dzhafarov and Carl Mummert.Reverse mathematics—problems, reductions, and proofs

    Damir D. Dzhafarov and Carl Mummert.Reverse mathematics—problems, reductions, and proofs. Theory and Applications of Computability. Springer, Cham, [2022]©2022

    2022

  20. [20]

    El-Zahar and N

    M. El-Zahar and N. Sauer. The indivisibility of the homogeneousK n-free graphs.J. Combin. Theory Ser. B, 47(2):162–170, 1989

    1989

  21. [21]

    PhD thesis, UC Berkeley, 2013

    Julia Christina Erhard.The Carlson-Simpson Lemma in Reverse Mathe- matics. PhD thesis, UC Berkeley, 2013

    2013

  22. [22]

    Some systems of second order arithmetic and their use

    Harvey Friedman. Some systems of second order arithmetic and their use. Inin Proceedings of the International Congress of Mathematicians, Van- couver 1974, pages 235–242, 1975

    1974

  23. [23]

    A note on the indivisibility of the henson graphs, 2023

    Kenneth Gill. A note on the indivisibility of the henson graphs, 2023

    2023

  24. [24]

    S. S. Gonˇ carov and A. T. Nurtazin. Constructive models of complete de- cidable theories.Algebra i Logika, 12:125–142, 243, 1973

    1973

  25. [25]

    A. W. Hales and R. I. Jewett. Regularity and positional games.Trans. Amer. Math. Soc., 106:222–229, 1963

    1963

  26. [26]

    Partition theorems for left and right variable words.Combinatorica, 24(2):271–286, 2004

    Neil Hindman and Randall McCutcheon. Partition theorems for left and right variable words.Combinatorica, 24(2):271–286, 2004

    2004

  27. [27]

    Hirschfeldt.Slicing the truth, volume 28 ofLecture Notes Se- ries

    Denis R. Hirschfeldt.Slicing the truth, volume 28 ofLecture Notes Se- ries. Institute for Mathematical Sciences. National University of Singapore. World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ, 2015. On the computable and reverse mathematics of combinatorial principles, Edited and with a foreword by Chitat Chong, Qi Feng, Theodore A. Slaman, W...

    2015

  28. [28]

    Hirschfeldt and Richard A

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

    2007

  29. [29]

    Hirschfeldt, Richard A

    Denis R. Hirschfeldt, Richard A. Shore, and Theodore A. Slaman. The atomic model theorem and type omitting.Trans. Amer. Math. Soc., 361(11):5805–5837, 2009

    2009

  30. [30]

    Big ramsey degrees using parameter spaces.arXiv preprint arXiv:2009.00967, page 20, 2020

    Jan Hubiˇ cka. Big ramsey degrees using parameter spaces.arXiv preprint arXiv:2009.00967, page 20, 2020

    work page arXiv 2009

  31. [31]

    Jockusch, Jr

    Carl G. Jockusch, Jr. Semirecursive sets and positive reducibility.Trans. Amer. Math. Soc., 131:420–436, 1968

    1968

  32. [32]

    Jockusch, Jr

    Carl G. Jockusch, Jr. Ramsey’s theorem and recursion theory.J. Symbolic Logic, 37:268–280, 1972

    1972

  33. [33]

    Jockusch, Jr

    Carl G. Jockusch, Jr. and Robert I. Soare. Π 0 1 classes and degrees of theo- ries.Trans. Amer. Math. Soc., 173:33–56, 1972

    1972

  34. [34]

    Coloring of universal graphs.Graphs Combin., 2(1):55–60, 1986

    P´ eter Komj´ ath and Vojtˇ ech R¨ odl. Coloring of universal graphs.Graphs Combin., 2(1):55–60, 1986

    1986

  35. [35]

    Laflamme, N

    C. Laflamme, N. W. Sauer, and V. Vuksanovic. Canonical partitions of universal structures.Combinatorica, 26(2):183–205, 2006

    2006

  36. [36]

    A computable analysis of vari- able words theorems.Proc

    Lu Liu, Benoit Monin, and Ludovic Patey. A computable analysis of vari- able words theorems.Proc. Amer. Math. Soc., 147(2):823–834, 2019

    2019

  37. [37]

    Paris-Harrington incompleteness and progressions of theories

    Kenneth McAloon. Paris-Harrington incompleteness and progressions of theories. InRecursion theory (Ithaca, N.Y., 1982), volume 42 ofProc. Sympos. Pure Math., pages 447–460. Amer. Math. Soc., Providence, RI, 1985

    1982

  38. [38]

    Miller and Reed Solomon

    Joseph S. Miller and Reed Solomon. Effectiveness for infinite variable words and the dual Ramsey theorem.Arch. Math. Logic, 43(4):543–555, 2004

    2004

  39. [39]

    Open questions in reverse mathematics.Bull

    Antonio Montalb´ an. Open questions in reverse mathematics.Bull. Symbolic Logic, 17(3):431–454, 2011

    2011

  40. [40]

    Determinacy and reflection prin- ciples in second-order arithmetic.arXiv preprint arXiv:2209.04082, 2022

    Leonardo Pacheco and Keita Yokoyama. Determinacy and reflection prin- ciples in second-order arithmetic.arXiv preprint arXiv:2209.04082, 2022

    work page arXiv 2022

  41. [41]

    PhD thesis, Universit´ e Paris Diderot (Paris 7) Sorbonne Paris Cit´ e, 2016

    Ludovic Patey.The reverse mathematics of Ramsey-type theorems. PhD thesis, Universit´ e Paris Diderot (Paris 7) Sorbonne Paris Cit´ e, 2016

    2016

  42. [42]

    Iterative forcing and hyperimmunity in reverse mathemat- ics.Computability, 6(3):209–221, 2017

    Ludovic Patey. Iterative forcing and hyperimmunity in reverse mathemat- ics.Computability, 6(3):209–221, 2017

    2017

  43. [43]

    Lowness and avoidance

    Ludovic Levy Patey. Lowness and avoidance. Available at https://hal.science/hal-05343144/, 2025

    2025

  44. [44]

    F. P. Ramsey. On a Problem of Formal Logic.Proc. London Math. Soc. (2), 30(4):264–286, 1929. 57

    1929

  45. [45]

    Rosenstein.Linear orderings, volume 98 ofPure and Applied Mathematics

    Joseph G. Rosenstein.Linear orderings, volume 98 ofPure and Applied Mathematics. Academic Press, Inc. [Harcourt Brace Jovanovich, Publish- ers], New York-London, 1982

    1982

  46. [46]

    N. W. Sauer. Coloring subgraphs of the Rado graph.Combinatorica, 26(2):231–253, 2006

    2006

  47. [47]

    Edge partitions of the countable triangle free homogeneous graph.Discrete Math., 185(1-3):137–181, 1998

    Norbert Sauer. Edge partitions of the countable triangle free homogeneous graph.Discrete Math., 185(1-3):137–181, 1998

    1998

  48. [48]

    David Seetapun and Theodore A. Slaman. On the strength of Ramsey’s theorem.Notre Dame J. Formal Logic, 36(4):570–582, 1995. Special Issue: Models of arithmetic

    1995

  49. [49]

    Primitive recursive bounds for van der Waerden numbers

    Saharon Shelah. Primitive recursive bounds for van der Waerden numbers. J. Amer. Math. Soc., 1(3):683–697, 1988

    1988

  50. [50]

    J. R. Shoenfield. On degrees of unsolvability.Ann. of Math. (2), 69:644– 653, 1959

    1959

  51. [51]

    Simpson.Subsystems of second order arithmetic

    Stephen G. Simpson.Subsystems of second order arithmetic. Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009

    2009

  52. [52]

    Theodore A. Slaman. A note on dual Ramsey theorem. January 1997

    1997

  53. [53]

    Soare.Turing Computability

    Robert I. Soare.Turing Computability. Theory and Applications of Com- putability. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016

    2016

  54. [54]

    A simple proof and some difficult examples for Hindman’s theorem.Notre Dame J

    Henry Towsner. A simple proof and some difficult examples for Hindman’s theorem.Notre Dame J. Form. Log., 53(1):53–65, 2012

    2012

  55. [55]

    The Paris-Harrington principle and second-order arithmetic-bridging the finite and infinite Ramsey theorem

    Keita Yokoyama. The Paris-Harrington principle and second-order arithmetic-bridging the finite and infinite Ramsey theorem. InICM— International Congress of Mathematicians. Vol. 3. Sections 1–4, pages 1504–1528. EMS Press, Berlin, [2023]©2023. 58

    2023