# Brouwer's fixed point theorem for infinite dimensional real space in subsystems of second order arithmetic

$\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)?

## 1 Answer

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.

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