Is the dual of Cantor's theorem provable without choice? without excluded middle? For the sake of concreteness let's say we're talking about ZF, though I imagine this question can be asked for any 'typical' set theory without a choice axiom (and would prefer an answer that doesn't rely on some particular detail about ZF specifically).
Let $X$ be a set and $\mathcal{P}X$ its power set. Cantor's theorem states that there exists no surjective map $X \to \mathcal{P}X$ (and therefore no bijection between the two). The usual proof of this fact by diagonalization is entirely constructive, and goes through just fine in an intuitionistic setting without the use of any choice axioms.
One might ask about a dual version of this theorem: that there exists no injective map $\mathcal{P}X \to X$.
Can this be proven without appeal to a choice axiom?
Can it be proven without appeal to the law of excluded middle?
 A: As far as the axiom of choice part goes, this is quite easy. If $f\colon X\to Y$ is an injective function, the either $X$ is empty, or there is $g\colon Y\to X$ such that $g(f(x))=x$.
To see this, note that if $x$ is not empty, then we can fix $x_0\in x$ and define $g(y)=x$ exactly when $f(x)=y$, and if not such $x$ exists, then $g(y)=x_0$.
No choice necessary here. But of course, we did rely on excluded middle quite a lot. For example, every set is empty or not; $y$ is in the range of $f$ or is not.
I am not the expert to remark on usage of excluded middle, so I will leave this to someone else.
A: Yes, it can be proved without using excluded middle, assuming by injective you mean: $(\forall x,y\in X) (f(x) = f(y) \rightarrow x = y)$.  (As opposed to the contrapositive condition $(\forall x, y \in X) (x \ne y \rightarrow f(x) \ne f(y))$ which is sometimes used as the definition in classical mathematics textbooks.)
To see this, suppose that $g : \mathcal{P}X \to X$ is injective in this sense.  Then define
$$ S_0 := \{ g(S) \mid g(S) \notin S, S \in \mathcal{P}X \}. $$
Or, if you prefer,
$$ S_0 := \{ x \in X \mid (\exists S \in \mathcal{P}X) (g(S) \notin S \wedge g(S) = x) \}. $$
We now consider whether $g(S_0) \in S_0$.  By definition, we have the equivalence
$$ g(S_0) \in S_0 \leftrightarrow (\exists S \in \mathcal{P} X) (g(S) \notin S \wedge g(S) = g(S_0)). $$
Now, applying the assumed injectivity of $g$, $g(S) = g(S_0)$ is equivalent to $S = S_0$, and by substitution, we then see that $g(S_0) \in S_0 \leftrightarrow g(S_0) \notin S_0$.
But it is intuitionistically valid that for any proposition $p$, $\lnot (p \leftrightarrow \lnot p)$; so the assumption that $g : \mathcal{P}X \to X$ implies a contradiction, and intuitionistically it's completely valid to conclude that $g : \mathcal{P}X \to X$ is not injective.  (The proof that $\lnot (p \leftrightarrow \lnot p)$: suppose that $p \leftrightarrow \lnot p$.  Then assuming $p$, we also have $\lnot p$ and therefore a contradiction; this shows that $\lnot p$.  But now, we also have $p$ and therefore we have a contradiction.)

It is, however, interesting to observe that Cantor's diagonalization argument shows that every function $f : X \to \mathcal{P} X$ is constructively non-surjective, in the sense that it constructs an element of $\mathcal{P} X$ which is not in the image of $f$.  On the other hand, I do not see a way to adapt the proof above to show that every function $g : \mathcal{P} X \to X$ is constructively non-injective, in the sense of showing that there exist $S_1, S_2 \in \mathcal{P} X$ such that $S_1 \ne S_2$ but $g(S_1) = g(S_2)$.
A: Suppose $f : {\cal P} X \rightarrowtail X$ is the injection. Consider the the following $g : X → {\cal P} X$
$$g(x) = \{y \in X : ∀s \in {\cal P}X . f(s) = x → y \in s\}$$
Then:
$$g(f(t)) = \{y \in X: ∀ s \in {\cal P}X. f(s) = f(t) → y \in s\}$$
$t$ is a candidate for $s$, and we know by injectivity of $f$ that $f(s) = f(t)$ means $s = t$. So, you can simplify:
$$g(f(t)) = \{y \in X: y \in t\} = t$$
If $x$ is not in the image of $f$, then $g(x)$ is actually all of $X$, so this specifies an analogous function to the one J.G. did in the comments, but using operations that should be valid in any topos (e.g. specifying the function by cases on whether $x$ is in the image of $f$ seems non-constructive). If you use a similar existential statement instead, you'll get an alternate function that assigns the empty set to $x$ not in the image of $f$.
Anyhow, $g$ is a surjection, because you can get every $t$ via $g(f(t))$. Now you can apply Cantor's diagonal argument to $g$.
What this did require was impredicativity (quantifying over ${\cal P}X$ to define a value of ${\cal P}X$). However, the idea of the "powerset" isn't exactly well defined without that.
A: Given any injection $f:\mathcal{P}X \to X$, define $g:X \to \mathcal{P}X$ where $g(x)=\{y \in X \mid \exists S \in \mathcal{P}X \, ((f(S)=x) \land (y \in S))\}$.
Then, for any $S \in \mathcal{P}X$, $g(f(S))=\{x \in X \mid \exists T \in \mathcal{P}X \, ((f(T)=f(S)) \land (x \in T))\}$. By injectivity of $f$, $f(T)=f(S)$ implies $T=S$, so $g(f(S))=S$. This implies that $g$ is surjective, which contradicts Cantor's theorem. S0, no such injection $f$ could exist even in intuitionistic mathematics.
