This paper by Normann and Sanders apparently caused a stir in the reverse mathematics community when it came out a couple years ago. It says that Cousin's lemma, which is an extension of the Heine-Borel theorem, requires the full strength of second-order arithmetic (SOA) to prove. It also says this lemma is helpful in mathematically justifying the Feynman path integral. So this is an apparent counterexample to both

  • a) The reverse mathematics precept that theorems of classical analysis can (usually?) be proved using one of the "Big Five" subsystems of SOA, with the strength of subsystem required forming a useful classification of such theorems; and
  • b) Solomon Feferman's argument that scientifically useful mathematics can generally be handled by relatively weak axioms, generally not stronger than PA / ACA0.

I don't exactly have a mathematical question about the Normann-Sanders paper, but would like to know if it has impacted the reverse mathematics program, and what its significance is seen as. Could path integrals really require such powerful axioms?

Also, Cousins' lemma is traditionally fairly easily proved using the completeness property of the real numbers. The issue is that the completeness property is a second-order property of the reals (i.e. it uses a set quantifier), and SOA is a first-order theory of the reals, that doesn't have sets of reals. In classical analysis though, the completeness axiom really does refer to sets of reals, and this result shows that converting a completeness-based proof to a first-order proof isn't so easy (I haven't read the paper closely and have no idea right now how to prove Cousin's lemma in SOA). Is that significant?

I can understand that the (second order) induction axiom from the Peano axioms translates naturally to the induction schema in first order PA, making induction proofs work about the same way as before. I'd be interested to know why analysis is identified with SOA instead of something that allows sets of reals (needed for functions anyway), since there's not such a straightforward translation of the completeness axiom. Analysis=SOA goes back a long way, since the Hilbert program aimed to prove CON(SOA) once it was done with the consistency of arithmetic. Reverse mathematics came much later.


  • 1
    $\begingroup$ That some results don't fit into the Big Five framework is not exactly news; see this and this for example. But examples like this are always interesting. As for what Feferman would say, we can't know for sure, but he might challenge the claim that Cousin's Lemma is indispensable for physics. As I understand it, the "correct" way to formalize the Feynman path integral mathematically is still an open question, so it's still unclear that full SOA is required for path integrals. $\endgroup$ – Timothy Chow May 16 at 13:41
  • $\begingroup$ Tim Chow's comment seems accurate: BOOT (or RANGE) in my below answer is not stronger than $ACA_0$ (in isolation) and implies HBU. One can formalise mathematics using BOOT and stay at the level of $ACA_0$ as long as one avoids $(\exists^2)$. Due to finite measurement precision, we cannot know whether nature involves discontinuous functions (like $(\exists^2)$), i.e. we can avoid those in applications. However, BOOT is "anti-predicativst" as it (essentially) states the existence of the range of an arbitrary third-order functional, i.e. one explicitly quantifies over N^N in its full glory. $\endgroup$ – Sam Sanders May 18 at 11:12
  • 1
    $\begingroup$ @TimothyChow Given that Feynman's path integral can be made to work with an innocent-looking refinement of the Riemann integral (which nonetheless requires some more logical strength as Normann and Sanders show), I am surprised that Feynman's integrals remain so mysterious and controversial. $\endgroup$ – Monroe Eskew May 18 at 15:26
  • 1
    $\begingroup$ As shown by Pat Muldowney (see google), the gauge integral can handle a special case of the Feynman path integral. The infinite dimensional case turns out to be quite subtle, and even then one does not cover all of the applications. $\endgroup$ – Sam Sanders May 18 at 19:37
  • 1
    $\begingroup$ @TimothyChow Measure theory is firmly engrained and will remain so due to inertia. As an argument against the gauge integral, it is often said that the step to the multi-dimensional gauge integral is harder than in the case of the Lebesgue integral, though this seems to be (mostly) a matter of presentation. By contrast, what is great about the gauge integral is Hake's theorem: for any function $f$, if $\lim_{a\rightarrow b} \int_a^c f $ or $\int_b^c f$ exists, then both exist and are equal. This is how physicists (want to) use limits: take limits first and ask questions later/never. $\endgroup$ – Sam Sanders May 19 at 7:43

Sam Sanders here, one of the authors of the paper you mention. Thanks for the nice words. I will answer your questions based on my personal opinion.

