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

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"

(quote from you; my emphasis)

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.