# Is there any result that has applications that can't be proved in constructive mathematics?

Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “ we can construct”.

Is there any result in classical mathematics that is extensively used in applications (engineering, physics, etc.) but that can't be proved constructively?

• No, because in real life everything is finite as everything is a subset of the set of all (finitely many) atoms. May 6, 2018 at 10:32
• I feel amused by the thought that constructive mathematicians may not care much about applications in real life :D
– SK19
May 6, 2018 at 11:04
• @StefanH We don't really know the nature of the cosmos, we just have some models that turn out to predict events correctly to a certain degree most of the time. And a lot of discrete can be approximated by continuous. Best example: en.wikipedia.org/wiki/Central_limit_theorem
– SK19
May 6, 2018 at 11:08
• @SK19, very pertinent remark. In my experience, constructive mathematicians seem to care more about having mathematical objects exist to their ontological satisfaction, than about their applicability "in real life". May 6, 2018 at 11:08
• @StefanH More importantly, we can only measure things to a finite degree of precision. "Matter is made of atoms" is not really a satisfying justification for a belief that the universe is discrete (isn't the space between atoms continuous? More importantly, is the question even meaningful?), but what we can say without getting lost in metaphysics is that we can only measure things to a finite number of decimal places. May 6, 2018 at 12:07

The Intermediate value theorem comes to mind.

If $f$ is continuous on a closed interval $[a,b]$, and $c$ is any number between $f(a)$ and $f(b)$ inclusive, then there is at least one number $x$ in the closed interval such that $f(x)=c$.

While it looks very theoretically in nature, it is the foundation for a lot of real analysis. It is important for numerical proofs, and in turn numerical mathematics is important for e.g. Computer Tomography.

• But we have a reasonable substitute for it; see Bishop & Bridges, page 40. May 6, 2018 at 11:24
• @MauroALLEGRANZA, such "substitutes" often beg the question as they are often not applicable in "real-life" situations in physics; see this answer. May 6, 2018 at 15:46
• The intermediate value theorem is for all practical purposes proved by the extremely constructive bisection method. Granted, you'll only get an approximate result, but that's all that matters in physics anyway. May 6, 2018 at 21:19
• @leftaroundabout: you may know this already, but the problem with the bisection method in constructive analysis is that we cannot in general assert the trichotomy principle that a given real $x$ has $x > 0 \lor x = 0 \lor x < 0$, and so the proof relies on a non-constructive decision about whether a root has already been found at each step. The proof works fine for floating-point numbers where we do have an effective trichotomy principle. May 6, 2018 at 21:45
• I would be interested to see a result in numerical analysis that uses the intermediate value theorem but doesn't follow from the approximate intermediate value theorem. Could you give an example?
– aws
May 8, 2018 at 10:23

Yes, there are many such results. For example, a very common tool in applications is the Lebesgue measure, used in areas ranging from probability to physics. A familiar property of the Lebesgue measure is that a positive real function necessarily has positive Lebesgue integral. However, such a property depends on the (constructively unacceptable) axiom of choice; see this 2017 publication in Real Analysis Exchange for details.

Some applications of Lebesgue integration in physics and engineering are discussed here.

• I don't think measure theory is needed in "real life". I have a feeling that Riemann integral and finite probability theory suffice for applications, even though they lack the "elegance" mathematicians like. I might be mistaken though, in that case could you be more specific? May 6, 2018 at 10:52
• @Julien__ Oh, it is. Measure theory is a foundation for non discrete probability theory, which is used e.g. by insurance companies to calculate their risks and how much they have to charge for a policy so they can stay in business.
– SK19
May 6, 2018 at 11:02
• I think the issue is not whether measure theory has real life applications (which it indisputably does) but whether it would be possible to replace its real life applications with a stripped-down constructive version. Of course the latter is almost certainly true, given that human experience is inherently finite. The gap seems to be that while nonconstructive mathematics is never absolutely necessary in a formal sense, it does simplify things, and simplification has practical utility.
– Owen
May 6, 2018 at 13:24
• @Owen I think your comment is really the best answer to the question (broadened from measure theory). May 6, 2018 at 13:32
• @Owen, what do you base yourself on when you claim that constructive mathematics simplifies things in the context of Lebesgue measure and/or integration? In this particular case the opposite is true, as using choice one can prove Lebesgue measure to be countably additive ($\sigma$-additive), which simplifies things, and simplification has practical utility. So in this particular case, it is the idealizing assumption of choice that leads to practical utility (not its rejection). May 6, 2018 at 15:41

The extreme value theorem is a typical example of a result that holds classically but is rejected by Errett Bishop's constructive mathematics, and replaced by rather weak versions where the extremum cannot be said to exist. The extreme value theorem is of extreme utility in many applications in physics including the theory of Calabi-Yau manifolds. The existence of such entities depends strongly on highly nontrivial PDEs where existence of extrema is relied upon time and again. See this 2011 article in Intellectica for a more detailed discussion.

• HI Daniel, you are obviously more of an expert in the field than I am, but at any rate I included a comment I found at an Oxford site. It seems to me it is hard to deny that this is a legitimate area of physics. As far as the "approximate" business is concerned, I find it dubious since it would put into question the irrationality of $\sqrt2$ as far as applications are concerned. May 8, 2018 at 8:45