Hacker News Reader

Comment by rocqua | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com