You write:

[...] would like to know if it has impacted the reverse mathematics (RM) program, and what its significance is seen as. Could path integrals really require such powerful axioms?

First of all, I cannot speak for the RM community. What I can tell you is that we have gotten all sorts of comments, negative and positive, from lots of (senior) people. I believe it is also fair to say that our paper (and related results) shows that coding even e.g. basic analysis in second-order RM does not accurately represent mathematics. There are those that disagree, as one would expect, but I would speculate people in RM have (on average) started working on "less coding intense" topics. Part of the problem is that second-order arithmetic cannot directly deal with functions from $\mathbb{R}$ to $\mathbb{R}$ that are discontinuous, which is discussed in detail in my "splittings and disjunctions" paper (see arxiv/NDJFL).

Secondly, regarding your question on "powerful" axioms. This ties in nicely with recent results Dag Normann and I have. In a nutshell, the usual scale for measuring logical strength (based on comprehension and discontinuous functionals) is not satisfactory for e.g. Cousin's lemma and we need a second scale, based on (classically valid) continuity axioms from Brouwer's intuitionistic mathematics. This new scale is a Platonist's dream: the canonical ECF embedding maps part of this new scale and equivalences to the 'Big Five' and their equivalences. In other words, the Big Five are merely a reflection of a higher-order truth!

Let me first sketch the main results in our paper pertaining to Cousin's lemma.

We work in the language of higher-order arithmetic. This means that all the below should be interpreted in Kohlenbach's higher-order RM and Kleene's higher-order computability (S1-S9). Not much specific knowledge of these frameworks is needed, however.

Let HBU be Cousin's lemma for [0,1], i.e. for any $\Psi:[0,1] \rightarrow \mathbb{R}^+$, there are $y_0, ..., y_k \in [0,1]$ such that $\cup_{i\leq k} B(y_i, \Psi(y_i))$ covers $[0,1]$. In other words, the reals $y_0, ..., y_k \in [0,1]$ provide a finite sub-covering of the uncountable covering $\cup_{x\in [0,1]}B(x,\Psi(x))$.

Let $Z_2$ be second-order arithmetic with language $L_2$. The systems $Z_2^\omega$ and $Z_2^\Omega$ are known conservative extensions of $Z_2$. Then the former cannot prove HBU while the latter can. This is what we mean by "a proof of HBU requires full second-order arithmetic", as $Z_2^\omega$ cannot prove HBU, but $Z_2^\Omega$ can.

Clearly, HBU is a statement in the language of third-order arithmetic. The system $Z_2^\omega$ is also third-order in nature: it includes, for any $k \geq 1$, a third-order functional $S_k$ that decides $\Pi_k^1$-formulas from $L_2$ in Kleene normal form (see the work of Sieg & Feferman). The system $Z_2^\Omega$ is fourth-order, as it is based on Kleene's (comprehension) quantifier $\exists^3$ (see the work of Kleene on higher-order recursion theory). Note in particular that HBU is provable in ZF: countable choice is not needed.

There are many statements that exhibit the same (or similar) behaviour as HBU. I refer to e.g. our paper on Pincherle's theorem (APAL) and open sets (JLC), where whole lists can be found, as well as the original paper. Convergence theorems for nets in $[0,1]$ indexed by Baire space also behave like HBU (see my 2019 CiE and WolliC papers).

Now that we have established the results, let me explain what these results mean. Indeed, there is an apparent contradiction here: on one hand, HBU should be intuitively weak, but we need absurdly strong comprehension axioms to prove HBU. This feeling you express in your posting, I believe.

The fundamental problem is that we are comparing apples and oranges as follows:

The aforementioned comprehension functionals $\exists^3$ and $S_k$ are discontinuous (in the usual sense of mathematics). By contrast, HBU does not imply the existence of a discontinuous function (say on $\mathbb{R}$ or Baire space). Let us call a (third-order) theorem 'normal' if it implies the existence of a discontinuous function on $\mathbb{R}$, and 'non-normal' otherwise.

It is an empirical observation that there are many non-normal theorems (like HBU) that cannot be proved in $Z_2^\omega$, but can be proved in $Z_2^\Omega$. In other words, the usual 'normal' scale based on comprehension functionals is not a good scale for analysing the strength of non-normal theorems.

