$\text{WKL}_0$ proves Brouwer's fixed point theorem for continuous functions on $\lbrack 0,1 \rbrack^n$, when $n$ is finite. What subsystem of second order arithmetic is needed to prove Brouwer's fixed point theorem for $\lbrack 0,1 \rbrack^\omega$ (i.e., the infinite dimensional unit interval)?


Too long for a comment (and if I'm missing a subtlety, my apologies):

Stephen Simpson's Subsystems of Second Order Arithmetic, second edition, Theorem IV.7.9, page 152, proves Schauder's fixed point theorem which seems to be what you're looking for:

The following is provable in $\mathsf{WKL_0}$. Let $C$ be a nonempty closed convex set in $[−1, 1]^{\mathbb{N}}$ . Then every continuous function $f\colon C \to C$ has a fixed point.

The entire section IV.7 is devoted to fixed point theorems.

  • 1
    $\begingroup$ You could be interested in this question on MathOverflow where you can find a number of resources and references for reverse mathematics. $\endgroup$ – Martin Jan 27 '13 at 20:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.