3 ms·

I'm not familiar with this specific proof, but reading the description it sounds perfectly constructive. A true proof by contradiction would be "Assume [0, 1]

I'm not familiar with this specific proof, but reading the description it sounds perfectly constructive. A true proof by contradiction would be "Assume [0, 1] is not uncountable. That leads to a contradiction, so [0, 1] is not not uncountable. By the law of the excluded middle, [0, 1] is therefore uncountable." This proof seems to be "Assume [0, 1] is countable. That leads to a contradiction, so [0, 1] is not countable." That's not a proof by contradiction - it's just how you prove a negative. This is a nice blog post about the distinction: https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/ https://existentialtype.wordpress.com/2017/03/04/a-proof-by-...

fractionalhare 6y ago
Nice comment. A succinct explanation of the difference between negation and contradiction can also be found in this r/math comment: https://reddit.com/r/math/comments/cu9gsk/_/exse1ps/?context=1 https://reddit.com/r/math/comments/cu9gsk/_/exse1ps/?context... The terminology gets abused a lot, even by professors. It's actually hard to find theorems which really require proof by contradiction.
- Smaug123 6y ago
  Well, if your logical system defines "not P" as "assuming P, you can derive falsity", then "uncountable" precisely means "if you assume it is countable then you can derive falsity". That's exactly what the proof did. If you particularly care then you can just replace the final word "contradiction" with "QED"; it doesn't change the structure or content of the proof.
a1369209993 6y ago
> [0, 1] is not not uncountable. By the law of the excluded middle, [0, 1] is therefore uncountable. Nitpick: that's not excluded middle, that's double negation elimination. They're both non-constructive and (IIRC) equivalent in most formalizations, but they're not the same thing.
- millimeterman 6y ago
  Oops, good catch.
- cjfd 6y ago
  Actually, the thing that is excluded in constructive mathematics is ~ ~ P -> P. ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics.
  - a1369209993 6y ago
    > ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics. Could you provide a citation for this? I can vaguely see how that might work, being ~~Q->Q for the special case where Q can be decomposed into Q = ~P, but it's obviously rather difficult to search for.
    - millimeterman 6y ago
      Here is a StackExchange post: https://math.stackexchange.com/questions/2453533/triple-negation-in-intuitionistic-logic https://math.stackexchange.com/questions/2453533/triple-nega...
    - cjfd 6y ago
      It is very easy to prove. Note first that ~P is an abbreviation for P -> False. So we can rewrite this as (~ ~ P -> False) -> P -> False. This is tautologically true by modes ponens if P -> ~ ~ P. But that is a well known fact.

fractionalhare 6y ago

Nice comment. A succinct explanation of the difference between negation and contradiction can also be found in this r/math comment: https://reddit.com/r/math/comments/cu9gsk/_/exse1ps/?context=1 https://reddit.com/r/math/comments/cu9gsk/_/exse1ps/?context... The terminology gets abused a lot, even by professors. It's actually hard to find theorems which really require proof by contradiction.

Smaug123 6y ago
Well, if your logical system defines "not P" as "assuming P, you can derive falsity", then "uncountable" precisely means "if you assume it is countable then you can derive falsity". That's exactly what the proof did. If you particularly care then you can just replace the final word "contradiction" with "QED"; it doesn't change the structure or content of the proof.

a1369209993 6y ago

> [0, 1] is not not uncountable. By the law of the excluded middle, [0, 1] is therefore uncountable. Nitpick: that's not excluded middle, that's double negation elimination. They're both non-constructive and (IIRC) equivalent in most formalizations, but they're not the same thing.

millimeterman 6y ago
Oops, good catch.
cjfd 6y ago
Actually, the thing that is excluded in constructive mathematics is ~ ~ P -> P. ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics.
- a1369209993 6y ago
  > ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics. Could you provide a citation for this? I can vaguely see how that might work, being ~~Q->Q for the special case where Q can be decomposed into Q = ~P, but it's obviously rather difficult to search for.
  - millimeterman 6y ago
    Here is a StackExchange post: https://math.stackexchange.com/questions/2453533/triple-negation-in-intuitionistic-logic https://math.stackexchange.com/questions/2453533/triple-nega...
  - cjfd 6y ago
    It is very easy to prove. Note first that ~P is an abbreviation for P -> False. So we can rewrite this as (~ ~ P -> False) -> P -> False. This is tautologically true by modes ponens if P -> ~ ~ P. But that is a well known fact.