# Are there any non-constructive proofs for which an example was never constructed?

By non-constructive I mean the following:

A mathematical object is proven to exist yet it is not constructed in the proof.

Are there any examples of proofs like this where the mathematical object was never constructed? (by which i mean even after the existence of it was proven)

The game of Chomp is an example. A short and extremely simple strategy-stealing argument shows that no matter the size of the playing board, the first player always has a winning strategy; the complete argument is given in the Wikipedia article. But there is no general strategy known for an arbitrarily sized board.

• +1 for a proof that does not use AC, and for which, as far as we know, an example could be found (but so far hasn't been). – Ilmari Karonen Nov 21 '13 at 16:43
• No general strategy known $\neq$ it cannot be constructed. Chess, Go, and several other games have the same properties. Having finite number of moves they are certainly Borel and therefore determined. So there is a winning strategy (if we concede and say that the first player just wants not to lose the game, and will win in the event of a tie). But no such strategy is known so far. – Asaf Karagila Nov 22 '13 at 2:14
• @AsafKaragila: You probably already realize this, but for general explicitness: in Chomp, it's known that the first player has a winning strategy; in Chess, and in the general case of Go, it's known only that one of the two players has a winning strategy. (More about Go at http://math.stackexchange.com/q/229733/19345.) – ruakh Nov 22 '13 at 3:37
• @Asaf, what's your point? I never claimed that a winning strategy cannot be constructed and the original question clearly didn't ask for such an example, either. Even then, note that the claim is that a winning strategy for the first player exists on an arbitrarily sized board -- your comment that there are only finitely many moves is only relevant once you fix the board size. Of course a computer can find a winning strategy for a given board that's not too large, but that's beside the point. – Dan Petersen Nov 22 '13 at 7:31
• @Dan Thanks! That's exactly the kind of thing i was looking for! – Saal Hardali Nov 22 '13 at 8:56

There are many. In the proof that every vector space has a basis; in the proof that every ideal can be extended to a maximal ideal; in the proof that every filter can be extended to an ultrafilter.

All those use Zorn's lemma and in fact just show that such object exists. None of these proofs can construct the actual object in explicit details, because it is consistent that Zorn's lemma is false and these sort of objects may not exist sometimes (that is, some vector spaces won't have a basis, and so on). Generally speaking the axiom of choice (which is equivalent to Zorn's lemma) is responsible for a lot of the non-constructiveness of modern mathematics, as the axiom asserts the existence of certain objects which cannot be proved to exist otherwise.

If you want another semi-non constructive proof you can use the Cantor-Bernstein theorem for that. It's very easy to prove there is a bijection between $\Bbb{N^N}$ and $\mathcal P(\Bbb N)$ without constructing one, if you are using Cantor-Bernstein. While it is possible to actually construct such bijection, it's much easier to just prove it exists by other means.

In another direction one can argue, for example, that the proof that a continuous function from a closed and bounded interval to $\Bbb R$ must attain its minimum and maximum is non-constructive, because we don't actually construct the point, we just prove it exists.

• Maybe there's a problem with my question. What I'm trying to figure is whether it is possible to be able to prove an existence of an object yet not be able to provide an example of one. – Saal Hardali Nov 21 '13 at 10:56
• But the proof of CSB is constructive, and in principle following it with the injections at hand will give the desired bijection explicitly. That we are usually not interested in this is a different matter. – Lord_Farin Nov 21 '13 at 10:57
• @Lord_Farin: The proof is constructive, yes. But using it often gives you easy existence proofs without actually constructing the bijection. Moreover there are constructive mathematics context (not just $\sf ZF$) where the theorem fails, so it's not "really constructive". – Asaf Karagila Nov 21 '13 at 10:58
• @Shaul: Yes. It's possible. It's done most of the time in modern mathematics. – Asaf Karagila Nov 21 '13 at 10:59
• Ah... I just read about Zorn's lemma and it clicked. toda! – Saal Hardali Nov 21 '13 at 11:01

Classical examples of non-constructive proofs for where no explicit construction is possible naturally come from proofs that essentially use Zorn's Lemma. One such example would be the fact that any vector space has a basis. In particular, $\mathbb R$ is a vector space over $\mathbb Q$, and so there is a basis for $\mathbb R$ over $\mathbb Q$. Such a basis is called a Hamel basis. But, no such basis is given explicitly.

• Thannks Assaf ;;) – Ittay Weiss Nov 21 '13 at 10:54
• Sure thing Itay. :-) – Asaf Karagila Nov 21 '13 at 10:54
• Is it impossible to construct a Hamel basis, or is it an open problem? – Jack M Nov 21 '13 at 13:04
• @Jack: There are plenty of models where the axiom of choice fails and there is no Hamel basis for $\Bbb R$ over $\Bbb Q$. I've covered some of these in several answers on the site before (as well the topic itself). – Asaf Karagila Nov 21 '13 at 13:31

On the same line of thought but, imo, more striking, is the use of Zermelo's Theorem to prove there must exist a well-ordering of the reals (and thus, that golden dream of having a grip on that elusive first positive real number seems to be closer...).

Yet no such ordering on $\;\Bbb R\;$, as far as I am aware, is known. Of course, Zermelo's Theorem, Zorn's Lemma and The Axiom of Choice are all logically equivalent in ZFC.

• Everything [true] is equivalent to the axiom of choice in $\sf ZFC$... :-) – Asaf Karagila Nov 21 '13 at 11:11
• @Asaf: So $\mathrm{Con} ( \mathsf{ZFC} )$ is equivalent to Choice in $\mathsf{ZFC}$? – user642796 Nov 21 '13 at 11:17
• @Arthur: I meant everything true in $\sf ZFC$. You know that very damn well, too! In $\sf ZFC+\rm Con(\sf ZFC)$, however, $\sf AC$ and $\rm Con(\sf ZFC)$ are equivalent. – Asaf Karagila Nov 21 '13 at 11:21
• @AsafKaragila: What I think you mean is everything provable in ZFC. – Henning Makholm Nov 21 '13 at 13:35
• @Henning: Yes, but you know damn well that abuse of language between "provable from $T$" and "true in $T$". :-P – Asaf Karagila Nov 21 '13 at 13:36