Examples of non-constructive results I'm giving a talk on constructive mathematics, and I'd like some snappy examples of weird things that happen in non-constructive math.  
For example, it would be great if there were some theorem claiming $\neg \forall x. \neg P(x)$, where no $x$ satisfying $P(x)$ were known or knowable.
But other examples are welcome as well.
 A: The existence of a Hamel Basis, that is, a basis for $\mathbb R$ as a vector space over $\mathbb Q$. No one knows a Hamel basis; it's probably unknowable in some sense.
The existence of a basis for every vector space is equivalent to the axiom of choice, which is the non-constructive piece of math by excellence.
A: If $\Phi$ is any statement, the following is a consequence of the law of the excluded middie:
$$
(\exists n \in \mathbb{N})[(n = 0 \land \Phi) \lor (n \not = 0 \land \lnot \Phi)]
$$
It will only be provable constructively if either $\Phi$ or $\lnot \Phi$ is provable constructively, because to prove it constructively you would have to produce an actual value of $n$, which means you would have to decide $\Phi$. 
A: At least some time ago (I'm not sure if this has been cleared up recently), it was not known which of the quantities $\sqrt 2^\sqrt 2$ and  $(\sqrt 2^\sqrt 2)^\sqrt 2$ furnishes an example of an irrational number raised to an irrational power that is rational. 
A: Brouwer's fixed point theorem in 2 dimensions is equivalent the fact that the game of Hex has a winning strategy but no one knows what that strategy is. 
A: At a fun level, there is the two-player game of Chomp.
Briefly, you have an $m\times n$ chocolate bar, divided into squares as usual. The lower left-hand little square is poisoned. The two players, A and B, play alternately. At any move, a player picks the lower left-hand corner of a square, and eats all squares above and/or to the right of that corner. The objective is not to eat the poisoned square.
One can prove quite simply that A has a winning strategy for any chocolate bar except the $1\times1$. But the proof is indirect. It is clear that for any specific bar, one of the two players has a winning strategy. One then shows that if B had a winning strategy, then A could adapt that strategy and win, by taking the square in the upper right-hand corner.  
However, for even modest-sized chocolate bars, say $19\times 19$, no winning strategy for A is known. I may be out of date on the $19$, but know that computer searches for strategies have not had great success.
A: It has been shown that almost all real numbers are normal in all bases (ref?), but I don't think that anyone has ever exhibited such a number. 
