Question

What are good/interesting examples of theorems than can be proven classically, but not constructively, and have applications in e.g. physics?

Answer 1

In general it is very difficult to be sure that a theorem cannot be constructivised in some form that preserves its applicability. As you will notice most of the answers offered have comments attesting this fact.

One reason for this is that many non-constructive theorems in analysis become constructive when they are relaxed a little bit. A typical example is the mean value theorem. It does not hold constructively as usually stated, but it its $\epsilon$ version does: if $f$ is continuous and $f(0) < 0 < f(1)$ then for every $\epsilon > 0$ there is $x \in [0,1]$ such that $|f(x)| < \epsilon$. Many other theorems can be relaxed in this way: Hahn-Banach, Brouwer fixed-point, etc. Moreover, such relaxed versions often make more sense in applications than their exact versions, for example because we need to take into account noise, errors, or bounded numerical precision.

Another reason is that for applications we typically do not need a theorem in its full generality because we have extra information, which allows for a specialized constructive version. For example, while the general mean value theorem fails constructively, it holds for locally non-constant maps. Special versions of Hahn-Banach holds constructively, and they will typically suffice in concrete situations.

There is a third reason why it is difficult to find classical theorems with applications that cannot be constructivized. Most applications belong to the fields of physics and computer science, which are both very naturally constructive. Physics is constructive by its very nature because "everything is continuous" in the real world, while in computer science "everything is computable". These are two main motivations for intuitionistic mathematics (namely Brouwerian continuity principles or sheaf-theoretic models, and computable interpretations of intuitionistic mathematics).

Lastly, there remains the simple fact that one has to perform an exhaustive literature search to be sure that a theorem has not been constructivized. A lot more has been constructivized than one would think, and the only obstacle seems to be lack of man power.

Answer 2

A famous Martin Gardner mathematical games column had a number of April Fool items, one of which was about a guy getting rich by duplicating gold spheres using the Banach-Tarski theorem. I guess that doesn't count as a real application, but it's surely nonconstructive and I can't resist mentioning it.

Answer 3

Sard's Theorem, which is foundational, may be an example of a theorem of the sort you are looking for when the differentiability class of the function is low. Let's recall its classical statement:

Sard's Theorem: Let $f\colon\, \mathbb{R}^n\to\mathbb{R}^m$ be a $k$ times continuously differentiable function, where $k\geq \text{max}(n-m+1,1)$. Let $X$ be the critical set of $f$. Then $f(X)$ has Lebesgue measure $0$ in $\mathbb{R}^m$.

A constructivist version was proven by Yuen-Kwok Chan in 1971:

Chan, Yuen-kwok, A constructive proof of Sard's theorem. Pacific J. Math. 36, 291–301 (1971; MR0276988).

The constructivist version relaxes the statement of Sard's theorem in a benign way ("critical points" are replaced by "almost critical points") and in at least one less benign way:

The function $f$ is taken to be a $k$ times continuously differentiable function, where $k\geq 2+\frac{1}{2}(n-m)(n-m+1)$.

I can imagine this being a real issue, because the function actually given to you might be $C^k$ only for $\text{max}(n-m+1,1)\leq k< 2+\frac{1}{2}(n-m)(n-m+1)$. John Milnor on Mathematical Reviews asks whether the bound on $k$ can be tightened, and so does the author at the end of the paper. If not, then Sard's Theorem for small $k$ seems to me to be a genuinely important result which can be proved classically, but not constructively.

Answer 4

One of the simplest is the monotone convergence principle, that every bounded increasing sequence of rationals is convergent.

Along with Henry Towsner's example of the Ergodic theorem there is Doob's martingale convergence theorem and Lebesgue's theorem that every function of bounded variation is differentiable a.e.

However, if more information is known then this non-constructivity can be overcome. For example, with a martingale, if the limit is computable in the $L^1$ norm and the $L^1$-bound is computable, then the rate of convergence is computable (both convergence in measure and a.e. convergence). (I assume the proof is constructive, but I haven't worked that out. However, computable rates of convergence are one of the most important consequences of constructive proofs.)

Similarly, the Lebesgue differentiation theorem has computable rates of convergence ($L^1$ convergence and a.e. convergence) since the limit is known (it is the function itself) and the Hardy-Littlewood maximal lemma controls the maximal amount of deviation from the limit.

Answer 5

The Knuth-Bendix completion algorithm is used in computer algebra. Its proof of correctness relies on Kruskal's tree theorem, if I understand correctly. The proof of Kruskal's tree theorem is very nonconstructive: http://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem

Answer 6

I would assume that the Hahn-Banach theorem would have to be close to the top of any list.

Answer 7

The mean and pointwise ergodic theorems are non-constructive, and I understand they were originally developed for applications to thermodynamics.

Answer 8

Well, the Brouwer Fixed Point Theorem comes to mind. An example of an application: http://physicsoffinance.blogspot.com/2011/09/brouwers-fixed-point-theoremwhy.html