arxiv: 2605.15151 · v1 · submitted 2026-05-14 · 🧮 math.LO

Recognition: 1 theorem link

· Lean Theorem

Avoiding logical strength in real analysis

Anton Freund , Nicholas Pischke , Patrick Uftring

Authors on Pith no claims yet

Pith reviewed 2026-05-15 02:51 UTC · model grok-4.3

classification 🧮 math.LO

keywords reverse mathematicsslow Cauchy sequencesconservative extensionsinfinite pigeonhole principlestrong cohesive principleBolzano-Weierstrass theoremHeine-Borel theoremArzelà-Ascoli theorem

0 comments

The pith

Real analysis in one dimension can be developed in theories conservative over RCA0 by using slow Cauchy sequences without rates of convergence.

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

The authors replace the usual representation of real numbers by Cauchy sequences with explicit rates of convergence by slow Cauchy sequences that lack such rates. In this setting, nearly all one-dimensional real analysis from Simpson's reverse mathematics text can be carried out in axiom systems that are conservative over RCA0. These developments yield two clusters of equivalences, one with the infinite pigeonhole principle and one with the strong cohesive principle. The second cluster encompasses theorems such as Bolzano-Weierstrass, Arzelà-Ascoli, and even Heine-Borel, which had been thought to require stronger axioms like arithmetical comprehension. This indicates that elementary analysis can avoid much of the logical strength traditionally associated with it and that the separation between analytical and combinatorial principles may not be as sharp as the reverse mathematics zoo suggests.

Core claim

Working without rates of convergence in the definition of real numbers via slow Cauchy sequences allows the development of almost all one-dimensional real analysis in theories conservative over RCA0, with the Bolzano-Weierstrass theorem, Arzelà-Ascoli theorem, and Heine-Borel theorem becoming equivalent to the infinite pigeonhole principle or the strong cohesive principle.

What carries the argument

Slow Cauchy sequences, which are Cauchy sequences of rationals without a specified rate of convergence, used as the representation for real numbers.

Load-bearing premise

Slow Cauchy sequences without rates of convergence suffice to perform the full range of one-dimensional analytic arguments while preserving conservativity and the stated equivalences.

What would settle it

A specific theorem in one-dimensional real analysis that still requires arithmetical comprehension or a stronger principle even when formalized using slow Cauchy sequences would falsify the main claim.

read the original abstract

