Fixed point theory in weak second-order arithmetic

We develop a basic part of fixed point theory in the context of weak subsystems of second-order arithmetic. RCA₀ is the system of recursive comprehension and Σ⁰₁ induction. WKL₀ is RCA₀ plus the weak König's lemma: every infinite tree of sequences of 0's and 1's has an infinite path. A topological space X is said to possess the fixed point property if every continuous function f:X→X has a point x ε{lunate} X such that f(x) = x. Within WKL₀ (indeed RCA₀), we prove Brouwer's theorem asserting that every nonempty compact convex closed set C in Rⁿ has the fixed point property, provided that C is expressed as the completion of a countable subset of Qⁿ. We then extend Brouwer's theorem to its infinite dimensional analogue (the Tychonoff-Schauder theorem for R^N) still within RCA₀. As an application of this theorem, we prove the Cauchy-Peano theorem for ordinary differential equations within WKL₀, which was first shown by Simpson without reference to the fixed point theorem. Within RCA₀, we also prove the Markov-Kakutani theorem which asserts the existence of a common fixed point for certain families of affine mappings. Adapting Kakutani's ingenious proof for deducing the Hahn-Banach theorem from the Markov-Kakutani theorem, we also establish the Hahn-Banach theorem for seperable Banach spaces within WKL₀, which was first shown by Brown and Simpson in a different way.