RCA0 versus WKL0 versus ACA0

[Vasco Brattka]

The Brouwer fixed point theorem (BFT) has been carefully analyzed
in Weihrauch complexity (which can be seen as a uniform computability
theoretic version of reverse mathematics) by Stéphane Le Roux,
Joseph S. Miller, Arno Pauly and myself, see

   https://arxiv.org/abs/1206.4809

and there are currently not all too many versions known,
where a computable fixed point exists in general:

1. Regarding BFT for Lipschitz continuous functions with
    Lipschitz constant L the following is known:

    a. if L<1, then one has the Banach fixed point theorem
       which is fully uniformly computable.

    b. if L=1, then the BFT is related to the
       Browder-Göhde-Kirk fixed point theorem, which
       has been carefully analyzed by Eike Neumann, see

       https://arxiv.org/abs/1506.05127

       The theorem is not uniformly computable, but whether
       there exist computable fixed points for computable functions
       or not depends on the dimension of the space.

    c. if L>1, then the BFT is uniformly computably equivalent
       (i.e. Weihrauch equivalent) to WKL and the full BFT
       (see the first cited article above).

    The question of the dependency of BFT on L has originally
    been raised by Ulrich Kohlenbach.

2. Regarding the dimension d of the underlying space
    the following is known:

    a. if d=1, then the BFT reduces to the intermediate value theorem.
       In this case there are always computable zeros for computable
       functions, but they cannot be determined in a uniform computable
       way in general.

    b. if d>2, then there is a simple geometric argument
       that helps to show that the BFT is uniformly computably
       equivalent (i.e. Weihrauch equivalent) to WKL.

    c. if d=2, then BFT is also Weihrauch equivalent to WKL,
       but the proof that we have is considerably more complicated
       and there are interesting open questions regarding
       pathwise connectedness versus connectedness
       in dimension 2 (see the article above).

3. Finally, it is easy to see that the BFT restricted to the
    case of uniquely determined fixed points, is fully uniformly
    computable. (Also isolated fixed points of computable
    functions are always computable etc.)

Of course, it is an interesting topic to determine other
meaningful conditions that one could impose on continuous
functions in order to get a (non-uniform or uniform)
computable version of the Brouwer fixed point theorem.

Also the questions regarding the fundamental group
are interesting and they have not yet been studied
in the above setting.

Kind regards

Vasco Brattka

PS A survey on Weihrauch complexity can be found here:

    https://arxiv.org/abs/1707.03202

Section 8 contains lists of many known equivalences in this setting.
A related bibliography can be found here:

    http://cca-net.de/publications/weibib.php


> Date: Mon, 17 May 2021 00:20:28 -0400
> From: Harvey Friedman <hmflogic at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: RCA0 versus WKL0 versus ACA0
> Message-ID:
> 	<CACWi-GX_QxnSYQsyDqkhXLe9p5+3KLBEkFVkFWEp-mr-xeuY-w at mail.gmail.com>
> Content-Type: text/plain; charset="UTF-8"
> 
> 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
> 
>