5 ms·

1) it's not a proof by contradiction, it's a proof of a negation :grump: 2) I am not a fan of this phrasing "we can't simplify forever". Why can't we? It's obv

1) it's not a proof by contradiction, it's a proof of a negation :grump: 2) I am not a fan of this phrasing "we can't simplify forever". Why can't we? It's obvious if you phrase it in the usual way as "the denominator is strictly smaller than it was before", but the "simplify" operation is kind of complex! They don't even mention "decreasing" until the very final Note box where they say offhand that actually it's an infinite descent (which is a critical part of the proof they've otherwise handwaved).

thaumasiotes 2y ago
> 1) it's not a proof by contradiction, it's a proof of a negation :grump: I don't get your complaint. It is a proof of a negation, yes, the conclusion is that √2 ∉ ℚ. But the proof is done by contradiction; "it's not a proof by contradiction" is flat-out false. "Proof by contradiction" describes the method of the proof, and "proof of a negation" describes its conclusion, which is why one of those phrases uses by and the other one uses of.
- Smaug123 2y ago
  https://en.wikipedia.org/wiki/Proof_by_contradiction https://en.wikipedia.org/wiki/Proof_by_contradiction, https://ncatlab.org/nlab/show/proof+by+contradiction https://ncatlab.org/nlab/show/proof+by+contradiction, https://web.stanford.edu/class/cs103/guide_to_proofs#proof-by-contradiction https://web.stanford.edu/class/cs103/guide_to_proofs#proof-b... all agree (the first three things that came up when I googled for "proof by contradiction"): a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true. There is already a perfectly cromulent term for proofs of negations: "refutation by contradiction" (https://ncatlab.org/nlab/show/refutation+by+contradiction https://ncatlab.org/nlab/show/refutation+by+contradiction), which admittedly nlab says it prefers to its other name "proof of negation".
  - renewiltord 2y ago
    The two seem isomorphic. Just sub R for \not P. Doesn't seem to change anything interesting about the proof structure.
    - Smaug123 2y ago
      As I said, according to the three sources above, which are the first sources I clicked on which didn't seem like blogspam, the phrase "proof by contradiction" is a term of art which means "uses the law of excluded middle to conclude the truth of a statement given a proof that its negation is false". It may be unfortunate that the mathematical world has standardised on the phrase "proof by contradiction" for this, but it has standardised on that phrase!
      - wazdra 2y ago
        > but it has standardised on that phrase! To me, the only formal distinction you can make between the two lies in the use of the excluded middle. However, this distinction has not standardised in mathematics, as many mathematicians simply do not care for intuitionistic logic. Such a mathematician could see the above proof as: I want to show ¬P by contradiction. Therefore I assume ¬(¬P) which is just P to me (the unintuitionistic mathematician has just used the excluded middle, without really caring). I derive a contradiction. Therefore ¬P holds. While I personally enjoy the kind of subtleties that can be thought of about mathematical reasoning, I also think the rant-train on contradiction vs negation must stop. You are expecting a consensus from the wrong community.
        thaumasiotes 2y ago
        > To me, the only formal distinction you can make between the two lies in the use of the excluded middle. It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all.
        Smaug123 2y ago
        Could you please explain this? Clearly we both understand something completely different by either the term "excluded middle" or "contradiction". Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.
  - thaumasiotes 2y ago
    > a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true. And this proof matches that description exactly, with P = "√2 ∉ ℚ". The only case where these would be different ideas is the case where ¬¬P ≠ P. And of course, that can never happen.
    - Smaug123 2y ago
      Your statement is, I think, being wilfully sloppy. To quote the outline of the proof: "First Euclid assumed √2 was a rational number.". To quote the proof itself: "Euclid's proof starts with the assumption that √2 is equal to a rational number p/q.". In two different places, the proof explicitly states that it is showing that "√2 in ℚ" is false. It is not showing that "√2 ∉ ℚ" is not false; such a proof would begin "Suppose that it were not the case that √2 ∉ ℚ", which is obviously not how the proof starts (and for good reason, because that would be much more confusing). By all means argue that "nobody cares about excluded middle"! You're probably right, and when I insist that "proof by contradiction" has a meaning that is correctly stated by Wikipedia and the nlab, I'm just like one of the old fogeys complaining about things like "could care less" or "irregardless"! But don't misquote arguments and say that they support your case when they don't.
LudwigNagasena 2y ago
It's both a proof by contradiction and a refutation by contradiction because it's the same thing in this context. Positing "P = is rational and ¬P = is irrational" is as valid as positing "P = is irrational and ¬P = is rational".
- Smaug123 2y ago
  No, "is not irrational" isn't the same as "is rational" without excluded middle; that's the whole point. (Equality of real numbers is not computable, so there is nonconstructive content to the implication "if not irrational, then rational".) (I will retract a whole bunch of my worldview if you can inhabit the type "not-not-rational -> rational" in something like MLTT.)
  - LudwigNagasena 2y ago
    You take a set S and partition it into two subsets, A and B, so that each element uniquely belongs to either of them. For each element of S it is true that "not-not-in-A -> in-A". Can this be shown to be true in MLTT? I don't know much about setoids to show it, but if it can't, that's the problem of MLTT, not mine. In the context of this proof, it is true.
