I read that Cantor's Theorem can be proven in type theory (although I haven't found/understood such a proof). My understanding however is that type theory can be impredicative and as such that wouldn't help me very much.
I have the impression that the proof I've seen on Wikipedia of Cantor's Theorem is impredicative. If it isn't enlighten me as I clearly then do not understand it. If it is, then my question stands.
Regards.
On
EDIT: I just now noticed that the OP never said which of Cantor's theorems under scrutiny! Below I assume that it's the uncountability of the reals.
Tl;dr: The proof of Cantor's theorem is completely predicative.
Predicativity is of course a somewhat informal notion, but ultimately it's about the perceived dangers of self reference. Self-reference here is construed broadly: a definition of an object $\alpha$ is impredicative if it involves quantifying over a set containing $\alpha$. For instance, the usual example is that the existence of least upper bounds of nonempty bounded sets of reals is impredicative: this is because the definition of "$\alpha$ is the l.u.b. of $A$" is
$\alpha$ is an upper bound of $A$, and for all upper bounds $\beta$ of $A$ we have $\alpha\le\beta$.
The bolded quantification over upper bounds is a quantification over a set which contains $\alpha$, so is impredicative.
So your question amounts to: what kind of quantification is used in Cantor's argument?
Let's take the following version of Cantor's theorem for simplicity:
If $F$ is a function from $\mathbb{N}$ to the set of infinite sequences of $0$s and $1$s, then there is some infinite sequence of $0$s and $1$s not in the range of $F$.
(Note that infinite sequences of $0$s and $1$s do not quite correspond exactly to real numbers in $[0,1]$: this is because a single real need not have a unique binary expansion. This is a minor point, but it does mean that things are a bit easier to visualize when working with sequences instead of with reals, at least at first.)
The proof goes as follows:
Let $g_F$ be the sequence ${\color{red}{\mbox{defined by}}}$: the $n$th bit of $g_F$ is $0$ iff the $n$th bit of $F(n)$ is $1$, and the $n$th bit of $g_F$ is $1$ iff the $n$th bit of $F(n)$ is $0$. ${\color{red}{\mbox{Then}}}$ $g_F\not\in ran(F)$, since for each $n$ we have $F(n)(n)\not=g_F(n)$.
There are two pieces to this proof, which I've highlighted in red. In order of increasing relevance, they are:
The verification that $g_F\not\in ran(F)$. This is as simple as it gets, and is in fact even intuitionistically valid; but we don't even need to observe this, since predicative logic is fine with the excluded middle ...
... it's the construction of $g_F$ we care about. But there's nothing impredicative here: to define $g_F$ we didn't quantify over all functions, we just needed to look at the specific functional $F$ and its range $ran(F)$. At no point in the definition of $g_F$ did we quantify over any set containing $g_F$.
(Incidentally, the definition of the functional $\mathcal{G}$ sending $F$ to $g_F$ is also fully predicative: while it involves quantifying over all maps from $\mathbb{N}$ to infinite binary sequences, it itself is not such a map.)
Cantor's proof that there is no bijection between a set $X$ and its powerset $\Bbb{P}(X)$ goes like this: if $f : X \to \Bbb{P}(X)$ is any function, then $\{x \in X \mid x \notin f(x)\}$ is a member of $\Bbb{P}(X)$ that is not in the range of $f$. This is a constructive argument: you give me an $f$ and I give you something that is not in its range. This doesn't require any impredicative reasoning.