# 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.

• Hilbert's hotel (en.wikipedia.org/wiki/Hilbert%27s_paradox_of_the_Grand_Hotel) explains this quite well. This problem is also featured in the book "The Joy of X" by Steven Strogatz. – Toby Mak May 8 '17 at 12:36
• Do you distinguish between "not uncountable" and "countable"? Otherwise it sounds strange that you want to prove the former without knowing the latter. Are you explicitly working in a logic where $\neg\neg P$ and $P$ are different? – hmakholm left over Monica May 8 '17 at 12:36
• @HenningMakholm At least I will not allow me the conclusion "if $\neg\neg P$, then $P$". Is this what you are asking for? – M. Winter May 8 '17 at 12:39
• @M.Winter: But what it sounds like here is that for some reason you want to avoid "Such-and-such, therefore $P$ and hence $\neg\neg P$" (where $P$ is the existence of a bijection $\mathbb N\leftrightarrow \mathbb Q$). But $P\vdash \neg\neg P$ is valid even intuitionistically! – hmakholm left over Monica May 8 '17 at 12:41
• @HenningMakholm Where do you read from that $P\vdash\neg\neg P$ is eventually valid for me? – M. Winter May 8 '17 at 13:01

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.

• Is the assumption that the map is injective actually used? It is at least not necessary in classical logic. – hmakholm left over Monica May 8 '17 at 12:44
• Good point. I was just being the typical classical mathematician :-) @HenningMakholm – Mikhail Katz May 8 '17 at 12:45
• With existence I mean that there is a provable sentence $(\exists X) [X \text{ infinite}\wedge\neg(\exists f) [f \text{ is bijection between$X$and$\Bbb N$}]]$. – M. Winter May 8 '17 at 13:05
• @M.Winter, the problem is the interpretation of quantifiers. I know it may sound odd to claim that the meaning of the existence quantifier is ambiguous. However, this is precisely the content of Brouwer's challenge to classical mathematics. – Mikhail Katz May 8 '17 at 13:07

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.

• This is not what "proof by contradiction" means. In virtually every constructive framework, you prove the non-existence of something by assuming it exists and deriving a contradiction. That's literally what $\neg \exists x.P(x)$ means, i.e. $\neg Q \equiv Q\Rightarrow\bot$. See this article by Andrej Bauer. – Derek Elkins left SE May 15 '17 at 9:37
• @DerekElkins Very interesting. I know that there is a difference between $\varphi \Rightarrow \neg\neg\varphi$ and $\neg\neg\varphi\Rightarrow\varphi$, but I have not known that there is different terminology for it, though it seems natural to me why most mathematicians think both of it is by contradiction. But this makes clearer to me, what constructivism is about. I will try to fix it, hopefully in the right way. – M. Winter May 15 '17 at 11:11