4 ms·

Proofs by contradiction are not accepted in some flavors of mathematics, like constructive mathematics. In fact, constructive mathematicians believe in a defini

Proofs by contradiction are not accepted in some flavors of mathematics, like constructive mathematics. In fact, constructive mathematicians believe in a definition of real numbers that is more in line with what this paper talks about.

millimeterman 6y ago
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.
ogogmad 6y ago
Proofs that derive a contradiction are perfectly acceptable in constructive mathematics. Indeed, the real numbers are uncountable in constructive mathematics. What is not allowed is elimination of double negatives, which is not present in the above proof.
- adamnemecek 6y ago
  I'm not sure that real numbers are uncountable in constructive mathematics as they are not computable.
  - ogogmad 6y ago
    See Andrej Bauer's proof that they are indeed uncountable: https://mathoverflow.net/questions/30643/are-real-numbers-countable-in-constructive-mathematics https://mathoverflow.net/questions/30643/are-real-numbers-co...
    - adamnemecek 6y ago
      I'm still unconvinced.
      - fractionalhare 6y ago
        Is there a specific issue you have with this proof? With respect, I think you may be conflating a constructive proof of the uncountability of the reals with a proof that the set of all computable reals is countable. These are two different claims. A statement about the reals which is provable under constructive mathematics does not reduce to a statement about the computable reals and vice versa. A set can be constructively definable without all of its elements being constructively enumerable.
      - ogogmad 6y ago
        Given any explicit sequence of real numbers, it's always possible to generate a number not in that sequence. In fact, this can be done algorithmically using essentially Cantor's method.
Davidzheng 6y ago
Ok I think what happens here is that we assume for the real numbers an increasing sequence which is bounded converges. I think that a number system with this property is probably already hard to construct in constructive math.
- Davidzheng 6y ago
  So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all, not that it's uncountable if you have its properties. Also the deeper point is that you have all the properties of the real numbers you can actually derive the law of excluded middle. (Coming from the supremum axiom)
  - adamnemecek 6y ago
    This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
    - Smaug123 6y ago
      I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
  - ogogmad 6y ago
    > So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all No. They exist in any topos with a Natural Number Object. In other words, they exist in all varieties of constructive mathematics that admit a set of natural numbers.
    - chongli 6y ago
      Brouwer (father of intuitionism) rejected actual infinity. He would not admit the axiom of infinity and therefore reject the set of all natural numbers. Tough to do things that way though.

millimeterman 6y ago

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.

ogogmad 6y ago

Proofs that derive a contradiction are perfectly acceptable in constructive mathematics. Indeed, the real numbers are uncountable in constructive mathematics. What is not allowed is elimination of double negatives, which is not present in the above proof.

adamnemecek 6y ago
I'm not sure that real numbers are uncountable in constructive mathematics as they are not computable.
- ogogmad 6y ago
  See Andrej Bauer's proof that they are indeed uncountable: https://mathoverflow.net/questions/30643/are-real-numbers-countable-in-constructive-mathematics https://mathoverflow.net/questions/30643/are-real-numbers-co...
  - adamnemecek 6y ago
    I'm still unconvinced.
    - fractionalhare 6y ago
      Is there a specific issue you have with this proof? With respect, I think you may be conflating a constructive proof of the uncountability of the reals with a proof that the set of all computable reals is countable. These are two different claims. A statement about the reals which is provable under constructive mathematics does not reduce to a statement about the computable reals and vice versa. A set can be constructively definable without all of its elements being constructively enumerable.
    - ogogmad 6y ago
      Given any explicit sequence of real numbers, it's always possible to generate a number not in that sequence. In fact, this can be done algorithmically using essentially Cantor's method.

Davidzheng 6y ago

Ok I think what happens here is that we assume for the real numbers an increasing sequence which is bounded converges. I think that a number system with this property is probably already hard to construct in constructive math.

Davidzheng 6y ago
So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all, not that it's uncountable if you have its properties. Also the deeper point is that you have all the properties of the real numbers you can actually derive the law of excluded middle. (Coming from the supremum axiom)
- adamnemecek 6y ago
  This is really interesting. I'm not surprised by axiom of choice being based on real numbers. I've been thinking about that lately but I don't have a good intuition why. Do you have a link?
  - Smaug123 6y ago
    I'd be very surprised if it were true in general. But there certainly has to be some non-computational component to the reals being a complete totally ordered Archimedean field, because the question of deciding the equality of two reals is uncomputable, so there is no procedure to decide the total order.
- ogogmad 6y ago
  > So the problem that constructive math has for real numbers is that it's hard to show real numbers exist at all No. They exist in any topos with a Natural Number Object. In other words, they exist in all varieties of constructive mathematics that admit a set of natural numbers.
  - chongli 6y ago
    Brouwer (father of intuitionism) rejected actual infinity. He would not admit the axiom of infinity and therefore reject the set of all natural numbers. Tough to do things that way though.