Hacker News Reader

Comment by DanWaterworth | Hacker News Reader

This is the sentence in question:

The first controversy occurred early in Hilbert’s career and concerned his vigorous use of the "law of the excluded middle" (proof by contradiction).

I don't see how you can interpret that as not implying that the law of the excluded middle and proof by contradiction are not one and the same thing.

if you do not accept the law of excluded middle than proof by contradiction ceases to be a valid proof method.

I don't believe that this is true, because that would imply that you can derive the law of the excluded middle from proof by contradiction.

View on HN

This is explained here nicely: http://philosophy.stackexchange.com/questions/1890/what-is-t...

The law of noncontradiction and proof by contradiction are different things.

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.

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/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.

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.

Reductio 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-...

That 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.

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.

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

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.

I 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

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.

OK, but we're not talking about classical logic, otherwise the question about whether the law of the excluded middle is derivable is uninteresting.

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.

Nice flame, eot.

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.

Actually, 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.

Actually, this is wrong. Reductio ad absurdum should be:

    ((~x) -> x) -> x

or:

    ((x -> _|_) -> x) -> x

Which is not constructible in Coq/Idris.

http://en.wikipedia.org/wiki/Reductio_ad_absurdum#The_princi...

I think stiff is correct here. You can derive the law of the excluded middle from proof by contradiction, obviously in classical logic but even in constructive logic.* See this blog post by Andrej Bauwer for an explanation: http://math.andrej.com/2010/03/29/proof-of-negation-and-proo...

* although there are logics in which this does not hold, but that's probably not what you are talking about here

I've tried to do so in Idris, but I haven't been able to:

    deriveExcludedMiddle : ((x:Type) -> ((x -> _|_) -> x) -> x) -> Either y (y -> _|_)

So, perhaps I am relying on one of those logics where it doesn't hold.

Shouldn't that be ((x -> _|_) -> _|_) -> x) and the y's at the end should presumably x's.

And shouldn't the quantification over x:Type be separately over each part?

(((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)) -> x) is more accurate. In any case, each of the three types are equivalent.

I wanted:

    (forall x. ((~x) -> x) -> x) -> (forall y. y \/ (~y))

Rather than:

    (forall x. (((~x) -> x) -> x) -> x \/ (~x))

Proof by contradiction goes like this: You assume ~x, and from this you derive a contradiction _|_. Then you conclude x. So from ~x -> _|_ we derive x. In other words: (~x -> _|_) -> x. That's the same as ((x -> _|_) -> _|_) -> x. But in any case, as you said, this is equivalent to (~x -> x) -> x because ~x -> x is equivalent to ~x -> _|_.

I think strictly speaking, _|_ isn't a contradiction, it's an absurdity. (x, x -> _|_) is a contradiction.

Ah I see, that's where the terminological differences came from.

Here is the thing you're looking for. LEM is law of excluded middle, DN is double negation elimination law. Lets define some type abbreviations:

    LEM = (x:Type) -> Either x (x -> _|_)
    DN = (x:Type) -> ((x -> _|_) -> _|_) -> x

We first constructively prove not not LEM:

    notnotLEMproof : (x:Type) -> ((LEM x) -> _|_) -> _|_
    notnotLEMproof x f = f (Right (\a -> f (Left a))

Now we can use double negation to obtain a proof for LEM:

    DNimpliesLEM : DN -> LEM
    DNimpliesLEM dn x = dn (LEM x) (notnotLEMproof x)

I hope this is correct, since I don't know Idris syntax. If Idris supports implicit parameters, you would not need the x's:

    notnotLEM f = f (Right (\a -> f (Left a))

    DNimpliesLEM dn = dn LEM notnotLEMproof

Thank you ever so much. I only had to make a few changes to make it work. Providing a computer verified proof is quite a definitive way of winning an argument.

    LEM : (x:Type) -> Type
    LEM x = Either x (x -> _|_)

    DN : (x:Type) -> Type
    DN x = ((x -> _|_) -> _|_) -> x

    notnotLEMproof : {x:Type} -> ((LEM x) -> _|_) -> _|_
    notnotLEMproof {x} f = f (Right (\a => f (Left a)))

    DNimpliesLEM : ((x:Type) -> DN x) -> LEM y
    DNimpliesLEM {y} dn = dn (LEM y) notnotLEMproof

Yes, thank you, I made some stupid mistakes there.

I find the last one slightly clearer if you change the argument order:

    DNimpliesLEM : ((x:Type) -> DN x) -> ((y:Type) -> LEM y)
    DNimpliesLEM dn y = dn (LEM y) (notnotLEMproof y)

Although with the original formulation you could prove the slightly stronger version:

    DNimpliesLEM : (x:Type) -> DN (LEM x) -> LEM x
    DNimpliesLEM x dn = dn (notnotLEMproof x)

so that you don't need DN z to be true for all z, but just on the z you need (i.e. z = LEM x). It was an interesting exercise, and I learned a lot. First I tried proving (((x:Type) -> LEM x) -> _|_ ->) _|_ to then apply double negation directly to this, but this is actually not possible (as far as I can see). The double negation needs to be inside the quantifier.

Maybe you can even write it simply like this with implicit parameters:

    DNimpliesLEM : DN (LEM x) -> LEM x
    DNimpliesLEM dn = dn notnotLEMproof

Reply on news.ycombinator.com