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 / RCA0.

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.

Thanks!

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.

Thanks!