When reflecting on applications of proof in the real-world, I find that I am only considering constructive proofs. For example, algorithms for performing robotic movement are useful because they provide instructions to be performed, not because it can be proven that such instructions exist.

What is an example where "proving that such instructions exist" has been sufficient for a real-world application?

  • 2
    $\begingroup$ Are you restricting attention only to algorithm design, or to mathematics as a whole? There are a lot of useful statements along the lines of "this bad thing doesn't happen", which don't construct anything because there's nothing to construct. Do you mean non-constructive existence proofs? These are quite useful in PDE theory and to a much lesser extent ODE theory. $\endgroup$ – Ian Nov 11 '15 at 0:55
  • $\begingroup$ Maybe both are interesting? Non-constructive existence proofs are what I was thinking of, so making a connection between such a proof and "this let us build that bridge" would be fascinating. $\endgroup$ – ToBeReplaced Nov 11 '15 at 4:17
  • $\begingroup$ Also, I worry that my language is ambiguous. In particular, I would like to see physical manifestations of proofs that do not require the law of excluded middle. $\endgroup$ – ToBeReplaced Nov 11 '15 at 4:21
  • $\begingroup$ The tradition in PDE theory (in problems where everything goes through nicely) is to prove existence, uniqueness, and regularity properties before coming up with ways to construct solutions (analytically or numerically). For example, in elliptic PDE there is the Lax-Milgram theorem, which gives existence and uniqueness. The particular way that it does that suggests that the finite element method might be a useful way to approximate solutions to such equations, though Lax-Milgram itself does not prove that this will work, nor does it provide a "construction" in the ordinary sense by itself. $\endgroup$ – Ian Nov 11 '15 at 4:21
  • $\begingroup$ In other words, I think in a real world application you will need some kind of a construction at the end of the day, but a non-constructive existence proof can be useful in obtaining that construction. The techniques may hint at a way to perform a constructive proof, or they may just make us more confident that an approximation technique should work. $\endgroup$ – Ian Nov 11 '15 at 4:25

Edit: I see that Ian has already given this answer. Nevertheless, I'll leave this here because it offers more detail. This is the closest thing to a real-world application of an existence proof of which I am aware.

Numerical PDE have many applications in modeling physical problems and help us accomplish many engineering feats - for example, building a bridge or placing an oil rig in the ocean.

To be confident in the answers that these numerical methods produce, we must know that the equations involved are well-posed, meaning

1) the solution exists,

2) the solution is unique, and

3) the solution depends continuously on the data given.

If (1) isn't true, then the model is flawed. If (2) isn't true, then which solution are you converging to? If (3) isn't true, then your discretization of the problem may introduce significant errors.

So for numerical PDE to work (and their applications in engineering), non-constructive proofs of existence, uniqueness, and continuity are used.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.