Confusion about Cantor's theorem Let $P_0, P_1, P_2, ...$ be an enumeration of all one-variable predicates, and let $f(n) = \{m \in \mathbb{N} \mid P_n(m)\}$. This $f$ isn't surjective since it misses $X = \{m \in \mathbb{N} \mid m \not\in f(m)\}$. But isn't "$m \not\in f(m)$" one of the predicates in the enumeration!?
 A: If your proof seems correct, but contradicts something known (and especially as simple) as Cantor's theorem, it's time to look at your assumptions.
You assume that there is an enumeration of all predicates. So maybe that's the problem? Maybe you've just proved that there isn't any enumeration of all predicates. Or maybe the conclusion is false, and simply $\{m\notin f(m)\mid m\in\Bbb N\}$ is not a predicate.
Now. The question is what exactly do you mean by "predicate". If you meant just subsets of $\Bbb N$, well, then there are a lot more subsets. So of course there is no enumeration. But if you mean "predicate" in the sense of a second-order logic kind of object, then we generally have from this that $\{m\notin f(m)\mid m\in\Bbb N\}$ is not a predicate, or that $f$ was not a predicate to begin with.
In other words, to be able and define a predicate from $f$, you have an implicit assumption that $f$ itself is a definable relation, and that the numeration is somehow definable. In general neither of them is definable, neither is a predicate.
A: I think there's two main misunderstandings.
The first problem is that I'm mixing up the difference between a string of characters which represents a valid formula, and the formula itself. So we do have an enumeration $P_0, P_1, ...$ of strings representing formula, but it doesn't make sense to say $\{m \in \mathbb{N} \mid P_n(m)\}$, because "$P_n(m)$" is just a meaningless string, not a formula.
What would make sense, is saying either:

*

*$\{m \in \mathbb{N} \mid \ulcorner P_n \urcorner(m)\}$, where $\ulcorner F \urcorner$ refers to the actual logical formula encoded by the string $F$. And this solves the problem since this "$\ulcorner F \urcorner$" is something from outside the logic, so it isn't covered by the enumeration.


*$\{m \in \mathbb{N} \mid \text{there's a proof of } P_n(m)\}$, where "proof" is an object listing the sequence of logical manipulations giving the string "$P_n$".
This is where the second problem comes up. The first-order formula expressing "there's a proof of $P_n(m)$" is NOT equivalent to $\ulcorner P_n \urcorner(m)$ itself, because of something called the incompleteness theorem! More precisely, $m \not\in f(m)$ says "there is no proof of $P_m(m)$", which is not equivalent to "there is a proof of $\lnot P_m(m)$".
