What is (Bishop style) constructive mathematics?

“Mathematics with the use of intuitionistic logic (and some appropriate set- or type-theoretic foundations).”

Naturally, restricting the logic makes proving results harder and (sometimes impossible).

To “rescue results” we can either *weaken* the outcome, or *strengthen* the assumptions. There’s a few usual suspects.

The following is a quote from "techniques of constructive analysis".

In this chapter we discuss a peculiarly constructive technique that, normally under the hypothesis that one or more of the metric spaces under consideration is complete, enables us to prove results that otherwise would require some nonconstructive principle such as LPO, LLPO, or Markov’s principle.

Finding the square root of a complex number.

*Bishop’s Lemma*

If $A$ is a complete, located subset of a metric space $(X,\rho)$, and $x \in X$, then there exists $y \in A$ such that if $x \neq y$, then $\rho(x,A)>0$.

Bishop’s Lemma is very useful!

Embedding functions $2^{\mathbb{N}} \to \mathbb{R}$ to $[0,1] \to \mathbb{R}$.

*Ishihara’s first trick*

Let $f$ be a strongly extensional mapping of a complete metric space $X$ into a metric space $Y$, and let $(x_{n})_{n \geqslant 1} $ be a sequence in $X$ converging to a limit $x$. Then for all positive numbers $\alpha \lt \beta$, either $\rho(f(x_{n}),f(x)) > \alpha$ for some $n$ or $\rho(f(x_{n}),f(x)) \lt \beta$ for all $n$.

*Ishihara’s second trick*

Let $f$ be a strongly extensional mapping of a complete metric space $X$ into a metric space $Y$, and let $(x_{n})_{n \geqslant 1}$ be a sequence in $X$ converging to a limit $x$. Then for all positive numbers $\alpha \lt \beta$, either $\rho(f(x_{n}),f(x)) \lt \beta$ eventually or $\rho(f(x_{n}),f(x)) > \alpha$ infinitely often.

In constructive reverse mathematics

The following are equivalent:

- Every function $f:[0,1] \to \mathbb{R}$ is strongly extensional.
- For all $a,b \in \mathbb{R}$ every function $f: \overline{ \{ a,b \} } \to \mathbb{R}$ is strongly extensional.

If $X$ is complete then every sequentially continuous $f:X \to \mathbb{R}$ is strongly extensional.

Notice that in all of these examples we actually only ever needed the existence of a very special kind of Cauchy sequence.

Let $(X, \rho)$ be a metric space. For a sequence $x = (x_{n})_{n \geqslant 1}$ in $X$ converging to $x_{\infty} \in X$ and an increasing binary sequence $\lambda = (\lambda_{n})_{n \geqslant 1}$ we define a sequence $\lambda \circledast x $ by One can easily show that this is a Cauchy sequence.

*Definition*

A metric space $(X,\rho)$ is called complete enough, if for every sequence $x = (x_{n})_{n \geqslant 1}$ in $X$ converging to $x_{\infty} \in X$ and every increasing binary sequence $\lambda = (\lambda_{n})_{n \geqslant 1}$ the (Cauchy) sequence $\lambda \circledast x$ converges in $X$.

- Under the assumption of LPO every metric space is complete enough. (Actually this is an equivalence).
- Every complete metric space is complete enough.
- Not the best name.
- Some variations in the definition possible.

So if we can find an (interesting) space that is complete enough but not complete we have generalised (for free)

- Ishihara’s tricks
- Bishop’s Lemma (modulo details)
- …

The original example of a complete enough space that is not complete was the space $\mathbf{P}$ of all permutations $\pi : \mathbb{N} \to \mathbb{N}$.

This was useful in the following: The Riemann permutation theorem states that if every rearrangement of a series converges, then the series is absolutely convergent

Notice that $\mathbf{P}$ can be written in the form

so $\mathbf{P}$ is a $G_\delta$ subset of Baire space.

In fact we can prove:

$G_\delta$ subsets of a complete enough space are also complete enough.

This proposition actually provides us with more examples for spaces that are complete enough, but not necessarily complete:

- Open subsets of complete (enough) spaces,
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ is surjective} \}$,
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ attains $0$ infinitely often} \}$,
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ is increasing} \}$, (actually complete)
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ is strictly increasing} \}$, (actually complete)
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ is injective} \}$, (actually complete)

But there is more: the class of complete enough spaces is bigger than $G_\delta$

Every stable (a set $S$ is stable if $\neg \neg S \subset S$) subset of a metric space is complete enough.

Hence we have even more natural and interesting examples for spaces that are complete enough, but not necessarily complete:

- The irrational numbers and the “irrational” members of Baire space; i.e. the sequences which are are not eventually zero.
- More general: any co-countable set.
- Even more general: any set that is a complement.
- $ \{f \subseteq \mathbb{N}^\mathbb{N} \ \mid \ f \text{ is not unbounded} \}$,

Open questions

- Any good characterisation of complete enough?
- Can we extend an
*arbitrary*functions $f:2^\mathbb{N} \to \mathbb{R}$ to one of $[0,1] \to \mathbb{R}$ - The role of countable choice.