# Are there “essentially non-constructive” statements?

There exist constructive and non-constructive proofs.

Sometimes, for a mathematical statement, we can have both non-constructive and a constructive proof.

However, are there statements for which there is only a non-constructive proof? (The fact that there maybe a construction of the required object but we don't know it yet doesn't count here).

Phrased differently, are there statements (that claim existence of objects) that are essentially non-constructive?

-
How about anything that we know cannot be proved in ZF, that is, requires some version of the Axiom of Choice, possibly weaker than full AC? Then there is a huge number of statements, important in standard mathematics, that only have a non-constructive proof. Hahn-Banach, existence of a non-principal ultrafilter on $\mathbb{N}$, existence of a basis for a general vector space, and so on and so on. –  André Nicolas Oct 17 '11 at 18:11
Could anyone give a simpler example? Moreover, what ensures that there does not exist a constructive proof for a statement? –  wu9 Oct 17 '11 at 18:58
To ensure that there is no "constructive proof", one usually constructs a model of ZF in which the statement is not true. You have not told us what is your background, so it is very difficult to know what you consider simple! –  Mariano Suárez-Alvarez Oct 17 '11 at 19:12
@Mariano, I think you are confusing constructible with constructive (also see SEP). –  Kaveh Nov 12 '11 at 17:47

There exist real numbers that don't have names. You can prove this, but you can't construct such a real number, because by the very act of constructing it, you would be giving it a name.

-
If you look at constructive set theory you could probably construct the real numbers out of them. You don't really need the law of excluded middle to get to the statement you just said i.e. not all real numbers are describable. –  simplicity Oct 17 '11 at 22:37
This is just a disguised version of computable numbers, isn't it? –  lhf Oct 17 '11 at 22:39
Actually, the set of computable numbers isn't the same as the set of nameable numbers. For example chaitin constant isn't computable, but you can define i.e. name it. –  simplicity Oct 17 '11 at 23:06
I actually don't think you can prove this, but I suppose it depends upon what you mean by "nameable." If a real is nameable if, say, it uniquely satisfies some formula in the language of set theory, then it is consistent that every real number is nameable. –  user83827 Oct 18 '11 at 1:36
@ccc, I'm not sure if you are responding to me or to simplicity. In any event, "names" are finite strings of symbols from a finite alphabet and are thus countably infinite, whereas reals are an uncountable infinity, hence, there are reals without names. –  Gerry Myerson Oct 18 '11 at 2:34

The existence of a basis for $\mathbb R$ as a vector space over $\mathbb Q$ is a consequence of the axiom of choice but it has no constructive proof.

-
Can you point somewhere that proves it has no construction? –  Henrique Tyrrell Oct 17 '11 at 20:12
@Henrique, sorry I don't have a reference, except for the fact that such a basis is uncountable and the set of constructive numbers is countable. See for instance math.stackexchange.com/questions/58036/…. –  lhf Oct 17 '11 at 20:17
@Henrique Tyrrell: The existence of a basis for an arbitrary vector space implies the axiom of choice, but I believe not much is known (in the sense of what version of the axiom must follow) in the specific case of the reals over the rational number field. See the following: math.lsa.umich.edu/~ablass/bases-AC.pdf and mathoverflow.net/questions/68950 and mathoverflow.net/questions/46063 –  Dave L. Renfro Oct 17 '11 at 20:40
A basis for the reals over the rationals creates a set without the property of Baire, so you need strictly more than Dependent Choice to prove its existence. Pinning it down exactly might require a bit more work, but it definitely requires an uncountable choice principle. –  user83827 Oct 18 '11 at 1:38