Fixed point theorems for constructive metric spaces?

Question

Banach's fixed point theorem says that if we have a nonempty complete metric space $A$, then any uniformly contractive function $f : A \to A$ it has a unique fixed point $\mu(f)$. However, the proof of this theorem requires the axiom of choice -- we need to choose an arbitrary element $a \in A$ to start iterating $f$ from, to get the Cauchy sequence $a, f(a), f^2(a), f^3(a), \ldots$.

1. How are fixed point theorems stated in constructive analysis?
2. Also, are there any concise references to constructive metric spaces?

The reason I ask is that I want to construct a model of System F in which the types additionally carry metric structure (among other things). It's rather useful that in constructive set theory, we can cook up a family of sets $U$, such that $U$ is closed under products, exponentials, and $U$-indexed families, which makes it easy to give a model of System F.

It would be very nice if I could cook up a similar family of constructive ultrametric spaces. But since adding choice to constructive set theory makes it classical, obviously I need to be more careful about fixed point theorems, and probably other stuff too.

Answer 1

The axiom of choice is used when there is a collection of "things" and you choose one element for each "thing". If there is just one thing in the collection, that's not the axiom of choice. In our case we only have one metric space and we are "choosing" a point in it. So that's not the axiom of choice but elimination of existential quantifiers, i.e., we have a hypothesis $\exists x \in A . \phi(x)$ and we say "let $x \in A$ be such that $\phi(x)$". Unfortunately, people often say "choose $x \in A$ such that $\phi(x)$", which then looks like application of the axiom of choice.

For reference, here is a constructive proof of Banach's fixed point theorem.

Theorem: A contraction on an inhabited complete metric space has a unique fixed point.

Proof. Suppose $(M,d)$ is an inhabited complete metric space and $f : M \to M$ is a contraction. Because $f$ is a contraction there exists $\alpha$ such that $0 < \alpha < 1$ and $d(f(x), f(y)) \leq \alpha \cdot d(x,y)$ for all $x, y \in M$.

Suppose $u$ and $v$ are fixed point of $f$. Then we have $$d(u,v) = d(f(u), f(v)) \leq \alpha d(u,v)$$ from which it follows that $0 \leq d(u,v) \leq (\alpha - 1) d(u,v) \leq 0$, hence $d(u,v) = 0$ and $u = v$. This proves that $f$ has at most one fixed point.

It remains to prove the existence of a fixed point. Because $M$ is inhabited there exists $x_0 \in M$. Define the sequence $(x_i)$ recursively by $$x_{i+1} = f(x_i).$$ We can prove by induction that $d(x_i, x_{i+1}) \leq \alpha^i \cdot d(x_0, x_1)$. From this it follows that $(x_i)$ is a Cauchy sequence. Because $M$ is complete, the sequence has a limit $y = \lim_i x_i$. Since $f$ is a contraction, it is uniformly continuous and so it commutes with limits of sequences: $$f(y) = f(\lim_i x_i) = \lim_i f(x_i) = \lim_i x_{i+1} = \lim_i x_i = y.$$ Thus $y$ is a fixed point of $f$. QED

Remarks:

1. I was careful not to say "choose $\alpha$" and "choose $x_0$". It is common to say such things, and they just add to the confusion that prevents ordinary mathematicians from being able to tell what is and isn't the axiom of choice.

2. In the uniqeness part of the proof people often assume unnecessarily that there are two different fixed points and derive a contradiction. This way they have only managed to prove that if $u$ and $v$ are fixed points of $f$ then $\lnot\lnot (u = v)$. So now they need excluded middle to get to $u = v$. Even for classical mathematics this is suboptimal and just shows that the author of the proof does not exercise good logical hygiene.

3. In the existence part of the proof, the sequence $(x_i)$ depends on the existential witness $x_0$ we get from eliminating the assumption $\exists x \in M . \top$. There is nothing wrong with that. We do that sort of thing all the time. We did not choose anything. Think of it this way: someone else gave us a witness $x_0$ for inhabitedness of $M$, and we are free to do something with it.

4. Classically, "$M$ is inhabited" ($\exists x \in M . \top$) and "$M$ is non-empty" ($\lnot\forall x \in M . \bot$) are equivalent. Constructively, the former makes more sense and is useful.

5. Because we showed uniqueness of fixed points we actually get a fixed-point operator $\mathrm{fix}_M$ from contractions on $M$ to points of $M$, rather than just a $\forall\exists$ statement.

6. Finally, the following fixed-point theorems have constructive versions:

   • Knaster-Tarski fixed-point theorem for monotone maps on complete lattices
   • Banach's fixed-point theorem for contractions on a complete metric space
   • Knaster-Tarski fixed-point theorem for monotone maps on dcpos (proved by Pataraia)
   • Various fixed-point theorems in domain theory usually have constructive proofs
   • Recursion theorem is a form of fixed-point theorem and it has a constructive proof
   • I proved that Knaster-Tarski fixed-point theorem for monotone maps on chain-complete posets does not have a constructive proof. Similarly, the Bourbaki-Witt fixed-point theorem for progressive maps on chain-complete posets fails constructively. The counter-example for the later one comes from the effective topos: in the effective topos ordinals (suitably defined) form a set and the successor maps is progressive and has no fixed points. By the way, the successor map on the ordinals is not monotone in the effective topos.

Now that's rather more information than you asked for.