[FOM] Reverse Mathematics and higher types

[sasander at cage.ugent.be]

Dear All,

Dag Normann and I have recently submitted the paper:

?On the mathematical and foundational role of the uncountable"

which may be found here:

https://arxiv.org/abs/1711.08939

In a nutshell, we identify a number of basic/well-known theorems of  
ordinary mathematicswhich require full second-order arithmetic (as  
given by 3E) for a proof.

The oldest such theorem, dating back 135 years, is Cousin?s lemma, aka
the Heine-Borel theorem for uncountable covers (of the unit interval).  A
number of similar ?covering lemmas? are identified, all part of  
third-order arithmetic.

Cousin?s lemma is shown to be equivalent to many basic properties
of the *gauge integral*.  The latter generalises Lebesgue?s integral and
was introduced (in a different form) no ten years later.  The gauge
integral also provides a (the only?) direct formalisation of part of Feynman?s
path integral.

Besides these interesting Reverse Math properties, there are also  
foundational/
philosophical implications:

1) We identify two fairly natural mathematical statements (the uniform  
Lindeloefcovering lemma for Baire space, and Feferman?s mu functional)  
which arepredicatively reducible in isolation, but imply Pi_1^1-CA_0  
when combined, i.e. the combination "blows up" to an impredicative  
system.

2) Cousin?s lemma holds in INT and is hence called ?semi-constructive?  
and ?more constructive than LPO? in the constructive literature.  The  
Lindeloef lemma is even called ?neutral? (since true in INT and RUSS).
But both the Cousin and Lindeloef lemmas require full second-order  
arithmetic (as in 3E) for a classical proof, and calling such  
statements ?semi-constructive? or ?neutral? seems paradoxical (from  
the classical pov).

3) Over the years, FOM has seen claims like

?the Big Five system ACA_0 can capture 85% of ordinary math"

?ATR_0 can prove all math needed for physics?

Cousin?s lemma and its ilk would seem provide rather strong  
counterexamples to such claims.

Best,

Sam Sanders

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.