> 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.
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.
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!
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.
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.
excluded middle: the logical axiom that, for any proposition P, (P v ¬P) is a tautology/valid/always holds.
contradiction: a proof of ⊥. The definition of ⊥ does not matter (it just means false), thanks to the ex falso quodlibet principle.
A proof by contradiction: proving P by showing that (¬P -> ⊥).
Notice that I haven't defined the ¬ operator. This is due to the fact that its definition differs between classical logic and intuitionistic logic. Since the intuitionistic definition of ¬, i.e. "¬P" is a short-hand for "P -> ⊥", is classically equivalent to the definition of ¬ in the classical context (¬P is the statement "P does not hold"), it makes sense to adopt this definition.
The astute reader will notice that, with this definition of ¬, a proof by contradiction is exactly a proof of ¬¬P,
and it happens that ¬¬P -> P is an equivalent formulation of the excluded middle.
Now, back to Euclid's proof. Let P = "√2 is rational". We want to show Q = ¬P. We can do so by contradiction: assume ¬Q, and derive a contradiction. It *happens* that, when using the scheme of proof by contradiction on a property of the form ¬A, you can simply rearrange the negations to get rid of the use of the excluded middle.
So, going back to your statement,
>Note that Euclid's proof is intuitionistically valid, so it can't use excluded middle.
Well, whether Euclid's proof is intuitionistically valid is a question of point of view. Historically? I doubt it. I doubt that Euclid gave any kind of thought to whether he used the excluded middle, and probably used it pervasively, as all "classical" mathematicians today.
However, I agree that it can be made intuitionistically valid using a purely syntactic rewriting.
Said differently, Euclid's proof does not rely on the excluded middle. This does not mean you cannot use it because that's how you think or because you prefer it that way. When you see the blow-up of sizes of certain proofs in the non-classical context, you understand why many mathematicians would rather not give a thought to their use of the excluded middle.
The same way many people in this thread used the PTA to show that √2 is irrational: that's overkill, but they prefer it that way !
Sure, I agree with everything you've said; I was sloppy in saying "Euclid's proof" (whose baroque language I haven't actually bothered to wade through) when I meant "the proof in the OP", though I was precise in saying "it can't use LEM" where you've interpreted it as "a mathematician can't use LEM".
(I asked for an explanation because I resented being called "dumb" by someone I'm pretty sure doesn't actually understand the distinction I'm talking about.)
>>>> 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"
In that case your "It's much dumber than that, since he's invoking the law of the excluded middle to use contradiction at all." is simply false: you can use contradiction to refute a proposition without proving that proposition, without using LEM.
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.