FOM and representations

[Sam Sanders]

Dear FOM,

I feel the need to remind everyone (including the participants) that this discussion about topology 
is entirely in the realm of heavy coding.  

The Lebesgue number lemma as follows, mentioned by Tim Chow in this discussion, is fairly weak when formulated in the language of second-order arithmetic.  

> Lemma.  Let A be an open covering of a compact metric space.  Then there exists delta > 0 such that every subset of X with diameter less than delta is contained in some element of A.

A basic third-order version is obtained by considering arbitrary Y: [0,1] -> R^+ and the associated canonical cover consisting of the open ball B(x, Y(x)) for any x in [0,1].  

This version is “hard to prove” and the Lebesgue number delta claimed to exist is “hard to compute” (Kleene S1-S9) from the other data, in that full second-order arithmetic comes to the fore.  

What is more, this hardness does not disappear when one goes to third-order functions that are of bounded variation or lower semi-continuous.  

So apparently coding in SOSOA already “breaks down” for countably many points of discontinuity (which is what bounded variation guarantees).  

This may be found in the recent papers by myself and Dag Normann.  

Best,

Sam

PS: Even coding continuous functions can be problematic (despite results due to Kohlenbach/Kleene):

https://arxiv.org/abs/1910.07913

Certain versions of the Tietze extension thm drop from the level of ACA_0 to 
the level of RCA_0 when working with third-order functions (that are continuous
on part of their domain).