3 ms·
> [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 negatio
by 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 agoOops, good catch.
- cjfd 6y agoActually, 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 agoHere 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 agoIt 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.