RCA0 versus WKL0 versus ACA0

[Harvey Friedman]

Chow's probing posting
https://cs.nyu.edu/pipermail/fom/2021-May/022673.html immediately
suggests, among other things, the question of finding really
interesting sufficient conditions for the function in fixed point
theorems such as Brouwer's to have an effective fixed point, or for
weakened forms of the fixed point theorems to be provable ein RCA0.

One can of course start with the comparatively trivial theorem that
every uniformly continuous function f: [0,1] into [0,1] has a fixed
point.

It would seem that the whole matter rests on the nature of sequences
x,fx,ffx,fffx,... . and the Bolzano Weierstrass theorem, but this is
WRONG. BW is provably equivalent to ACA0 over RCA0.

POSSIBLE LINE OF INVESTIGATION? Take simple and not so simple
fundamental statements that are not provable in RCA0, be they
equivalent to WKL0 or ACA0 (or whatever). Analyze and classify the
additional natural hypotheses one can place for them that does make
the statement provable in RCA0. As is well known, being a CONTRACTION
is sufficient. This is the Contraction Mapping Theorem, where the
fixed point is even unique. But one wants weaker sufficient conditions
than Contraction to get an effective fixed point. OR IS THERE A RESULT
that in a sense, the only condition of a certain shape that works here
is Contraction?

Harvey Friedman