Can the nonexistence of a constructive proof be proven when an existential proof exists?

Question

Proofs are usually constructive or existential. For example, we know there are an infinite number of primes, and therefore the centillionth prime exists. We don't know what it is, though we can make bounds on its location.

Are there any existential proofs where it has been proven that there is NOT a constructive proof of the same fact?

Answer 1

Certainly, there are many such situations. For example, given a continuous function $f$ on $[0,1]$, it is known that a maximum of $f$ "exists". However, the proof relies essentially on an argument by contradiction, whose key ingredient is the law of excluded middle. It can be shown that such a maximum could never be constructed without reliance on the latter. See e.g., Constructivism in Mathematics. By A.S. Troelstra, D. van Dalen (http://www.google.co.il/books?id=-tc2qp0-2bsC&source=gbs_navlinks_s) Thus, in an intuitionistic framework, one cannot rule out the existence of a real $a$ such that it cannot be shown that $(a\leq 0)\vee (a\geq 0)$. Now consider the function $f(x)=ax$. If we could find a maximum of $f$, we could also pin down the sign of $a$, which is impossible as per above.

This type of construction is known as a Brouwerian counterexample in the literature. Of course, the first theorem "refuted" in this fashion is... Brouwer's fixed point theorem :-)

The counterexample above is discussed in Troelstra-van Dalen on page 295 which unfortunately is missing from the online version.

Answer 2

In the strictest sense it is impossible to prove "there is not a constructive proof of $S$", because there is no formal notion of "constructive proof". There are many different forms of constructivism, and they do not agree on whether various principles are constructively valid (e.g. forms of Markov's principle are accepted by some branches of constructivism and not by others). Moreover, there has been an historical trend where many constructivists avoid formalization altogether.

There are, however, formal systems that model constructive reasoning. It is certainly possible to show that particular theorems cannot be proved in these formal systems. For example, it is often possible to show in a constructive system $T$ that a particular statement $S$ implies the law of the excluded middle, or some other omniscience principle. Because these principles are generally not accepted in constructivism, we interpret this as saying that $S$ is not provable constructively. But really all that we have shown is that $S$ is not provable in $T$; there could well be some other system that someone calls constructive which is able to prove $S$.

For commonly studied systems of constructivism, there are many classical results that are known to be unprovable. user72694 mentioned the principle "every continuous function $[0,1] \to \mathbb{R}$ has a maximum" (when we do not assume the function is uniformly continuous). Others include:

• "Every strictly increasing bounded sequence of rational numbers converges"
• "Every finite square matrix of complex numbers can be put into Jordan form over $\mathbb{C}$"
• "Every ideal in a countable partial order extends to a maximal ideal

Here is an example to illustrate the importance of paying attention to the system. Bishop did prove "Every continuous function $[0,1] \to \mathbb{R}$ has a supremum" in his book on constructive analysis. He was able to do this because, in his system, a continuous function is defined to be uniformly continuous, and that additional information allows for a constructive proof.