Is there a constructive proof that $2^X$ can't inject into $X$?

259 Views Asked by At

Let $X$ be a set. Constructively, it is not hard to show that $\mathcal{P}(X)$ does not inject into $X$: If $f : \mathcal{P}(X) \rightarrow X$ is an injection, consider $D := \lbrace x \in X \mid \exists Y f(Y) = x \wedge x \not\in Y \rbrace$. Then $f(D) \in D \Leftrightarrow f(D) \not\in D$.

However, this argument doesn't carry over if we replace $\mathcal{P}(X)$ with $2^X$, since the $D$ from above cannot generally be assumed to be decidable. Is there another argument that works for $2^X$ or is the statement that $2^X$ doesn't inject into $X$ independent of constructive mathematics?

Edit: $2^X$ is the set of functions from $X$ to $\lbrace 0,1\rbrace$, or equivalently, the decidable subsets of $X$. In constructive mathematics we are not able to conflate $\mathcal{P}(X)$ and $2^X$.

1

There are 1 best solutions below

1
On BEST ANSWER

It's consistent with constructive mathematics that there is an injection from $\mathbb{N}^\mathbb{N} \rightarrow \mathbb{N}$, and in particular composing with the inclusion $2^\mathbb{N} \hookrightarrow \mathbb{N}^\mathbb{N}$ gives an injection $2^\mathbb{N} \rightarrow \mathbb{N}$.

This was proved not so long ago by Andrej Bauer in An injection from the Baire space to natural numbers. The proof is basically to work in a realizability model over infinite time Turing machines. Similarly to the more usual forms of realizability, in the model the functions $\mathbb{N} \rightarrow \mathbb{N}$ are those that are computable by some infinite time Turing machine, $\psi_e$. However, with infinite time Turing machines we can compute a partial function $r : \mathbb{N} \rightarrow \mathbb{N}$ such that if $\psi_e$ is total, then $r(e)$ is defined and $\psi_{r(e)} = \psi_e$, and so that if $\psi_e = \psi_{e'}$ (ie $e$ and $e'$ are programs that happen to give the same function), then $r(e) = r(e')$. In the realizability model, this means that we get an actual well defined function $R\colon \mathbb{N}^{\mathbb{N}} \rightarrow \mathbb{N}$ such that for any $f \in \mathbb{N}^\mathbb{N}$, $f = \psi_{R(f)}$. Any such function is necessarily injective.