DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics
by Mark Bickford
We present a proof of Brouwerâ€™s fixedpoint theorem in intuitionistic mathematics. Unlike most constructive proofs of the theorem it does not use Spernerâ€™s lemma. Instead, we first reduce the theorem to the no-retraction theorem and then use a constructive version of a proof by Karol Sieclucki that there is no retraction |K| â†’ |âˆ‚K| from a n-dimensional complex to its boundary. In our constructive version of this theorem we use rational cubical complexes rather than arbitrary simplicial complexes. We define the the polyhedron |K| of a cubical complex K to be the stable union of the cubes in K. We prove that a stable union of finitely many compact spaces is compact and this allows us to conclude that |K| is compact. In intuitionistic mathematics we may then derive a strong version of the fixedpoint theorem using the fact that all functions from a compact metric space to another metric space are uniformly continuous. Our proof has been completely checked using the proof assistant Nuprl. Nuprlâ€™s type theory is fully intuitionistic because it includes free choice sequences and has rules for bar induction and a continuity principle for numbers. Our argument could also be carried out in the system BISH of Bishopâ€™s school by proving the theorem only for uniformly continuous functions. Some additional work would be needed to prove that certain homeomorphisms (e.g. between a ball and a cube) are uniformly continuous, so we have not made a formal proof in BISH. Our proof is of interest because it is akin to Brouwerâ€™s original proof which used simplicial methods, and because it shows how a statement with constructive content (viz. the existence of an approximate fixedpoint) can be reduced to a statement with no constructive content (the non-existence of a retraction). Also, our use of the stable union, which is crucial to this proof, seems to be novel, and hence, a contribution to the tool kit of constructive mathematics (in both the BISH and INT systems).