Hacker News Reader

Comment by codeflo | Hacker News Reader

I wonder what’s going on with the passive aggressive edit war in this answer: 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/propIX...)

View on HN

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

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.

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.

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.

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

> Sorry. Point taken. I'm way too quick to annoy at the moment

That makes two of us. No offense taken.

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

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.

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

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.

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

You might be interested to know that in intuitionistic logic, you still have a one-sided contrapositive law, i.e. (A > B) > (~B > ~A):

  [1] A > B(assumption)
  [2] ~B (assumption)
  [3] A (assumption)
  [4] B (modus ponens on 1 and 3)
  [5] ~A (proof of negation on 3, 4 and 2)

It's only the converse that no longer holds. In general familiar equivalences from classical logic are still valid in intuitionistic logic but only in one direction.

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.

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.

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

I am certainly not intending to intentionally spread FUD, though I guess you probably mean that I am unintentionally propagating FUD spread by other people.

All I mean by saying it's a "logical error" is that it's not an argument which is always valid. Of course particular instances can still be correct.

I think a definition of "proof by contradiction" which includes proof of negation is useful if you are reasoning classically (and this doesn't have to be something you always do, or always avoid; you can reason classically some of the time and intuitionistically some of the time). Although the ideal situation to avoid any confusion would be to have three separate terms, one covering both types of proof and two for the individual types.

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.

Reply on news.ycombinator.com