Constructive proof for existence of uncountable sets?

Question

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.

Answer 1

Your question "Can I show the existence of an infinite set with no bijection to N N without using proof by contradiction?" is ill-posed because it does not clarify the nature of "existence" you have in mind. This is the gist of constructivist objections to classical mathematics as formulated for instance by Errett Bishop. What you can retain from Cantor's diagonal argument is the following: if you have a map from the natural numbers to the reals then it won't be surjective. This is proved without using the law of excluded middle and in fact this is proved in Bishop's book.

Answer 2

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:

1. Constructive math.
2. 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.