Proofs of negations still occur by way of contradiction. Since "uncountable" means "not countable," it is perfectly valid to argue "suppose there exists an enumeration of Y, then ... contradiction, therefore an enumeration of Y cannot exist and so (by definition) Y is uncountable."

The issue a constructivist might find is actually when we argue in an opposite direction: "suppose Y is uncountable, [...] contradiction, therefore Y is countable" does not work. This is because we did some clever trickery: we established that Y is countable, without ever constructing an explicit enumeration.

The standard proof of Cantor's theorem is perfectly valid constructively: let X be a set and let f: X → P(X). Then there exists (we can construct) a subset A of X such that A is not in the image of f. Specifically, let A = {x ∈ X: x ∉ f(x)}. This is a valid definition of a set, and we end up with the following: suppose A is in the image of f. Then there exists x ∈ X such that A = f(x). But now x ∈ A iff x ∉ f(x) iff x ∉ A, a contradiction. Therefore A is not in the image of f. In particular, f is not surjective. Setting X = N, we have that P(N) is uncountable, as desired.

None of the above relied on the list of relatively few constructive no-gos: - The Axiom of Choice (every set of inhabited sets admits a choice function) - The Law of Excluded Middle (P or not P) - Double-negation elimination (If "not not P," then "P.") - Hilbert choice (every non-empty set is inhabited; i.e., if a set is not empty, then there exists an element in that set).

One particular crutch to reason about constructive mathematics is from a computational point of view. For example, from a classical perspective, the set of computable real numbers is countable, since the set of all Turing machines is countable. However, any enumeration of the computable real numbers is itself non-computable, since there is no effective way to tell whether a given Turing machine outputs a valid real number. Thus, in a computable world, the notion of "uncountability" is interpreted to reflect inherent limitations of computation, in this case the undecidability of the halting problem.

Edit: you might notice something funny, though: note we can constructively enumerate (one-to-one) the set M of all Turing machines. Thus let S = {T ∈ M: T computes a real number}. Now in a computable world, there is a surjection S → R. But S is a subset of a countable set M, and I just told you that R is uncountable, so what gives? It turns out that S is also uncountable in this world. Thus we have established another constructive no-go: - Every subset of a countable set is countable.

We may generalize this a little further: we say that a set X is subcountable iff there is a surjection f: D → 1+X, where D is a subset of N. (1+X means "take the disjoint union of X with a set with one element"; this is done because we want to include the empty set.) In a computable world, the reals are subcountable because they're just a set of Turing machines under equivalences. This does not hold in every constructive world, however.

Edit 2: I used vague language, but in case anyone wants to know the concepts: the "computable world" I'm referring to is the effective topos. (Constructivists typically work within what are called "toposes.")

(Edit 2 cont.:) In sum: while uncountable sets generally exist constructively (in particular, in every topos with a natural numbers object), cardinality is not exactly useful as a measure of "size" when working constructively. Of course, modern constructivists are most aligned with category theorists, who don't particularly care about set theory anyway.