In reverse mathematics, real numbers are traditionally represented by Cauchy sequences with a given rate of convergence. We work without rates and speak of slow Cauchy sequences. It turns out that almost all one-dimensional real analysis from the reverse mathematics book by Simpson can then be developed in theories that are conservative over $\mathsf{RCA}_0$. Specifically, we obtain clusters of equivalences with the infinite pigeonhole principle and the strong cohesive principle. The second cluster includes results like the Bolzano-Weierstrass and Arzel\`a-Ascoli theorems, which are traditionally associated with the stronger axiom of arithmetical comprehension, but also the Heine-Borel theorem, which is normally separated from these principles. This suggests two things: In elementary analysis, one can avoid logical strength to an extent that the traditional picture seems to forbid. And the division of the so-called reverse mathematics zoo into analytical and combinatorial principles may be less rigid than previously assumed.

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.

Desk Editor's Note private letter to a colleague

Slow Cauchy sequences let the authors push most one-dimensional analysis down to RCA0 plus combinatorial principles like IP and COH, but the transfer to standard rate-equipped statements needs checking.

read the letter

The paper's central move is to drop convergence rates and work with slow Cauchy sequences. This lets them recover almost all the one-dimensional analysis from Simpson inside theories conservative over RCA0, and they produce two clusters of equivalences: one with the infinite pigeonhole principle and another with the strong cohesive principle. The second cluster pulls in Bolzano-Weierstrass, Arzelà-Ascoli, and even Heine-Borel, which is the part that stands out against the usual reverse-math picture where those theorems sit at ACA0 or WKL strength. The development is systematic and the conservativity claims are stated cleanly. That is the actual novelty: a rate-free representation that still supports the classical theorems while lowering the logical overhead and mixing analytical and combinatorial strength in a way the literature has not done before. The proofs appear to be carried out directly in the base theory plus the combinatorial axioms, with no obvious circularity or extra parameters. The main soft spot is the implicit step that the slow versions are equivalent, over RCA0, to the rate-equipped statements used in Simpson. If the slow Bolzano-Weierstrass or Heine-Borel turns out to be strictly weaker, then the conservativity and the equivalence clusters apply only to the modified statements, not automatically to the traditional ones. The abstract claims the full range carries over, but that equivalence is the load-bearing point and will need explicit verification in the proofs. This work is aimed at reverse mathematicians who care about the exact strength of analysis and the analytical-combinatorial boundary. A reader already comfortable with RCA0, WKL, and ACA0 will get the most from the equivalences and the conservativity results. It is coherent on its own terms and shows clear engagement with the literature, so it deserves a serious referee even if the equivalence details require tightening.

Referee Report

2 major / 2 minor

Summary. The manuscript claims that representing real numbers by slow Cauchy sequences (without a prescribed rate of convergence) permits the development of almost all one-dimensional real analysis from Simpson's reverse-mathematics text inside subsystems of second-order arithmetic that are conservative over RCA0. It obtains two clusters of equivalences over RCA0: one with the infinite pigeonhole principle and one with the strong cohesive principle, the latter encompassing Bolzano-Weierstrass, Arzelà-Ascoli, and Heine-Borel.

Significance. If the conservativity and equivalence results hold, the work shows that a substantial body of elementary analysis can be carried out without invoking arithmetical comprehension or stronger principles, thereby weakening the traditional association of analytic theorems with higher logical strength and suggesting that the analytical-combinatorial divide in the reverse-mathematics zoo is less rigid than usually assumed.

major comments (2)

The central transfer argument—that the slow-Cauchy versions of Bolzano-Weierstrass, Arzelà-Ascoli, and Heine-Borel are provably equivalent over RCA0 to the rate-equipped statements used in Simpson—must be stated and proved explicitly. Without this equivalence, the claimed conservativity over RCA0 applies only to a modified theory and does not automatically yield the stated results for the traditional formulations.
Section 4 (or the section containing the main equivalence proofs): the derivation that the strong-cohesive cluster is conservative over RCA0 relies on the slow representation preserving the combinatorial content of the analytic statements; an explicit reduction or conservation lemma is required to confirm that no additional strength is introduced by the absence of rates.

minor comments (2)

Clarify the precise definition of 'slow Cauchy sequence' at the first appearance and state whether the modulus of convergence is merely omitted or provably nonexistent in the base theory.
Add a short comparison table or paragraph contrasting the logical strength obtained here with the corresponding results in Simpson for the rate-equipped setting.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We agree that the transfer between slow-Cauchy and rate-equipped formulations requires explicit treatment to secure the conservativity claim for the traditional statements. We will revise the manuscript accordingly.

read point-by-point responses

Referee: The central transfer argument—that the slow-Cauchy versions of Bolzano-Weierstrass, Arzelà-Ascoli, and Heine-Borel are provably equivalent over RCA0 to the rate-equipped statements used in Simpson—must be stated and proved explicitly. Without this equivalence, the claimed conservativity over RCA0 applies only to a modified theory and does not automatically yield the stated results for the traditional formulations.

Authors: We agree that the equivalence must be stated and proved explicitly. In the revised manuscript we will insert a dedicated subsection (placed immediately before the main equivalence theorems) that proves, over RCA0, that each slow-Cauchy statement is equivalent to its rate-equipped counterpart as formulated in Simpson. The argument proceeds in two directions: (i) any rate-equipped sequence is automatically slow, and (ii) given a slow Cauchy sequence, the relevant combinatorial principle (IPP or SC) supplies a subsequence that converges at a computable rate, thereby recovering the traditional formulation. This establishes the transfer without increasing logical strength. revision: yes
Referee: Section 4 (or the section containing the main equivalence proofs): the derivation that the strong-cohesive cluster is conservative over RCA0 relies on the slow representation preserving the combinatorial content of the analytic statements; an explicit reduction or conservation lemma is required to confirm that no additional strength is introduced by the absence of rates.

Authors: We accept that an explicit conservation lemma is needed. The revised Section 4 will contain a formal reduction lemma showing that any theorem proved from RCA0 plus the slow-Cauchy versions of the analytic statements can be translated, via the already-established equivalences to SC, into a proof in RCA0 + SC. Since SC is known to be conservative over RCA0, this yields the desired conservativity for the slow formulations and, by the transfer lemma, for the traditional statements as well. revision: yes

Circularity Check

0 steps flagged

No circularity in the derivation chain

full rationale

The paper formalizes one-dimensional real analysis over RCA0 using slow Cauchy sequences (without rates) and proves conservativity plus clusters of equivalences to combinatorial principles such as the infinite pigeonhole principle and strong cohesive principle. These results are obtained by explicit syntactic translations and proof-theoretic reductions inside second-order arithmetic; no parameter is fitted to data and then renamed as a prediction, no definition is given in terms of its own output, and no load-bearing step reduces to a self-citation or ansatz imported from the authors' prior work. The claimed equivalence between slow and standard representations is established by the formal development itself rather than presupposed, rendering the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the standard base theory RCA0 together with the newly introduced notion of slow Cauchy sequences; no free parameters or invented entities are introduced.

axioms (1)

standard math RCA0 is the base system of reverse mathematics
Invoked throughout as the conservative base over which the new developments remain conservative.

pith-pipeline@v0.9.0 · 5452 in / 1189 out tokens · 39946 ms · 2026-05-15T02:51:23.690962+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean; IndisputableMonolith/Cost/FunctionalEquation.lean reality_from_one_distinction; washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We work without rates and speak of slow Cauchy sequences... clusters of equivalences with the infinite pigeonhole principle and the strong cohesive principle... Bolzano-Weierstrass and Arzelà-Ascoli theorems

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

48 extracted references · 48 canonical work pages

[1]

David Belanger,Conservation theorems for the cohesiveness principle, 2022, arXiv:2212.13011

work page arXiv 2022
[2]

Errett Bishop,Foundations of constructive analysis, McGraw-Hill, New York, 1967

work page 1967
[3]

8, article no

Vasco Brattka,A Galois connection between Turing jumps and limits, Logical Methods in Computer Science14(2018), no. 8, article no. 13

work page 2018
[4]

6, 623–655

Vasco Brattka, Guido Gherardi, and Alberto Marcone,The Bolzano-Weierstrass Theorem is the jump of Weak K˝ onig’s Lemma, Annals of Pure and Applied Logic163(2012), no. 6, 623–655

work page 2012
[5]

Slaman,On the strength of Ramsey’s theorem for pairs, The Journal of Symbolic Logic66(2001), no

Peter Cholak, Carl Jockusch, and Theodore A. Slaman,On the strength of Ramsey’s theorem for pairs, The Journal of Symbolic Logic66(2001), no. 1, 1–55

work page 2001
[6]

C. T. Chong, Steffen Lempp, and Yue Yang,On the role of the collection principle forΣ 0 2- formulas in second-order reverse mathematics, Proceedings of the American Mathematical Society138(2010), no. 3, 1093–1100

work page 2010
[7]

1, 195–206

Chris Conidis and Theodore Slaman,Random reals, the rainbow Ramsey theorem, and arith- metic conservation, The Journal of Symbolic Logic78(2013), no. 1, 195–206

work page 2013
[8]

3, 455–490

Damir Dzhafarov, Stephen Flood, Reed Solomon, and Linda Westrick,Effectiveness for the dual Ramsey theorem, Notre Dame Journal of Formal Logic62(2021), no. 3, 455–490

work page 2021
[9]

Problems, Reductions, and Proofs, Theory and Applications of Computability, Springer, Cham, 2022

Damir Dzhafarov and Carl Mummert,Reverse Mathematics. Problems, Reductions, and Proofs, Theory and Applications of Computability, Springer, Cham, 2022

work page 2022
[10]

2248, article no

David Fern´ andez-Duque, Paul Shafer, Henry Towsner, and Keita Yokoyama,Metric fixed point theory and partial impredicativity, Philosophical Transactions of the Royal Society A 381(2023), no. 2248, article no. 20220012

work page 2023
[11]

David Fern´ andez-Duque, Paul Shafer, and Keita Yokoyama,Ekeland’s variational principle in weak and strong systems of arithmetic, Selecta Mathematica26(2020), article no. 68

work page 2020
[12]

4, 479–483

Anton Freund,What is effective transfinite recursion in reverse mathematics?, Mathematical Logic Quarterly66(2020), no. 4, 479–483

work page 2020
[13]

Anton Freund and Patrick Uftring,More conservativity for weak K˝ onig’s lemma, Documenta Mathematica (to appear), 21 pp, doi:10.4171/DM/1049

work page doi:10.4171/dm/1049
[14]

James, ed.), vol

Harvey Friedman,Some systems of second order arithmetic and their use, Proceedings of the International Congress of Mathematicians, Vancouver 1974 (Ralph D. James, ed.), vol. 1, Canadian Mathematical Congress, 1975, pp. 235–242

work page 1974
[15]

osu.edu/friedman.8/files/2021/12/RMfoundingETF122921a.pdf(accessed on 23 December 2025)

,The emergence of (strict) revese mathematics, 2021, Manuscript available atu. osu.edu/friedman.8/files/2021/12/RMfoundingETF122921a.pdf(accessed on 23 December 2025). A VOIDING LOGICAL STRENGTH IN REAL ANALYSIS 59

work page 2021
[16]

,Strict reverse mathematics/1-3, 2025, Manuscripts of three talks at the Erwin Schr¨ odinger Institute, Vienna, 20-28 August 2025, available atesi.ac.at/events/e554/(ac- cessed on 21 December 2025)

work page 2025
[17]

Herman Geuvers, Milad Niqui, Bas Spitters, and Freek Wiedijk,Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science17(2007), 3–36

work page 2007
[18]

Petr H´ ajek and Pavel Pudl´ ak,Metamathematics of first-order arithmetic, Perspectives in Mathematical Logic, Springer, Berlin, 1993

work page 1993
[19]

1, 171–206

Denis Hirschfeldt and Richard Shore,Combinatorial principles weaker than Ramsey’s theorem for pairs, The Journal of Symbolic Logic72(2007), no. 1, 171–206

work page 2007
[20]

11, 5805–5837

Denis Hirschfeldt, Richard Shore, and Theodore Slaman,The atomic model theorem and type omitting, Transactions of the American Mathematical Society361(2009), no. 11, 5805–5837

work page 2009
[21]

Jeffry Hirst,Combinatorics in subsystems of second order arithmetic, PhD thesis, Pennsylvania State University, 1987

work page 1987
[22]

Mathematics55(2007), no

,Representations of reals in reverse mathematics, Bulletin of the Polish Academy of Sciences. Mathematics55(2007), no. 4, 303–316

work page 2007
[23]

1, 99–120

Chun-Kuen Ho,Relatively recursive reals and real functions, Theoretical Computer Science 210(1999), no. 1, 99–120

work page 1999
[24]

Carl Jockusch and Frank Stephan,A cohesive set which is not high, Mathematical Logic Quarterly39(1993), 515–530

work page 1993
[25]

Ulrich Kohlenbach,Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals, Archive for Mathematical Logic36(1996), 31–71

work page 1996
[26]

3, 223–245

,Things that can and things that cannot be done inPRA, Annals of Pure and Applied Logic102(2000), no. 3, 223–245

work page 2000
[27]

,Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, Springer, Berlin and Heidelberg, 2008

work page 2008
[28]

II, World Scientific, 2018, pp

,Proof-theoretic methods in nonlinear analysis, Proceedings of the International Con- gress of Mathematicians, Rio de Janeiro 2018 (Boyan Sirakov, Paulo Ney de Souza, and Marcelo Viana, eds.), vol. II, World Scientific, 2018, pp. 79–102

work page 2018
[29]

Christoph Kreitz and Klaus Weihrauch,Theory of representations, Theoretical Computer Science38(1985), 35–53

work page 1985
[30]

Kreuzer,The cohesive principle and the Bolzano-Weierstraß principle, Math- ematical Logic Quarterly57(2011), no

Alexander P. Kreuzer,The cohesive principle and the Bolzano-Weierstraß principle, Math- ematical Logic Quarterly57(2011), no. 3, 292–298

work page 2011
[31]

3, 177–183

,From Bolzano-Weierstraß to Arzel` a-Ascoli, Mathematical Logic Quarterly60(2014), no. 3, 177–183

