Constructive gem: an injection from Baire space to natural numbers

• 15 June 2011
• Andrej Bauer
• Constructive math, Gems and stones, Logic, Publications

I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$.

At the Mathematical Foundations of Programming Semantics XVII, which took place at Carnegie Mellon University in May 2011, Paulo Oliva and Martín Escardó showed a program which witnessed the fact that there was no injection from the Baire space $\mathbb{N}^\mathbb{N}$ to natural numbers $\mathbb{N}$. The program took as input a function $h : \mathbb{N}^\mathbb{N} \to \mathbb{N}$ and produced two sequences $x, y \in \mathbb{N}^\mathbb{N}$ such that $x \neq y$ and $h(x) = h(y)$. Martín Escardó popularized the program as interesting example of extraction of computational content from classical proofs, which lead me to wonder whether there was a constructive proof of the statement
$$\forall h : \mathbb{N}^\mathbb{N} \to \mathbb{N} .
\exists x, y \in \mathbb{N}^\mathbb{N} .
(x \neq y \land h(x) = h(y))$$
that would yield such programs more directly. Fred Richman asked for a constructive proof of the weaker statement that there was no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, and nobody could come up with one.

Classically there is no injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, of course. Constructively, it is easy to see that it must be wildly discontinuous, if it exists. Thus we cannot hope to find one in any of the usual varieties of constructive mathematics, as they all satisfy some kind of continuity principle.

If I am not mistaken, the realizability topos based on infinite time Turing machines by Joel Hamkins contains an injection $\mathbb{N}^\mathbb{N} \to \mathbb{N}$. This is possible because infinite time Turing machines are powerful enough to be able to compute canonical realizers for infinite time computable maps $\mathbb{N} \to \mathbb{N}$. The details are in the paper, attached below. It is likely that the topos can be used for other ominous purposes. For example, it validates the principle LPO but its logic is not classical.

Download: injection.pdf

Comments

Eighth Linkfest

25 June 2011 at 22:04

[...] Andrej Bauer: Constructive Gem: an injection from Baire space to natural numbers [...]

Embedding the Baire space into natural numbers « Mathematics and Computation

06 December 2011 at 16:22

[...] see the post Constructive gem: an injection from Baire space to natural numbers for written notes on this topic. December 6th, 2011 | Category: Talks, [...]

What is an injection in a topos? - mathfreebook

21 July 2016 at 00:34

[…] Space $mathbb{N}^mathbb{N}$ to the natural numbers $mathbb{N}$. This is discussed in Andrej’s blog […]