[FOM] Reverse Mathematics and higher types

sasander at cage.ugent.be sasander at cage.ugent.be
Mon Mar 19 17:49:39 EDT 2018

```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.

```