KnowledgeBase » PUBLICATION » ID = 778

DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics

by Mark Bickford
2020

• PDF

Abstract
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).