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

1$\begingroup$ Which sort of "constructively" are you referring to? Errett Bishop's constructivism, for example, or just avoiding the use of the Axiom of Choice? $\endgroup$ – Robert Israel May 14 '12 at 16:06

1$\begingroup$ @Robert Israel: The former. $\endgroup$ – Ruud Koot May 14 '12 at 16:16
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 nonconstructive 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: HahnBanach, Brouwer fixedpoint, 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 nonconstant maps. Special versions of HahnBanach 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 sheaftheoretic 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.

12$\begingroup$ We may summarize, in the words of the Rolling Stones: You can't always get what you want, but if you try sometimes you might find you get what you need. $\endgroup$ – Gerry Myerson May 16 '12 at 5:33
I would assume that the HahnBanach theorem would have to be close to the top of any list.

4$\begingroup$ Bishopists might counter that in the cases they (and hence, by inference, all rightminded people) care about, one can do HahnBanach constructively. (I say this as someone who uses HB nonconstructively all the time.) $\endgroup$ – Yemon Choi May 14 '12 at 17:34

2$\begingroup$ Almost. There is a constructive HahnBanach, see blms.oxfordjournals.org/content/21/1/79.abstract and cs.math.ist.utl.pt/ftp/pub/CederquistJ/98CCNhahnbanach.pdf. $\endgroup$ – Andrej Bauer May 14 '12 at 21:08

$\begingroup$ @Andrej: Are these the same normed spaces as mentioned obliquely by @Yemon? $\endgroup$ – Igor Rivin May 15 '12 at 0:13

1$\begingroup$ Well, I can't read Yemon's mind, but I think so, yes. Ishihara's paper would certainly count as episcopal. (There is an ubounded potential for silly jokes based on the last name "Bishop".) $\endgroup$ – Andrej Bauer May 15 '12 at 8:54

1$\begingroup$ Are you sure the paper would not count as Erratic? Two can play at this game... $\endgroup$ – Igor Rivin May 15 '12 at 11:44
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}(nm+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 YuenKwok Chan in 1971:
Chan, Yuenkwok, 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}(nm)(nm+1)$.
I can imagine this being a real issue, because the function actually given to you might be $C^k$ only for $\text{max}(nm+1,1)\leq k< 2+\frac{1}{2}(nm)(nm+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.

2$\begingroup$ I'm confused  wouldn't replacing critical points by "almost critical points" make the statement stronger? Because then you'd be asserting that an even larger set still has measure 0. $\endgroup$ – Harry Altman May 16 '12 at 7:15

1$\begingroup$ The statement of the constructive version isn't that the set is of measure zero, but that it is "measure epsilon", thus the statement is not stronger. $\endgroup$ – Daniel Moskovich May 16 '12 at 8:38

$\begingroup$ As the link in the post contains
ezproxylogin1.ntu.edu.sg
, it probably does not work for other users. However, even after shortening to ams.org/mathscinet/search/… it does not work for me (without MathSciNet subscription). $\endgroup$ – Martin Sleziak Apr 19 '17 at 2:30 
1$\begingroup$ I guess that this link ams.org/mathscinetgetitem?mr=0276988 should work for both users with and without MathSciNet subscription. (The difference being that the subcribers are also shown the review.) I will also add projecteuclid link. $\endgroup$ – Martin Sleziak Apr 19 '17 at 2:30
The mean and pointwise ergodic theorems are nonconstructive, and I understand they were originally developed for applications to thermodynamics.

3$\begingroup$ Jeremy Avigad has recenty done some proofmining work which extracts constructive meaning from ergodic theorems, see andrew.cmu.edu/user/avigad/Papers/ergodic.pdf $\endgroup$ – Andrej Bauer May 14 '12 at 21:10

2$\begingroup$ Bishop gave a constructive interpretation as well, by giving an upcrossing proof similar to Doob's proof of martingale convergence. It is interesting because Bishop's result is still used to get numerical bounds on Ergodic convergence. (Also, the paper @Andrej cited of Avigad's was a summary of work Avigad did with Philipp Gerhardy, Ksenija Simic, and Henry Towsner. Some of it was based on Bishop's work. Many of the results are analogous to the martingale and differentiability results I mentioned in my answer.) $\endgroup$ – Jason Rute May 14 '12 at 21:37
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 nonconstructivity 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 HardyLittlewood maximal lemma controls the maximal amount of deviation from the limit.
The KnuthBendix 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

1$\begingroup$ I'm not sure Kruskal's tree theorem is nonconstructive. I recall seeing several approaches to constructive proofs, though the only one I can find quickly is Wim Veldman's "An intuitionistic proof of Kruskal's Theorem". $\endgroup$ – Henry Towsner May 14 '12 at 17:46

1$\begingroup$ Really? The proof I know relies on Dickson's lemma, en.wikipedia.org/wiki/Dickson's_lemma, which is nonconstructive. But as far as I remember, the lemma is needed only to show termination. So, if you believe in Markov Principle, as some constructivists do, then that would count as a constructive theorem. $\endgroup$ – Andrej Bauer May 14 '12 at 20:57

$\begingroup$ I was discussing Dickson's lemma with some colleagues last year. As far as I can tell, the statement becomes constructive if we weaken the statement to say that any nonempty subset is a contained in a union of finite many quarter planes. I don't know if this weaker version is sufficient for the KnuthBendix completion. ... BTW also any empty subset also works, so we can constructively prove that any empty or nonempty subset is contained in a union of finite many quarter planes. $\endgroup$ – Russell O'Connor May 22 '12 at 7:08
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 BanachTarski theorem. I guess that doesn't count as a real application, but it's surely nonconstructive and I can't resist mentioning it.
Well, the Brouwer Fixed Point Theorem comes to mind. An example of an application: http://physicsoffinance.blogspot.com/2011/09/brouwersfixedpointtheoremwhy.html

2$\begingroup$ The standard proof (using Sperner's lemma) is quite constructive, I think. $\endgroup$ – Igor Rivin May 14 '12 at 16:06

6$\begingroup$ Thanks, but Brouwer Fixed point theorem fails in the effective topos, therefore it cannot have a constructive proof. Of course, the approximate version is constructive. The link pointed to in the answer is not a serious application, it is just popular math. $\endgroup$ – Andrej Bauer May 14 '12 at 21:01

3

1$\begingroup$ This worries me: jstor.org/stable/2156239. I will look at full version when I get to my office (stupid paywall), there must be an assumption that is not stated on the first page. $\endgroup$ – Andrej Bauer May 15 '12 at 5:12

2$\begingroup$ The jstor paper referenced above is "constructive" in the sense that it is "explicit". The paper is written in classical logic, it seems. $\endgroup$ – Andrej Bauer May 15 '12 at 8:57