In a nutshell: normal theorems = apples and non-normal theorems = oranges.

An obvious follow-up question is:

What is a good scale for analysing non-normal theorems?

As explored in the following paper (see Section 5), the neighbourhood function principle NFP provides the right scale.


NFP is a classically valid continuity axiom from Brouwer's intuitionistic mathematics.
Fragments of NFP are equivalent to e.g. HBU and other milestone non-normal theorems, like the monotone convergence theorem for nets in [0,1] (called $\textsf{MCT}_{\textsf{net}}$ in the above paper). Note that NFP was introduced under a different name by Troelstra-Kreisel, and is mentioned in Troelstra & van Dalen.

Finally, the Kleene-Kreisel 'ECF' embedding is the canonical embedding of higher-order into second-order arithmetic. It maps third-order and higher objects to second-order associates/RM-codes, which reflects the 'coding practise' of RM.

What is more, the ECF embedding maps equivalences involving HBU to equivalences involving WKL, as follows:

HBU $\leftrightarrow$ Dini's theorem for nets (indexed by Baire space).

is mapped by ECF to

HBC $\leftrightarrow$ Dini's (usual) theorem (for sequences),

where HBC is the Heine-Borel theorem for countable coverings of intervals.

Another example is the following:

RANGE $\leftrightarrow$ Monotone convergence theorem for nets (indexed by Baire space)

is mapped by ECF to

range $\leftrightarrow$ Monotone convergence theorem (for sequences),

where RANGE states that the range of a third-order function exists, while range states that the range of a (second-order) function exists; it is well-known that range $\leftrightarrow \textsf{ACA}_0$.

In general, the Big Five equivalences are a reflection of higher equivalences under ECF as in the following picture:

The Big Five as a reflection of a higher truth

Since ECF is a lossy translation, this pictures resembles -in my not so humble opinion- the allegory of the cave by Plato. This observation is inspired by Steve Simpson's writings on Aristotle that can be found in the (RM) literature.

I would like to finish this answer with a history lesson: I have heard wildly inaccurate claims from very smart (RM) people about the history of mathematics. These claims are often used to justify the coding practise of RM. So let us set the historical record straight, while it still matters.

1) Hilbert and Bernays did NOT introduce second-order arithmetic. In the "Grundlagen der Mathematik", they formalise a bunch of math in a logical system $H$ (see esp. Supplement IV). This system involves third-order parameters in an essential way, as has been observed before by e.g. Sieg (see e.g. his book on Hilbert's program). Hilbert-Bernays vaguely sketch how one could perhaps do the same formalisation with less.

I was told that Kreisel then introduced second-order arithmetic based on the above.

2) Riemann's Habilschrift established discontinuous functions as part of the mathematical mainstream around 1850. Thus, discontinuous functions definitely predate set theory.

3) The modern concept of function was already formulated by Dedekind and Lobasjevski in the 1830ies. (This view is not without its critics)

4) The gauge integral is more general than the Lebesgue integral. The main theorems (Hake and FTC) of the former in particular apply to any (possibly non-measurable) function. In this way, the development of the gauge integral does not need measure theory, but can instead be done similarly to the Riemann integral. To study the gauge integral restricted to measurable functions goes against its generalist/historical spirit, to say the least.

5) There are a number of formalism to give meaning to Feynman's path integral. The gauge integral is heralded as one of the few that can avoid 'imaginary time', a desirable feature from the pov of physics. This is briefly discussed on page 20 here:


References are provided, of course.

| cite | improve this answer | |
  • $\begingroup$ Thanks! For those following along, "Splitting and Disjunctions" is here and this paper also looks relevant. I'm still reading them. $\endgroup$ – none May 20 at 22:42
  • 1
    $\begingroup$ The main theme of the "Splittings and ..." paper is the following: on one hand there are only few results in second-order Reverse Mathematics where one can prove $A\leftrightarrow [B \wedge C]$ (a splitting), where $B$ and $C$ are independent and natural. There are only very few results in second-order Reverse Mathematics where one can prove $D\leftrightarrow [E \vee F]$ (a disjunction), where $E$ and $F$ are independent and natural. On the other hand, I identify a plethora of such splittings and disjunctions in higher-order Reverse Mathematics. I also discuss the cause of this observation. $\endgroup$ – Sam Sanders May 22 at 12:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.