Constructive proof for existence of uncountable sets? I stumbled upon this question by trying to prove that the rationals $\Bbb Q$ are not uncountable, but not by using the knowledge that they are already provably countable. I think I forbid myself using a proof by contradiction. But then, can I even show that the reals are uncountable in a construcive way. In the end, any kind of diagonal argument is using proof by contradiction, right? So in more general terms:

Can I show the existence of an infinite set with no bijection to $\Bbb N$ without using proof by contradiction?

I found this, and read from it that this seems to be a hard and still studied question for the reals. But I ask this in more general terms.

I want to answer my question with the knowledge I obtained from the other answers and my later research.

First, I unintentionally used two terms interchangeably which are not the same:


*

*Constructive math.

*Not using proof by contradiction.


While constructive math does not allow showing the existence of individuals by using proofs by contradiction, but insists in constructing a witness explictely, some branches of constructivism do indeed allow showing the non-existence of individuals by assuming their existence and deriving a contradiction (proof of negation). So in this terms, there is no problem using the diagonal argument here:

Let $X$ me any countable set, which I assume exists. Then $\mathcal P(X)$, its powerset, is uncountable. This can be shown by assuming the existence of a bijections $f:X\leftrightarrow\mathcal P(X)$ and deriving a contradiction in the usual way.

The construction of $\mathcal P(X)$ is explicit and, well, constructive. The contradiction is only used to show the non-existence of a bijection $f$.
In this sense, I have answered the question in the title.
