5 ms·
In a logical system you have axioms, that are sentences that are true by definition and proof methods which are rules of sentence transformation that are assume
by stiff 14y ago
In a logical system you have axioms, that are sentences that are true by definition and proof methods which are rules of sentence transformation that are assumed to preserve truthiness. The law of noncontradiction is an axiom that states:
X and (not X) == False for any sentence X
If you start with a sentence y, and then via the proof methods arrive at a sentence (not y), this is the same as saying
(y -> (not y)) == True
Which is equivalent to:
((not y) or (not y)) == True
Which is equivalent to:
(not y) == True
Now, if you accept the law of non-contradiction this implies that:
y == False
If you do not accept it, y can both True and False at the same time and the proof method is not valid anymore. Hence the proof method of reductio ad absurdum, or "proof by contradiction" as you call it, is valid if and only if this law holds.
- DigitalTurk 14y agoThe law of excluded middle is not sufficient for proof by contradiction. What you actually need is ex falso quodlibet (principle of explosion). For instance, paraconsistent logic has the law of excluded middle but not ex falso quodlibet. https://en.wikipedia.org/wiki/Principle_of_explosion https://en.wikipedia.org/wiki/Principle_of_explosion https://en.wikipedia.org/wiki/Paraconsistent_logic https://en.wikipedia.org/wiki/Paraconsistent_logic -- addendum Specifically, notice that in classical logic the axioms law of excluded middle and law of non-contradiction can be substituted for one another (they are equivalent). However, that is not the case for all semantics.
- stiff 14y agoI just wanted to explain the authors mental leap, I originally said: if you do not accept the law of excluded middle than proof by contradiction ceases to be a valid proof method. The law of excluded middle might not be sufficient, but is necessary for the reductio ad absurdum and proof by contradiction methods. You are right though I jumped too quickly to the "if and only if", the details get quite complicated.
- DanWaterworth 14y agoMy point is that you can add reductio ad absurdum as an axiom. So long as you can't then derive the law of the excluded middle, your assertion is incorrect.
- deleted 14y ago[deleted]
- stiff 14y agoReductio ad absurdum is: (x->(~x))->(~x) Law of excluded middle is: x | ~x Proof follows: (x->(~x))->(~x) From definition of implication is equivalent to: (~x) | ~(x->(~x)) From definition of implication is equivalent to: (~x) | ~((~x) | (~x)) From de Morgans law is equivalent to: (~x) | (x & x) From identity law is equivalent to: ~x | x I am not a logician and I might not have gotten all the details right, but I certainly think this is possible. I also have quite a good proof by authority ;) in form of an article by Alonzo Church: http://www.ams.org/journals/bull/1928-34-01/S0002-9904-1928-04516-0/S0002-9904-1928-04516-0.pdf http://www.ams.org/journals/bull/1928-34-01/S0002-9904-1928-...
- DigitalTurk 14y agoThat looks correct to me. Actually, at first I thought it was incorrect because you used De Morgan's law, which I mistakenly thought was invalid in intuitionistic logic. However, I looked it up and apparently only ~(p & q) |- ~p v ~q is invalid in IL.
- stiff 14y agoThanks, that was the part I felt uncertain about, funny how this seems completely elementary on one hand and on the other it is so easy to make a mistake.
- DanWaterworth 14y agoCan you justify using material implication? It's possible to create reductio ad absurdum in Coq: Definition reductioAdAbsurdum (X:Prop) (f : (X -> (X -> False))) (x:X) : False := f x x. But not the law of the excluded middle. Edit: It's much clearer in Idris: reductioAdAbsurdum : (x -> (x -> _|_)) -> (x -> _|_) reductioAdAbsurdum f x = f x x