The reason for the “discomfort” with the proof by contradiction rule (RAA, reduction ad absurdum) is that it is not “constructive” (technically, not intuitionistic). The best way to understand this is by formalizing logic in natural deduction style. In intuitionistic logic (Brouwer) in natural deduction style (Gentzen, Prawitz), there is a rule that allows the deduction of ANY proposition from a deduction (from premises) that yields falsity (F). There is also a rule (implication introduction) that allows you to deduce P => Q from a deduction of Q under the premise P. The negation of a proposition neg P is an abbreviation for P => F (F is the symbol for falsity). Then the implication introduction rule yields the rule that says that if you can deduce F from P then P => F, that is neg P, is provable. In particular, if you can deduce F from neg P then you can deduce neg neg P. But, in intuitionistic logic P is NOT provable from neg neg P in general (the law of the excluded middle)! This is equivalent to the fact that P or neg P is NOT provable in general in intuitionistic logic. In fact, the proof by contradiction rule (RAA) is equivalent to adding P or neg P as axioms to intuitionistic logic, or to add axioms neg neg P => P in intuitionistic logic. I explain all this in chapter 2 of my book on discrete math (Section 2.4) see second edition in progress http://www.cis.upenn.edu/~jean/discmath-root-b.pdf Best, -- Jean Gallier
On Feb 2, 2017, at 9:08 PM, Brent Meeker <meekerdb@verizon.net> wrote:
Right. And it's even harder than finding the chain of implication; it's finding the a Z to start from. That's because you only know not-Z because Z is absurd. But a false proposition implies anything. So /*logically*/ you can start from any absurdity but to get anywhere you have to get to a Z that's implied by not-Y, which is implied by not-W, etc.
Brent
On 2/2/2017 5:56 PM, William R Somsky wrote:
If the 'reducto' proof is:
not-X => A => B => ... => Y => Z, but Z is clearly false, hence not-not-X, ie X
you should be able to invert that to be
not-Z (which is clearly true) => not-Y => ... => not-B => not-A => X
but good luck trying to find that from starting at the not-Z end.
On 2017-02-02 17:15, David Wilson wrote:
The reduction ad absurdum argument to prove X generally goes not-X => ... => false, a contradiction, therefore X is true. e.g. not-X => A, not-X => not-A, hence x => A and not-A => F, therefore X is true. I've always found such arguments, while effective, in a way unsatisfying, because by the time you find your contradiction, you have wander far from your premise. I was wondering if there might always be a way to turn such an argument around, so that a proof of not-X => false, can be flipped to prove the contrapositive, true => X. I'm obviously not talking about building the argument around not-X => false and then invoking the contrapositive, but rather inverting the entire argument into a direct argument where X appears only as the last statement proven, not as part of an earlier supposition.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com https://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun