4 ms·
The law of excluded middle is not sufficient for proof by contradiction. What you actually need is ex falso quodlibet (principle of explosion). For instance, p
by DigitalTurk 14y ago
The 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
- stiff 14y agoI am assuming that we are talking about taking the law of excluded middle out from classical logic, where all the other things independent from that law still hold, and I think implication being material is independent.
- DanWaterworth 14y agoI mean material implication as in: In propositional logic, material implication is a valid rule of replacement which is an instance of the connective of the same name. It is the rule that states that "P implies Q" is logically equivalent to "not-P or Q". http://en.wikipedia.org/wiki/Implication http://en.wikipedia.org/wiki/Implication
- stiff 14y ago