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

Solution 1:

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.

Solution 2:

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.

Solution 3:

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.

For instance, here one reads:

The theory of strings on Calabi-Yau manifolds was first initiated by Philip Candelas, in collaboration with Horowitz, Strominger and Witten. This has grown into a rich subject, with an intricate interplay between the geometric and topological properties of Calabi-Yau manifolds and particle physics in four dimensions. Indeed, one of the remarkable features of string theory is that it naturally includes the correct ingredients for particle physics, as well as gravity. One finds that different Calabi-Yau manifolds, with different topological shapes, lead to different models of particle physics in four spacetime dimensions. For example, in the simplest models, the number of generations of elementary particles (three in the Standard Model) is related to the Euler number of the Calabi-Yau manifold.