901 Remarks on Reverse Mathematics 6 (Harvey Friedman)

[Ulrich Kohlenbach]

Dear FOM,

in connection with the recent exchange between Harvey Friedman
and Sam Sanders I like to make the following remarks:

For mathematics dealing only with continuous functions, the
approach via codings of the latter as in RM is - from the
perspective of Higher Order Reverse Mathematics (HRM) -
largely unproblematic in view of a result due to Dag Normann
and myself (see Corollary 4.11 in my paper "Foundational and
mathematical uses of higher types", In: Sieg, W. et al. (eds.),
Reflections on the Foundations of Mathematics.
Lecture Notes in Logic vol. 15, pp. 92-116,(2002).):
let F:[0,1]->R be an arbitrary function (represented
as a 3rd order object). If F happens to continuous, then WKL
proves that F has a code in the sense of RM (in my paper
this is stated for Cantor space but it also adapts to e.g.
[0,1] as shown by Dag Normann.

So for continuous functions and compact domains, from WKL_0 on
HRM and RM largely coincide. Also note that the higher order
base system is conservative over the 2nd order one (when the
latter is formulated in an equivalent version with function
variables rather than set variables).

Thus the main emphasis in current HRM as carried out by
Dag Normann and Sam Sanders is on mathematics which is
not restricted to continuous functions.

Shortly after I wrote my old paper on HRM, the need of a w.r.t.
to mathematical practice particularly important different
extension of the 2nd order framework occurred to me in the
context of proof mining: namely the use of abstract metric,
normed etc. spaces X which are added as atoms to the system
and are not defined as completions of countable spaces and
hence not assumed to be separable. This is crucial in the
extraction of highly uniform bounds from proofs which are
uniform not just w.r.t. parameters in compact spaces but from
parameters in metrically bounded substructures. If separability
is used, the separability property itself provides a
counterexample to this since the uniform version of it
(restricted to - say - the unit ball) gives the total
boundedness of the latter (and so in the normed case implies
finite dimension). Even though the bounds are mostly of
interest only for concrete Polish spaces such as X=L^2[0,1]
it is necessary to treat X as an abstract (here
Hilbert-)space in order to get (even just for L^2[0,1]!) a
uniform bound. So to some extent separability assumptions may
destroy the numerical content of a proof (Kreisel once mentioned
to me that Serre already in the 50's made some comment to him in
this direction). The addition of such abstract spaces largely
does not increase the proof-theoretic strength as one can
interpret these spaces also as Polish spaces and so they do
not create any foundational challenge (but is essential in
most of the by now about 100 concrete proof minings). It seems 
that Harvey Friedman's suggestion for extensions of RM by
"new sorts and new relations and operations" goes into a similar 
direction.

In proof mining, *both* abstract spaces X and higher types (formed
over N and X) are used where the latter occur mostly implicitly in
the course of Dialectica-style arguments while the mathematically
statements considered themselves usually use at most type level 2
(i.e. 3rd oder).

Best,
Ulrich Kohlenbach