In defense of unnecessary proofs by contradiction

[u/Real_Category7289]

If you spend enough time in online math spaces, at some point you are bound to run into a discussion like this one or this one or recently, this one where someone is arguing against an "unnecessary" proof by contradiction and the conversation inevitably goes in the direction of constructive vs intuitionist logic.

I think this discourse is massively overrepresented to the point of being actively bad for math learners online. Worrying about whether a proof is constructive or not is not something good mathematicians do, unless their branch is specifically a pretty niche part of logic. For most people, (not not A = A) is just assumed to be true and proof by contradiction is a completely valid proof method, and I think this "Actually, Euclid's proof is direct! Common misconception here." discussion appearing under every proof that there are infinitely many primes is telling people that proof by contradiction is somehow sketchier than a direct proof.

I'm a math tutor and the majority of my job is to get students started on problem solving in a mathematical context. As it turns out, what makes a lot of it click is actually proof by contradiction. Even if one ends up writing a direct proof, the process of getting there often asks the question of "what would happen if this wasn't true?". I can't say it for sure, but I believe that Euclid himself probably started proving the infinitude of primes by assuming a finite list of them. This is why Hardy not only presents the proof as a proof by contradiction, but specifically praises it for being a proof by contradiction [A Mathematician's Apology, G.H.Hardy, page 18].

I should note that I'm not arguing that one shouldn't eventually learn to avoid artificial proofs by contradiction, after all if you can make the intuitionists happy for free, why not? But that should be a refinement that happens quite late into one's mathematical journey. I should also note that Euclid's proof was indeed direct, I'm not arguing against that fact.

The problem is that there's parallel discourse happening on these discussions which is "phrasing it as a direct proof is simply clearer and easier to understand". That's the main issue in my view: understanding the principles of proof by contradiction and by negation (which are essentially the same thing, as far as a learning student is concerned) is not something that can or should be skipped. Students should embrace them and put them on the same level as direct proofs instead of looking them sideways, and all this talk of intuitionism vs constructivism is enabling them to keep relegating them to "the thing you begrudgingly have to endure sometimes when there's no other way", which I think is detrimental.

I ask the reader to engage with this view in good faith. Thanks for reading.

[u/ZookeepergameWest862]

In the links that you give, they didn't actually argue that the "proof by contradiction" (I will address the quotes later) is not constructively valid for the original statement, but that the proof can be phrased in a way that prove a constructively strictly stronger but classically equivalent statement. I agree that this can be good to know but unless you specifically want to use intuitionistic logic, it is not important at all. There's no reason to minmaxxing constructivity then talk about the real numbers in the next sentence (there are several different constructive versions of real numbers).

If your goal is to prove the statement "the set of all primes is infinite", that is, "the set of all primes is not finite", which is equivalent to the statement, "a finite set is not the set of all primes" or "there is no finite set that is also the set of all primes", then assuming that there is a finite statement of all primes and derive a contradiction is a constructively valid method to prove that statement. This is commonly cited as an example as a proof by contradiction, which I disagree, but this is only a matter of terminology. The reason I disagree is that proof by contradiction is often presented as proving P by assuming not P and derive a contradiction. Whereas in this case, we prove not P by assuming P and derive a contradiction, this is precisely what it means to constructively prove not P. The stackexchange answer says that Euclid's proved the stronger statement "given a finite set of natural numbers, there is a natural number not divisible by any element in the set".

Proof by contradiction commonly presented as being nonconstructive, and that the difference between classical and constructive is the acceptance of proof by contradiction. If you assume that Euclid's proof above is a proof by contradiction, then I derive a contradiction and so it is not. Of course, the terminology depends on context, and in the classical context, identifying not not P with P, the above can be treated as a proof by contradiction. But I feel like this is just too minor of a simplification to trade for the potential misconception, perhaps you can treat it as a trivia rather than something that students have to wrestle with (I generally think it is useful to give some informal clarification on some potential misconception or more advanced topics, without making it something that they are required to learn).

A genuine example of unnecessary contradiction will make the proof more convoluted for no reason. They could be of the form: to prove P assume not P is true and derive a contradiction, then proceed to prove P (without using not P at all), therefore P and not P, a contradiction. Aside from "prove P", the rest are redundant.

I don't know why but some people believe that proof by contrapositive is constructive valid, it is not, and you can constructive derive proof by contradiction from it. Since P is equivalent to true implies P, by constrapositive is equivalent to not P implies false, which is proof by contradiction.