5 ms·

I wonder what’s going on with the passive aggressive edit war in this answer: https://mathoverflow.net/a/23521 https://mathoverflow.net/a/23521 It’s about whet

I wonder what’s going on with the passive aggressive edit war in this answer: https://mathoverflow.net/a/23521 https://mathoverflow.net/a/23521 It’s about whether Euclid’s proof that there’s no finite set of primes is a proof by contradiction or not. The fact that this is disputed at all shows a certain unwillingness to use original sources — maybe each of them only looked at a different textbook’s restatement of the proof. Because no matter whether a proof of the theorem can be stated without contradiction, it took me all of 30 seconds to find a translation of the original proof to show that Euclid did in fact use one: > I say that G is not the same with any of the numbers A, B, and C. > If possible, let it be so. Now A, B, and C measure DE, therefore G also measures DE. But it also measures EF. Therefore G, being a number, measures the remainder, the unit DF, which is absurd. (http://aleph0.clarku.edu/~djoyce/java/elements/bookIX/propIX20.html http://aleph0.clarku.edu/~djoyce/java/elements/bookIX/propIX...)

ogogmad 5y ago
You can read the proof as saying that for any finite set of primes, there is a prime number outside the set. And within the context of Euclid's proof, given the set {A,B,C} of primes, the proof constructs a prime G outside of it. Within constructive logic, there are different non-equivalent definitions of infiniteness (that are all equivalent in classical logic): - A set is non-finite if its finiteness leads to a contradiction. - A set is infinite if any finite subset of it can be extended. Infiniteness implies non-finiteness, but non-finiteness does not imply infiniteness. Further discussion can be found here: http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/infinite+set http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/infin... Within the context of the MathOverflow answer, the claim that Euclid's proof establishes infiniteness as opposed to non-finiteness, is correct. And the proof is therefore not "by contradiction", because that would only show non-finiteness. [edit] Edited out some impoliteness.
- codeflo 5y ago
  Trying to be maximally precise, the prime G isn’t really constructed, but it must exist because ABC+1 must have a prime factorization by the fundamental theorem of arithmetic. And the contraction is that G can’t be any of {A, B, C}. Edit: The above added a nit-picky side-point to your original response, which was a lot shorter. Afterwards, you edited your reply to be a lot more exhaustive and a lot less... friendly? I don't think that's the best way to use HN's edit window. But see my grandchild comment below for my response to all the points you edited in afterwards.
  - ogogmad 5y ago
    G's existence is proved in a way which is valid in constructive foundations. It is therefore constructed. And this construction can be carried out algorithmically: Just find the prime factors of ABC+1. Obviously, this is not computationally efficient, but constructive logic doesn't care. Constructive logic only cares that a construction can be carried out, and that its worst case time complexity has some explicit bound. The existence of this bound for finding larger primes implies a weak bound on the density of the primes. Also, I made some edits to my original comment.
    - codeflo 5y ago
      Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Some points I’d like to clarify: 1. Multiple contradictory edits in the answer is weird by Stack Exchange standards regardless of the merits of the discussion, that’s the main thing I observed. 2. Whether Euclid uses contradiction or not is not really open to interpretation: the word “absurd” appears right in the proof. If people want to split hairs about whether that contradiction is in the lemma or the main proof, I guess fine. 3. There are of course multiple subschools of constructivism that accept and don’t accept different things. Not all of them ignore computational complexity. For example, some ultrafinitists reject the unique prime factorization theorem on the basis that you can’t really execute the factorization algorithm even for relatively modest numbers. To be clear, that’s not exactly my view, but I would for example agree that something like “just find the prime factors” sweeps a bit of relevant subtlety under the rug: you can only do that conceptually, not actually.
      - ogogmad 5y ago
        > Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Sorry. Point taken. I'm way too quick to annoy at the moment, and I retroactively edit too much. I probably should keep my comments relatively unchanged after making them. > If people want to split hairs This entire discussion is about splitting hairs. And the MO answer acknowledges that there's a contradiction somewhere, and only argues over where it is. See the last edit on the answer.
