# 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 standard example is the Intermediate Value Theorem, with $P(x)$ being "$f(x)=0$". But that one is not "weird"... Banach-Tarski is a pretty weird example. –  Arturo Magidin Feb 15 '12 at 18:21
@ArturoMagidin, the IVT has a constructive version based on nested intervals. –  lhf Feb 15 '12 at 18:22
related to math.stackexchange.com/questions/73400/… –  lhf Feb 15 '12 at 18:23
@lhf: The IVT ultimately relies on the supremum property; the proofs of which that I can think of right now are all by contradiction and non-constructive –  Arturo Magidin Feb 15 '12 at 18:24
@ArturoMagidin, I meant the bisection algorithm. Of course, the nested-interval property is equivalent to the existence of supremum and so in this sense is non-constructive. The IVT is also equivalent to both. –  lhf Feb 15 '12 at 18:25

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.

-
More generally, every two-player game of perfect information in which every play is finite and there are no ties has a winning strategy for one player or the other, by the Gale/Stewart theorem. E.g. if we declare that white wins any draw, then chess has this property and we have no idea which player has the winning strategy. –  Carl Mummert Feb 16 '12 at 0:46
I think you mean that no efficient winning strategy for A is known? –  Dan Brumleve Feb 16 '12 at 4:57
@Dan Brumleve: Yes, I was using the "no known" perhaps too casually, for any board one can try everything. –  André Nicolas Feb 16 '12 at 5:04
Actually today one student told me a strategy that works for square bars (like $19\times 19$): Let's say the squares are numbered, the poisoned being (1,1). A picks $(2,2)$ as his first move. Now at each move B can only pick $(1,k)$ or $(k,1)$, and A just responds by reflecting the move, picking $(k,1)$ or $(1,k)$. It's easy to see that B is forced to take the last square. On a non-square board this strategy would fail - if A picked $(2,2)$, B would just pick the necessary squares to make the board diagonally symmetric and subsequently win the game. –  Petr Pudlák Oct 29 '12 at 18:21

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.

-
There are plenty of constructive systems, such as Martin-Lof type theory, which include the axiom of choice. It is only nonconstructive when combined with various other principles of classical mathematics, such as the law of the excluded middle. –  Carl Mummert Feb 15 '12 at 22:43
The axiom of choice with extensionality implies the law of the excluded middle. Constructive type theory admits choice by not having extensionality; As soon as the law of the excluded middle is a consequence, existence proofs are possible and the system is no longer constructive. –  dezakin Oct 8 '13 at 6:40

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

-

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.

-
This was actually resolved quite a while ago by Gelfond-Schneider: en.wikipedia.org/wiki/Gelfond%E2%80%93Schneider_theorem . –  Steven Stadnicki Feb 15 '12 at 19:43

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.

-
It is equivalent to at least one player winning eventually, it has nothing to do with strategy. But we do know that the first player can always win in Hex. –  Michael Greinecker Feb 16 '12 at 1:31
@MichaelGreinecker Perhaps Wikipedia is wrong on this one then, but it says "John Nash proved in 1952 that a game of Hex cannot end in a tie, and that for a symmetric board there exists a winning strategy for the player who makes the first move (by the strategy-stealing argument). However, the argument is non-constructive : it only shows the existence of a winning strategy, without describing it explicitly. Finding an explicit strategy has been the main subject of research since then." –  Ragib Zaman Feb 16 '12 at 3:45
That is true, but the relation between Hex and the (two-dimensional) Brouwer fixed point theorem is due to David Gale. Nash's "stealing strategy"-argument is however a nice example of a nonconstructive proof. –  Michael Greinecker Feb 16 '12 at 9:22
@MichaelGreinecker I understand now, I was grouping two distinct results together. Thanks. –  Ragib Zaman Feb 16 '12 at 11:55

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.

-
@CarlMummert: You may be thinking of a different result; this one is pretty easy to prove. My favorite proof is probabilistic. Fix a base $b$. Since the base-$b$ digits of a $U(0,1)$ random variable $U$ are iid uniform on $\{0, 1, \dots, b-1\}$, the strong law of large numbers gives that $U$ is normal in base $b$, almost surely. Taking a countable intersection, $U$ is normal in every base, almost surely. Or in other words, Lebesgue-almost-every $x \in [0,1]$ is normal in every base. –  Nate Eldredge Feb 15 '12 at 23:55
@Nate Eldredge: the question I had asked about in a deleted comment was about the Champernowne number .123456789101112... which is known to be normal in base 10, but AFAIK not known to be normal in other bases. –  Carl Mummert Feb 16 '12 at 0:39