Hacker News Reader

Comment by millimeterman | Hacker News Reader

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

View on HN

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

Oops, good catch.

Actually, the thing that is excluded in constructive mathematics is ~ ~ P -> P. ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics.

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

Here is a StackExchange post: https://math.stackexchange.com/questions/2453533/triple-nega...

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.

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

The terminology gets abused a lot, even by professors. It's actually hard to find theorems which really require proof by contradiction.

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.

Reply on news.ycombinator.com