Yajirobe 5y ago
That edit history is ridiculuous and one of the reasons I hate such reddit-esque conversations. It's a bunch of people thinking they know their stuff giving wrong answers.
quietbritishjim 5y ago
This statement can be proved without contradiction (except the little one in the middle mentioned in the current answer): (1) Given a finite set of primes {p_1, ... p_n}, then there exists another prime not in that set. However, turning that into the following statement does require proof by contradiction (or, equivalently, the law of the excluded middle): (2) There are an infinite number of primes Euclid himself made statement (1) and proved it without contradiction, so looking at the original source gives the impression that you don't need it. But (2) is so similar-looking that many people incorrectly make the deduction that it doesn't need proof by contradiction either.
- ceh123 5y ago
  You could state (2) as a contrapositive where your re-phrasing of (2) is: If A is the set of all primes, then A is an infinite set. Contrapositive proof: Suppose A is a finite set containing only primes. By (1) we know there exists some p not in A and therefore A is not the set of all primes. I don't believe contrapositive needs law of excluded middle but I'm honestly not sure. Logic is not my area
  - quietbritishjim 5y ago
    Oops, perhaps I meant proof by contradiction is equivalent to contrapositive (rather than equivalent to law of excluded middle). If you write out a classic high school proof by contradiction formally, then you find yourself basically writing out the contrapositive. Let's say you know A and ~B=>~A, then you can deduce B. Proof by contradiction: assume otherwise, i.e. ~B, then by ~B=>~A you have ~A, but that contradicts A. So if you have ~B=>~A then you have A=>B.
    - ceh123 5y ago
      Okay yup, turns out this is correct and it's slightly upsetting to me honestly haha. Just for someone else if they're interested where contrapositive and contradiction both use law of excluded middle (the ==* step requires it): Contrapositive: A-> B == A or ~B == ~B or A ==* ~B or ~(~A) == ~B -> ~A Contradiction: ~(~A and B) == ~~A or ~B ==* A or ~B == A -> B
morelisp 5y ago
On the other hand, "Euclid's proof is not not by contradiction" is a (probably unintentional) meta-restatement of the constructive vs. classical approaches.
puffoflogic 5y ago
What you have quoted is a proof of negation, which is not the same as proof by contradiction. Your quoted part of the proof is constructive, ergo not by contradiction. Proof by contradiction has the following form: ~A -> false |- A. But the quoted proof has the form A -> false |- ~A.
housecarpenter 5y ago
The issue is that some people believe in intuitionistic logic, so to them, there's a difference between assuming something is true and deriving absurdity in order to prove its negation (which they think is perfectly fine, and which is what Euclid was doing), and assuming that its negation is false and deriving absurdity in order to prove that it's true (which they think is a logical error). They reserve the term "proof by contradiction" only for the latter type of proof, i.e. the one they think is not a valid type of proof. Whereas for believers in classical logic, to say that something is true is just to say that its negation is false, so they don't generally care about the distinction between these two types of proof---as far as they're concerned it's a valid proof, and a "proof by contradiction", either way.
- puffoflogic 5y ago
  > which they think is a logical error This is FUD designed to discredit intuitionistic logic. An instance of LEM is not "a logical error"; it is merely a claim which requires justification. For the claim at hand -- i.e. some natural number G is a member of a finite, constructed set, or it is not -- the corresponding LEM instance is perfectly true [and proven]. We say that the claim is decidable. So (given that we have a proof the claim is decidable) there would be no problem in intuitionistic logic with this part of Euclid's proof even if it took the form of a proof by contradiction (which of course it doesn't). To make a more general rebuttal of the FUD, proofs by contradiction are not automatically invalid in intuitionistic logic; they just require one extra piece of evidence. Furthermore the claim that whether something is a proof by contradiction depends on one's position on the logical validity of LEM is ridiculous on its face. There is a fact of the matter as to whether any given proof is by contradiction. There may be disagreements as to the definition of "proof by contradiction", but the definition which includes proof of negation is completely useless. In mathematics we usually treat useless definitions as in some sense "false" in order to facilitate communication - e.g., 1 could be prime depending on definitions, but that would be useless so we facilitate communication by treating "1 is prime" as false. Likewise here we should treat as false the claim that the quoted section of Euclid's proof is by contradiction. Source for claims about LEM/proof by contradiction: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...

