5 ms·

He basically says that Hilbert relied on the law of the excluded middle by using proofs by contradiction, which is valid, because if you do not accept the law o

by stiff 14y ago

He basically says that Hilbert relied on the law of the excluded middle by using proofs by contradiction, which is valid, because if you do not accept the law of excluded middle than proof by contradiction ceases to be a valid proof method.

DanWaterworth 14y ago
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.
- stiff 14y ago
  This is explained here nicely: http://philosophy.stackexchange.com/questions/1890/what-is-the-difference-between-law-of-excluded-middle-and-law-of-non-contradicti http://philosophy.stackexchange.com/questions/1890/what-is-t...
  - DanWaterworth 14y ago
    The law of noncontradiction and proof by contradiction are different things.
    - 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 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 ago
        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.
        DanWaterworth 14y ago
        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.
        deleted 14y ago
        [deleted]
        stiff 14y ago
        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-04516-0/S0002-9904-1928-04516-0.pdf http://www.ams.org/journals/bull/1928-34-01/S0002-9904-1928-...
    - stiff 14y ago
      http://en.wikipedia.org/wiki/Reductio_ad_absurdum#The_principle_of_non-contradiction http://en.wikipedia.org/wiki/Reductio_ad_absurdum#The_princi...
- jules 14y ago
  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-proof-by-contradiction/ 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
  - DanWaterworth 14y ago
    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.
    - jules 14y ago
      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?
      - DanWaterworth 14y ago
        (((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))
        jules 14y ago
        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 -> _|_.

by stiff 14y ago

DanWaterworth 14y ago

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.

stiff 14y ago
This is explained here nicely: http://philosophy.stackexchange.com/questions/1890/what-is-the-difference-between-law-of-excluded-middle-and-law-of-non-contradicti http://philosophy.stackexchange.com/questions/1890/what-is-t...
- DanWaterworth 14y ago
  The law of noncontradiction and proof by contradiction are different things.
  - 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 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 ago
        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.
        DanWaterworth 14y ago
        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.
        deleted 14y ago
        [deleted]
        stiff 14y ago
        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-04516-0/S0002-9904-1928-04516-0.pdf http://www.ams.org/journals/bull/1928-34-01/S0002-9904-1928-...
  - stiff 14y ago
    http://en.wikipedia.org/wiki/Reductio_ad_absurdum#The_principle_of_non-contradiction http://en.wikipedia.org/wiki/Reductio_ad_absurdum#The_princi...
jules 14y ago
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-proof-by-contradiction/ 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
- DanWaterworth 14y ago
  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.
  - jules 14y ago
    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?
    - DanWaterworth 14y ago
      (((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))
      - jules 14y ago
        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 -> _|_.