Countable sums in ZF

[Sam Sanders]

Dear Tim, dear FOM, 

> I was surprised to learn recently that the proof of "a positive real-valued function on [0,1] has a positive integral" requires countable choice (Kanovei and Katz, Real Analysis Exchange 42 (2017), 385-390).
> 
> Years ago, on MathOverflow, the following theorem was cited as being trickier to prove than it looks: If I_1, I_2, ... are intervals of real numbers with lengths that sum to less than 1, then their union cannot be all of [0,1].  Is there anything interesting about this theorem from a reverse mathematics perspective?

As it happens, Dag Normann and I have been working on this kind of thing in connection to the uncountability of R.  Here is an arxiv preprint:  

https://arxiv.org/abs/2007.07560

Note that we work in higher-order arithmetic (mostly third-order): the usual 
coding of third-order objects is generally not done.  And with exquisite consequences:

In a nutshell, the “uncountability of R” can be expressed as 

NIN: there is no injection from [0,1] to N.

NBI: there is no bijection from [0,1] to N.  

NIN and NBI are hard to prove, the objects claimed to exist
are hard to compute (Kleene S1-S9), relative to the usual scale
of comprehension and discontinuous functionals.  Full second-
order arithmetic is needed, in fact.  No fragment of AC is needed.  

We have come to view these “hard to prove/compute” features 
as just a choice of the wrong scale: there is an alternative “non-normal" scale
based on (classically) valid continuity axioms from Brouwer’s intuitionistic math.
On this non-normal scale, NIN and NBI are among the weakest principles
of third-order arithmetic.

Indeed, many thms of ordinary mathematics imply NIN or NBI, and I 
mention just a few that relate to the thms you mention above,
Note that “countable” has its usual definition (injection or bijection to N).

1) Arzela’s 1885 convergence thm for the Riemann integral.
2) The above with “convergence” replaced by Tao's metastability.
3) Heine-Borel/Vitali/Lindeloef covering lemmas for uncountable coverings of [0,1]
4) The above for *countable* collections of open intervals.
5) A closed set (in the sense of RM) that is countable, has finite measure. 
6) The well-known fragments of Ramsey’s theorem formulated for countable sets.

I point out that Borel himself formulated the Heine-Borel thm as in 4), 
while Ramsey made use of set theoretic formulation relates to Ramsey’s thm.

We list a large number of examples in the aforementioned paper (esp. the Appendix).  
The Ramsey stuff is not in this paper.  

Note that 2) and 4) suggests a certain robustness, while 1) and 5) suggests that
coding third-order objects can dramatically change which comprehension
axioms are needed to prove a given thm, even for basic math like the Riemann integral.  

Best,

Sam