ginkoleaf 2y ago
This distinction is only made by a small number of mostly constructivists. It is not common usage, and most working mathematicians will have no idea what you're talking about.
thaumasiotes 2y ago
> They don't even mention "decreasing" until the very final Note box where they say offhand that actually it's an infinite descent (which is a critical part of the proof they've otherwise handwaved). That isn't actually a critical part of the proof; you can just assume that your initial two integers are relatively prime and then derive a contradiction directly.
- Smaug123 2y ago
  Then why didn't they! Of course the proof can be fixed, we all know sqrt(2) is irrational, but why get so close to proving it and then just not finish the job?

thaumasiotes 2y ago

> 1) it's not a proof by contradiction, it's a proof of a negation :grump: I don't get your complaint. It is a proof of a negation, yes, the conclusion is that √2 ∉ ℚ. But the proof is done by contradiction; "it's not a proof by contradiction" is flat-out false. "Proof by contradiction" describes the method of the proof, and "proof of a negation" describes its conclusion, which is why one of those phrases uses by and the other one uses of.

Smaug123 2y ago
https://en.wikipedia.org/wiki/Proof_by_contradiction https://en.wikipedia.org/wiki/Proof_by_contradiction, https://ncatlab.org/nlab/show/proof+by+contradiction https://ncatlab.org/nlab/show/proof+by+contradiction, https://web.stanford.edu/class/cs103/guide_to_proofs#proof-by-contradiction https://web.stanford.edu/class/cs103/guide_to_proofs#proof-b... all agree (the first three things that came up when I googled for "proof by contradiction"): a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true. There is already a perfectly cromulent term for proofs of negations: "refutation by contradiction" (https://ncatlab.org/nlab/show/refutation+by+contradiction https://ncatlab.org/nlab/show/refutation+by+contradiction), which admittedly nlab says it prefers to its other name "proof of negation".
- renewiltord 2y ago
  The two seem isomorphic. Just sub R for \not P. Doesn't seem to change anything interesting about the proof structure.
  - Smaug123 2y ago
    As I said, according to the three sources above, which are the first sources I clicked on which didn't seem like blogspam, the phrase "proof by contradiction" is a term of art which means "uses the law of excluded middle to conclude the truth of a statement given a proof that its negation is false". It may be unfortunate that the mathematical world has standardised on the phrase "proof by contradiction" for this, but it has standardised on that phrase!
    - wazdra 2y ago
      > but it has standardised on that phrase! To me, the only formal distinction you can make between the two lies in the use of the excluded middle. However, this distinction has not standardised in mathematics, as many mathematicians simply do not care for intuitionistic logic. Such a mathematician could see the above proof as: I want to show ¬P by contradiction. Therefore I assume ¬(¬P) which is just P to me (the unintuitionistic mathematician has just used the excluded middle, without really caring). I derive a contradiction. Therefore ¬P holds. While I personally enjoy the kind of subtleties that can be thought of about mathematical reasoning, I also think the rant-train on contradiction vs negation must stop. You are expecting a consensus from the wrong community.
      - thaumasiotes 2y ago
        > To me, the only formal distinction you can make between the two lies in the use of the excluded middle. It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all.
        Smaug123 2y ago
        Could you please explain this? Clearly we both understand something completely different by either the term "excluded middle" or "contradiction". Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.
- thaumasiotes 2y ago
  > a proof by contradiction is specifically a proof which shows that P is not false, and concludes that it is true. And this proof matches that description exactly, with P = "√2 ∉ ℚ". The only case where these would be different ideas is the case where ¬¬P ≠ P. And of course, that can never happen.
  - Smaug123 2y ago
    Your statement is, I think, being wilfully sloppy. To quote the outline of the proof: "First Euclid assumed √2 was a rational number.". To quote the proof itself: "Euclid's proof starts with the assumption that √2 is equal to a rational number p/q.". In two different places, the proof explicitly states that it is showing that "√2 in ℚ" is false. It is not showing that "√2 ∉ ℚ" is not false; such a proof would begin "Suppose that it were not the case that √2 ∉ ℚ", which is obviously not how the proof starts (and for good reason, because that would be much more confusing). By all means argue that "nobody cares about excluded middle"! You're probably right, and when I insist that "proof by contradiction" has a meaning that is correctly stated by Wikipedia and the nlab, I'm just like one of the old fogeys complaining about things like "could care less" or "irregardless"! But don't misquote arguments and say that they support your case when they don't.

LudwigNagasena 2y ago

It's both a proof by contradiction and a refutation by contradiction because it's the same thing in this context. Positing "P = is rational and ¬P = is irrational" is as valid as positing "P = is irrational and ¬P = is rational".

Smaug123 2y ago
No, "is not irrational" isn't the same as "is rational" without excluded middle; that's the whole point. (Equality of real numbers is not computable, so there is nonconstructive content to the implication "if not irrational, then rational".) (I will retract a whole bunch of my worldview if you can inhabit the type "not-not-rational -> rational" in something like MLTT.)
- LudwigNagasena 2y ago
  You take a set S and partition it into two subsets, A and B, so that each element uniquely belongs to either of them. For each element of S it is true that "not-not-in-A -> in-A". Can this be shown to be true in MLTT? I don't know much about setoids to show it, but if it can't, that's the problem of MLTT, not mine. In the context of this proof, it is true.

ginkoleaf 2y ago

This distinction is only made by a small number of mostly constructivists. It is not common usage, and most working mathematicians will have no idea what you're talking about.

thaumasiotes 2y ago

> They don't even mention "decreasing" until the very final Note box where they say offhand that actually it's an infinite descent (which is a critical part of the proof they've otherwise handwaved). That isn't actually a critical part of the proof; you can just assume that your initial two integers are relatively prime and then derive a contradiction directly.

Smaug123 2y ago
Then why didn't they! Of course the proof can be fixed, we all know sqrt(2) is irrational, but why get so close to proving it and then just not finish the job?