work page 2014
[32]

1, article no

Quentin Le Hou´ erou, Ludovic Patey, and Keita Yokoyama, Π 0 4 conservation of Ramsey’s theorem for pairs, Journal of the London Mathematical Society113(2026), no. 1, article no. e70419

work page 2026
[33]

Andrew E. M. Lewis-Pye,The search for natural definability in the Turing degrees, Comput- ability7(2018), no. 2-3, 189–235

work page 2018
[34]

2, 609–620

Jiayi Liu,RT 2 2 does not implyWKL 0, The Journal of Symbolic Logic77(2012), no. 2, 609–620

work page 2012
[35]

8, University of Toronto Press, Toronto, 1953

Georg Lorentz,Bernstein polynomials, Mathematical Expositions, vol. 8, University of Toronto Press, Toronto, 1953

work page 1953
[36]

Webb Miller and D. A. Martin,The degrees of hyperimmune sets, Zeitschrift f¨ ur Mathe- matische Logik und Grundlagen der Mathematik14(1968), 159–166

work page 1968
[37]

Ludovic Patey and Keita Yokoyama,The proof-theoretic strength of Ramsey’s theorem for pairs and two colors, Advances in Mathematics330(2018), 1034–1070

work page 2018
[38]

Weiguang Peng and Takeshi Yamazaki,Two kinds of fixed point theorems and reverse math- ematics, Mathematical Logic Quarterly63(2017), 454–461