ogogmad 5y ago

You can read the proof as saying that for any finite set of primes, there is a prime number outside the set. And within the context of Euclid's proof, given the set {A,B,C} of primes, the proof constructs a prime G outside of it. Within constructive logic, there are different non-equivalent definitions of infiniteness (that are all equivalent in classical logic): - A set is non-finite if its finiteness leads to a contradiction. - A set is infinite if any finite subset of it can be extended. Infiniteness implies non-finiteness, but non-finiteness does not imply infiniteness. Further discussion can be found here: http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/infinite+set http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/infin... Within the context of the MathOverflow answer, the claim that Euclid's proof establishes infiniteness as opposed to non-finiteness, is correct. And the proof is therefore not "by contradiction", because that would only show non-finiteness. [edit] Edited out some impoliteness.

codeflo 5y ago
Trying to be maximally precise, the prime G isn’t really constructed, but it must exist because ABC+1 must have a prime factorization by the fundamental theorem of arithmetic. And the contraction is that G can’t be any of {A, B, C}. Edit: The above added a nit-picky side-point to your original response, which was a lot shorter. Afterwards, you edited your reply to be a lot more exhaustive and a lot less... friendly? I don't think that's the best way to use HN's edit window. But see my grandchild comment below for my response to all the points you edited in afterwards.
- ogogmad 5y ago
  G's existence is proved in a way which is valid in constructive foundations. It is therefore constructed. And this construction can be carried out algorithmically: Just find the prime factors of ABC+1. Obviously, this is not computationally efficient, but constructive logic doesn't care. Constructive logic only cares that a construction can be carried out, and that its worst case time complexity has some explicit bound. The existence of this bound for finding larger primes implies a weak bound on the density of the primes. Also, I made some edits to my original comment.
  - codeflo 5y ago
    Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Some points I’d like to clarify: 1. Multiple contradictory edits in the answer is weird by Stack Exchange standards regardless of the merits of the discussion, that’s the main thing I observed. 2. Whether Euclid uses contradiction or not is not really open to interpretation: the word “absurd” appears right in the proof. If people want to split hairs about whether that contradiction is in the lemma or the main proof, I guess fine. 3. There are of course multiple subschools of constructivism that accept and don’t accept different things. Not all of them ignore computational complexity. For example, some ultrafinitists reject the unique prime factorization theorem on the basis that you can’t really execute the factorization algorithm even for relatively modest numbers. To be clear, that’s not exactly my view, but I would for example agree that something like “just find the prime factors” sweeps a bit of relevant subtlety under the rug: you can only do that conceptually, not actually.
    - ogogmad 5y ago
      > Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Sorry. Point taken. I'm way too quick to annoy at the moment, and I retroactively edit too much. I probably should keep my comments relatively unchanged after making them. > If people want to split hairs This entire discussion is about splitting hairs. And the MO answer acknowledges that there's a contradiction somewhere, and only argues over where it is. See the last edit on the answer.

Yajirobe 5y ago

That edit history is ridiculuous and one of the reasons I hate such reddit-esque conversations. It's a bunch of people thinking they know their stuff giving wrong answers.

quietbritishjim 5y ago

