<p>The axiom of choice is used when there is a <em>collection</em> 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 "<em>choose</em> $x \in A$ such that $\phi(x)$", which then looks like application of the axiom of choice.</p>

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

<p><strong>Theorem:</strong> A contraction on an inhabited complete metric space has a unique fixed point.</p>

<p><em>Proof.</em> 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 &lt; \alpha &lt; 1$ and $d(f(x), f(y)) \leq \alpha \cdot d(x,y)$ for all $x, y \in M$.</p>

<p>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.</p>

<p>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</p>

<p>Remarks:</p>

<ol>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>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.</p></li>
<li><p>Finally, the following fixed-point theorems have constructive versions:</p>

<ul>
<li>Knaster-Tarski fixed-point theorem for monotone maps on complete lattices</li>
<li>Banach's fixed-point theorem for contractions on a complete metric space</li>
<li>Knaster-Tarski fixed-point theorem for monotone maps on dcpos (proved by Pataraia)</li>
<li>Various fixed-point theorems in domain theory usually have constructive proofs</li>
<li>Recursion theorem is a form of fixed-point theorem and it has a constructive proof</li>
<li>I proved that Knaster-Tarski fixed-point theorem for monotone maps on <em>chain-complete</em> posets does <em>not</em> 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 <em>not</em> monotone in the effective topos.</li>
</ul></li>
</ol>

<p>Now that's rather more information than you asked for.</p>

CC BY-SA 2.5
2011-04-07T16:25:38.180Z
Do any of the axioms of metric spaces need to be reformulated?
Neel Krishnaswami
CC BY-SA 2.5
2011-04-07T22:08:42.157Z
this is yet another nice answer, Andrej !
Suresh Venkat
CC BY-SA 2.5
2011-04-07T23:10:48.283Z
Thanks for a great answer. Could you suggest instructive material on exercising "good logical hygiene"? That's a delicious term.
Vijay D
CC BY-SA 3.0
2011-04-08T04:18:02.860Z
@Neel: No, the axioms are the same as in the classical case.
Andrej Bauer
CC BY-SA 3.0
2011-04-08T08:17:00.517Z
I see you're shooting for System F. In this case you might want to consider the question whether the fixed-point operator $\mathrm{fix}$ is suitably polymorphic. But first you must answer "is it even a function?" because it looks like there is choice involved in the construction of $\mathrm{fix}$ (for every inhabited complete metric space we "choose" a point). There is no choice, however, since the value of $\mathrm{fix}$ does not depend on the initial point. (continued)
Andrej Bauer
CC BY-SA 3.0
2011-04-08T08:19:28.707Z
Or to put it another way, everything is ok because $\mathrm{fix}$ is the only solution of the fixed-point equation $\mathrm{fix} = \lambda M . \lambda f . f(\mathrm{fix}_M(f))$ where $M$ ranges over inhabited complete metric spaces and $f$ is a contraction on $M$ (if you write down the type you will see polymorphism in $M$).
Andrej Bauer
CC BY-SA 2.5
2011-04-07T09:20:19.710Z
2011-04-07T09:36:40.337Z
2011-04-07T09:36:40.337Z
Andrej Bauer
<p>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$.   </p>

<ol>
<li>How are fixed point theorems stated in constructive analysis? </li>
<li>Also, are there any concise references to constructive metric spaces?</li>
</ol>

<p>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. </p>

<p>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. </p>

CC BY-SA 2.5
2011-04-07T08:10:48.887Z
You can change the hypothesis to $A$ being an [inhabited set](http://en.wikipedia.org/wiki/Inhabited_set). You aren't invoking the axiom of choice to pick $a\in A$.
Colin McQuillan
<reference-request><lo.logic><pl.programming-languages><denotational-semantics><metric-spaces>
Fixed point theorems for constructive metric spaces?
Neel Krishnaswami
# Fixed point theorems for constructive metric spaces?

(Asked by: username_0 on 2011-04-07)

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.

**Tags:** reference-request, lo.logic, pl.programming-languages, denotational-semantics, metric-spaces

> **Comments:**
> **username_1**: You can change the hypothesis to $A$ being an [inhabited set](http://en.wikipedia.org/wiki/Inhabited_set). You aren't invoking the axiom of choice to pick $a\in A$.  

---

## 1 answers

### Answer by username_2 on 2011-04-07. Score: 22 | Accepted answer

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.

> **Comments:**
> **username_0**: Do any of the axioms of metric spaces need to be reformulated?  
> **username_3**: this is yet another nice answer, Andrej !  
> **username_4**: Thanks for a great answer. Could you suggest instructive material on exercising "good logical hygiene"? That's a delicious term.  
> **username_2**: @Neel: No, the axioms are the same as in the classical case.  
> **username_2**: I see you're shooting for System F. In this case you might want to consider the question whether the fixed-point operator $\mathrm{fix}$ is suitably polymorphic. But first you must answer "is it even a function?" because it looks like there is choice involved in the construction of $\mathrm{fix}$ (for every inhabited complete metric space we "choose" a point). There is no choice, however, since the value of $\mathrm{fix}$ does not depend on the initial point. (continued)  
> **username_2**: Or to put it another way, everything is ok because $\mathrm{fix}$ is the only solution of the fixed-point equation $\mathrm{fix} = \lambda M . \lambda f . f(\mathrm{fix}_M(f))$ where $M$ ranges over inhabited complete metric spaces and $f$ is a contraction on $M$ (if you write down the type you will see polymorphism in $M$).  

---