work page 2017
[39]

Pour-El and J

Marian B. Pour-El and J. Ian Richards,Computability in analysis and physics, Springer, Berlin and Heidelberg, 1989

work page 1989
[40]

Special Issue on Computability and Com- plexity in Analysis54(2008), no

St´ ephane Le Roux and Martin Ziegler,Singular coverings and non-uniform notions of closed set computability, Mathematical Logic Quarterly. Special Issue on Computability and Com- plexity in Analysis54(2008), no. 5, 545–560

work page 2008
[41]

4, 570–582

David Seetapun and Theodore Slaman,On the strength of Ramsey’s theorem, Notre Dame Journal of Formal Logic36(1995), no. 4, 570–582

work page 1995
[42]

60 ANTON FREUND, NICHOLAS PISCHKE, AND PATRICK UFTRING

Stephen Simpson,Subsystems of second order arithmetic, Perspectives in Logic, Cambridge University Press, 2009. 60 ANTON FREUND, NICHOLAS PISCHKE, AND PATRICK UFTRING

work page 2009
[43]

Theodore Slaman, Σ n-bounding and∆ n-induction, Proceedings of the American Mathemat- ical Society1032(2004), 2449–2456

work page 2004
[44]

3, 145–158

Ernst Specker,Nicht konstruktiv beweisbare S¨ atze der Analysis, The Journal of Symbolic Logic14(1949), no. 3, 145–158

work page 1949
[45]

Troelstra and Dirk van Dalen,Constructivism in mathematics, vol

Anne S. Troelstra and Dirk van Dalen,Constructivism in mathematics, vol. 1, Studies in Logic and the Foundations of Mathematics, vol. 121, North-Holland, Amsterdam, 1988

work page 1988
[46]

4, article no

Patrick Uftring,Weak and strong versions of effective transfinite recursion, Annals of Pure and Applied Logic174(2023), no. 4, article no. 103232, 15 pp

work page 2023
[47]

Klaus Weihrauch,Computable analysis, Springer, Berlin and Heidelberg, 2000

work page 2000
[48]

Anton Freund, University of W ¨urzburg, Institute of Mathematics, Emil-Fischer- Str

Martin Ziegler,Revising type-2 computation and degrees of discontinuity, Electronic Notes in Theoretical Computer Science167(2007), 255–274, Proceedings of the Third International Conference on Computability and Complexity in Analysis (CCA 2006). Anton Freund, University of W ¨urzburg, Institute of Mathematics, Emil-Fischer- Str. 40, 97074 W ¨urzburg, Ger...

work page 2007