This statement can be proved without contradiction (except the little one in the middle mentioned in the current answer): (1) Given a finite set of primes {p_1, ... p_n}, then there exists another prime not in that set. However, turning that into the following statement does require proof by contradiction (or, equivalently, the law of the excluded middle): (2) There are an infinite number of primes Euclid himself made statement (1) and proved it without contradiction, so looking at the original source gives the impression that you don't need it. But (2) is so similar-looking that many people incorrectly make the deduction that it doesn't need proof by contradiction either.

ceh123 5y ago
You could state (2) as a contrapositive where your re-phrasing of (2) is: If A is the set of all primes, then A is an infinite set. Contrapositive proof: Suppose A is a finite set containing only primes. By (1) we know there exists some p not in A and therefore A is not the set of all primes. I don't believe contrapositive needs law of excluded middle but I'm honestly not sure. Logic is not my area
- quietbritishjim 5y ago
  Oops, perhaps I meant proof by contradiction is equivalent to contrapositive (rather than equivalent to law of excluded middle). If you write out a classic high school proof by contradiction formally, then you find yourself basically writing out the contrapositive. Let's say you know A and ~B=>~A, then you can deduce B. Proof by contradiction: assume otherwise, i.e. ~B, then by ~B=>~A you have ~A, but that contradicts A. So if you have ~B=>~A then you have A=>B.
  - ceh123 5y ago
    Okay yup, turns out this is correct and it's slightly upsetting to me honestly haha. Just for someone else if they're interested where contrapositive and contradiction both use law of excluded middle (the ==* step requires it): Contrapositive: A-> B == A or ~B == ~B or A ==* ~B or ~(~A) == ~B -> ~A Contradiction: ~(~A and B) == ~~A or ~B ==* A or ~B == A -> B

morelisp 5y ago

On the other hand, "Euclid's proof is not not by contradiction" is a (probably unintentional) meta-restatement of the constructive vs. classical approaches.

puffoflogic 5y ago

What you have quoted is a proof of negation, which is not the same as proof by contradiction. Your quoted part of the proof is constructive, ergo not by contradiction. Proof by contradiction has the following form: ~A -> false |- A. But the quoted proof has the form A -> false |- ~A.

housecarpenter 5y ago

The issue is that some people believe in intuitionistic logic, so to them, there's a difference between assuming something is true and deriving absurdity in order to prove its negation (which they think is perfectly fine, and which is what Euclid was doing), and assuming that its negation is false and deriving absurdity in order to prove that it's true (which they think is a logical error). They reserve the term "proof by contradiction" only for the latter type of proof, i.e. the one they think is not a valid type of proof. Whereas for believers in classical logic, to say that something is true is just to say that its negation is false, so they don't generally care about the distinction between these two types of proof---as far as they're concerned it's a valid proof, and a "proof by contradiction", either way.

puffoflogic 5y ago
> which they think is a logical error This is FUD designed to discredit intuitionistic logic. An instance of LEM is not "a logical error"; it is merely a claim which requires justification. For the claim at hand -- i.e. some natural number G is a member of a finite, constructed set, or it is not -- the corresponding LEM instance is perfectly true [and proven]. We say that the claim is decidable. So (given that we have a proof the claim is decidable) there would be no problem in intuitionistic logic with this part of Euclid's proof even if it took the form of a proof by contradiction (which of course it doesn't). To make a more general rebuttal of the FUD, proofs by contradiction are not automatically invalid in intuitionistic logic; they just require one extra piece of evidence. Furthermore the claim that whether something is a proof by contradiction depends on one's position on the logical validity of LEM is ridiculous on its face. There is a fact of the matter as to whether any given proof is by contradiction. There may be disagreements as to the definition of "proof by contradiction", but the definition which includes proof of negation is completely useless. In mathematics we usually treat useless definitions as in some sense "false" in order to facilitate communication - e.g., 1 could be prime depending on definitions, but that would be useless so we facilitate communication by treating "1 is prime" as false. Likewise here we should treat as false the claim that the quoted section of Euclid's proof is by contradiction. Source for claims about LEM/proof by contradiction: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016...