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.
I 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.
My 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.
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:
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.
Thanks, 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.
I 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.
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".
Yes I understand, but why do you think it needs justification? As far as I understand this is simply the definition of implication in classical logic, for one it follows from the truth tables of both expressions.
Well, that's exactly what people were considering and what the article is referring too, a variant of classical logic where everything except the law of excluded middle holds true. I don't think this is uninteresting, which postulates are independent from one another is one of the core problems in logic.
Arguably, the common sense definition of 'A -> B' is simply modus ponens. That is 'Given A and A->B, it follows that B'. It's then no longer obvious that A -> B is equivalent to ~A v B.
Indeed, implication in IL is different from material implication even though IL has modus ponens.
I didn't mean to flame, I thought we were having an interesting debate. I was under the impression we we're talking about logic systems in general where reductio ad absurdum exists, but the law of the excluded middle doesn't. Anyway, thanks, I learnt much.
This would be a very peculiar logic I think, maybe you just come from a very different background and hence all the hair-splitting was necessary, we just wandered so far away from the original point I lost patience, maybe unnecessarily, in the end it really was an interesting debate for me too.
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/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.