9
$\begingroup$

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?

  • 0
    @Mariano, I think you are confusing [constructible](http://en.wikipedia.org/wiki/Constructible_universe) with [constructive](http://en.wikipedia.org/wiki/Constructivism_%$2$8mathematics%29) (also see [SEP](http://plato.stanford.edu/entries/mathematics-constructive/)).2011-11-12

4 Answers 4

8

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.

  • 0
    Gerry, one last comment (sorry for this extended monologue). You are perhaps thinking of superficially similar cardinality arguments to establish the existence of transcendental or noncomputable real numbers. But these arguments are critically different because the notions of algebraicity and computability are formalizable via formulas in set theory. The notion of "nameability" isn't, else you would quickly run into self-referential paradoxes: "let $\alpha$ be the least ordinal which isn't nameable."2011-10-18
7

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.

  • 2
    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.2011-10-18
2

There are various flavors of constructive mathematics. Depending on what you mean exactly there might be different answers. But more importantly you would like to find a statement that makes sense from constructive view-point (and has the same sense from classical viewpoint) that is provable classically but not constructively. For example, if you think about real numbers, you cannot simply talk about arbitrary subsets of real numbers since the are not well-defined constructively. In fact you cannot talk about the set of real numbers as an object like we do in classical mathematics. Moreover different definitions of real numbers are not constructively equivalent.

The example given by Gerry is not true constructively simple because they don't believe in existence of those numbers. Similar problems are involved in lhf's answer.

The simplest example that one can give of a statement that cannot be proven constructively is the principle of excluded middle for arbitrary complex formulas.

0

Two canonical examples: the axiom of choice and the law of excluded middle are both assertions that are provable in a classical setting, but they aren't provable constructively.