Kakutani's fixed point theorem in constructive mathematics

TL;DR

This paper develops a constructive version of Kakutani's fixed point theorem within Bishop's constructive mathematics, addressing challenges in defining uniform continuity and proving the theorem constructively.

Contribution

It provides the first constructive formulation of Kakutani's fixed point theorem and proves its classical equivalence, including a constructive proof of its application to von Neumann's minimax theorem.

Findings

Constructive version of Kakutani's fixed point theorem established

Addressed uniform continuity issues in constructive setting

Proved a constructive generalization of von Neumann's minimax theorem

Abstract

In this paper we consider Kakutani's extension of the Brouwer fixed point theorem within the framework of Bishop's constructive mathematics. Kakutani's fixed point theorem is classically equivalent to Brouwer's fixed point theorem. The constructive proof of (an approximate) Brouwer's fixed point theorem relies on a finite combinatorial argument; consequently we must restrict our attention to uniformly continuous functions. Since Brouwer's fixed point theorem is a special case of Kakutani's, the mappings in any constructive version of Kakutani's fixed point theorem must also satisfy some form of uniform continuity. We discuss the difficulties involved in finding an appropriate notion of uniform continuity, before giving a constructive version of Kakutani's fixed point theorem which is classically equivalent to the standard formulation. We also consider the reverse constructive mathematics of Kakutani's fixed point theorem, and provide a constructive proof of Kakutani's first application of his theorem---a generalisation of von Neumann's minimax theorem.