Hacker News Reader

Comment by aisofteng | Hacker News Reader

>very very deep level

It's not a deep level at all.

If you write a paper that contains mathematical proofs, it is extremely unlikely that this distinction will play any role whatsoever.

Constructive proofs are better in the sense that they explain how a thing is true.

Consider the intermediate value theorem. The normal proof is by contradiction. However, it doesn't tell you anything about where the intermediate value is reached. One can constructively proof the theorem by bisection. This proof has the added benefit of showing you how to compute where the intermediate value is reached. Or rather, it shows that you can compute the intermediate value.

Meanwhile, the proof by contradiction doesn't tell us if we can ever compute where the intermediate value is reached. Having made the switch to CS from maths, it has struck me how useless some theorems proven by contradiction are.

You can view the issue as viewing math as truth finding in a world of platonic ideals, or math as a the study of computation.

It's not as helpful, but I like to teach my high school students: Say you're planning to rob a jewelry store. You can rob it constructively or by contradiction.

You could case the joint, figure out the guards and the employees, their schedules, their uniforms, the jewels on display, the layout of the place, and so on. You can make a plan, an appropriate scenario, disguises, make a copy of keys, some costume jewelry, some fake uniforms. Really know the place inside and out, Oceans-11 the whole thing. And if you do it right, you can make it out with the jewels before anyone even knows they were stolen.

Or you can get some masks and some baseball bats, steal a semi truck, and drive it through the front window of the jewelry store. If the jewel cases aren't open from the impact, or if someone gets in your way, well, refer back to the baseball bats.

Both accomplish what you set out to do, but the first is clearly more elegant and often takes more work and study, requiring/granting a greater understanding of the system. And future thieves would learn a lot more studying Danny Ocean than they would Johnny Smash-and-Grab.

For finite proofs, proof by contradiction can be interpreted as continuation passing and then results in an algorithm. On the other hand, this algorithm may be no better than exhaustive search.

What do you mean by 'finite proofs'?

In cases where the set of all possible examples is finite, I can see this trick working. Maybe a similar approach still works when all possible examples are enumerable or even recursively enumerable.

None of these hold for the intermediate value theorem on the real number line though.

Definitely, it's super weak but at the same time constructive. The issue is that it essentially ends up becoming a search algorithm where contradiction is backtracking. If the search algorithm doesn't stumble upon the solution (at least in principle) in finite time then it's a bit tough to consider it constructive.

The Curry-Howard isomorphism[1] is usually described as a correspondence between computer programs and mathematical proofs. What they usually mean, but don't usually say, is that the actual correspondence is between computer programs and proofs in intuitionistic or constructive logic[2]. (Natural deduction is a lovely example[3].) The important difference between constructive and "classical" logic is that in the former you cannot use the law of the excluded middle or double-negation-elimination.

One way this difference shows itself is in proofs of existence: rather than just demonstrating that something exists (by virtue of it not-not-existing), you have to create an example of it. This is similar to a program, where you cannot demonstrate that 2+2 has some value and then print "4"; instead you have to calculate 4 before you can print it.

Another weird place it shows up[4] is in Prolog, which uses classical first order logic by the closed-world assumption[5]: anything you cannot prove is false.

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[2] https://en.wikipedia.org/wiki/Intuitionistic_logic

[3] https://en.wikipedia.org/wiki/Natural_deduction

[4] At least I thought so, one morning in the shower.

[5] https://en.wikipedia.org/wiki/Closed-world_assumption

"... in many practical branches of pure and applied mathematics"

On the other hand, there have been many mathematical papers written there this distinction was key. It all depends upon your topic, really, and how many times you have to invoke the hobgoblins of mathematical foundations.

Reply on news.ycombinator.com