Can we prove $|A| < \left|2^{2^A}\right|$ constructively?

Question

Can we prove that there is no:

• Injection $2^{2^A} \to A$
• Surjection $A \to 2^{2^A}$
• Bijection between $A$ and $2^{2^A}$

Constructively?

Answer 1

You can show that there is no injection from $\mathcal{P}(\mathcal{P}(A))$ to $A$ by using Cantor's theorem $|A|<2^{|A|}$. As a consequence, there is no bijection between $\mathcal{P}(\mathcal{P}(A))$ and $A$. Since Cantor's theorem does not require any choice, we can prove the absence of injection without choice.

For the surjection part, use the following fact that is provable without choice:

If there is a surjection from $X$ to $Y$ then $2^{|Y|}\le 2^{|X|}$.

(The proof uses inverse image: if $f:X\to Y$ is a surjection, consider $f^{-1}:\mathcal{P}(Y)\to\mathcal{P}(X)$.)

If there is a surjection from $X$ to $\mathcal{P}(\mathcal{P}(X))$, then $2^{2^{2^{|X|}}}\le 2^{|X|}$, but we have $2^{2^{|X|}}<2^{2^{2^{|X|}}}$, so $2^{2^{|X|}}<2^{|X|}$, a contradiction.

---

As @bof pointed out, Cantor's theorem already excludes the surjection from $A$ to $\mathcal{P}(A)$, so my previous argument is verbose. Also, the OP also asked these facts hold constructively, and the answer is yes (at least over $\mathsf{IZF}$.)

Before answering, I have to point out some subtlety that came from the notation: the OP (supposedly) uses $2^A$ to denote the power set. It makes sense if we are working with classical logic. However, the power set of $A$ need not be bijective with $2^A$ constructively. In general, $\mathcal{P}(A)$ is bijective with $\Omega^A$ for $\Omega=\mathcal{P}(1)$. (Here $A^B$ be the set of all functions from $A$ to $B$.)

The usual proof of Cantor's theorem also works constructively, so $\mathsf{IZF}$ also proves there is no surjection from $A$ to $\mathcal{P}(A)$. Moreover, a slight modification of the proof of Cantor's theorem also shows there is no injection from $\mathcal{P}(A)$ to $A$: assume that there is such an injection $f$. Let $$X=\{a\in A \mid \exists b\in\mathcal{P}(A) [f(b)=a\land a\notin b]\}.$$ We can see easily that $f(X)\in X$ implies $f(X)\notin X$. If $f(X)\notin X$, then there is no $b\in\mathcal{P}(X)$ such that $f(b)=f(X)$ and $f(X)\notin b$, but $b=X$ satisfies that condition, a contradiction.

However, the answer changes if we stick to $2^A$ instead of $\mathcal{P}(A)$: we can still show that there is no surjection between $A$ and $2^A$. The usual proof for Cantor's theorem still works. However, it is consistent with $\mathsf{IZF}$ that there are just two decidable subsets of $\mathbb{R}$. (A subset $X\subseteq A$ is decidable if, for every $a\in A$, we have either $a\in X$ or $a\notin X$.) In that case, $2^{\mathbb{R}}\simeq 2$, hence $2^{2^{\mathbb{R}}}$ is embeddable into $\mathbb{R}$.