6 ms·

>very very deep level It's not a deep level at all.

Kenji 10y ago
If you write a paper that contains mathematical proofs, it is extremely unlikely that this distinction will play any role whatsoever.
- rocqua 10y ago
  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.
  - tel 10y ago
    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.
    - rocqua 10y ago
      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.
      - tel 10y ago
        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.
  - pflats 10y ago
    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.
- mcguire 10y ago
  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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [2] https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic [3] https://en.wikipedia.org/wiki/Natural_deduction 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 https://en.wikipedia.org/wiki/Closed-world_assumption
- tel 10y ago
  "... 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.

Kenji 10y ago

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

rocqua 10y ago
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.
- tel 10y ago
  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.
  - rocqua 10y ago
    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.
    - tel 10y ago
      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.
- pflats 10y ago
  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.
mcguire 10y ago
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_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [2] https://en.wikipedia.org/wiki/Intuitionistic_logic https://en.wikipedia.org/wiki/Intuitionistic_logic [3] https://en.wikipedia.org/wiki/Natural_deduction 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 https://en.wikipedia.org/wiki/Closed-world_assumption
tel 10y ago
"... 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.