52 ms·
Can you justify using material implication? It's possible to create reductio ad absurdum in Coq: Definition reductioAdAbsurdum (X:Prop) (f : (X -> (X -> F
by DanWaterworth 14y ago
Can 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 agoYes 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.
- DanWaterworth 14y agoOK, but we're not talking about classical logic, otherwise the question about whether the law of the excluded middle is derivable is uninteresting.
- stiff 14y agoWell, 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. Nice flame, eot.
- DanWaterworth 14y agoI 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.
- stiff 14y agoThis 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.
- DigitalTurk 14y agoActually, I guess he's right. 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.
- DanWaterworth 14y agoActually, this is wrong. Reductio ad absurdum should be: ((~x) -> x) -> x or: ((x -> _|_) -> x) -> x Which is not constructible in Coq/Idris.