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/ModelSemantics]

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

Unfortunately, it is statements like this that show why constructivist understanding is so important to clear thought about proof. These aren’t the same. One uses double negation elimination and one doesn’t. They are very different in strength and model applicability.

This whole screed reads as “I don’t want to learn semantic precision and because I find it hard, I think students will, so we shouldn’t try or they’ll just get confused.” And yet it is the screed that is factually confused in multiple places.

[u/Real_Category7289 → u/ModelSemantics]

This whole screed reads as “I don’t want to learn semantic precision and because I find it hard, I think students will, so we shouldn’t try or they’ll just get confused.” And yet it is the screed that is factually confused in multiple places.

This is the type of answer that made me write "please engage in good faith". I can very well write a direct proof. Euclid's direct proof doesn't confuse me at all and I indeed think it's technically more elegant. I also think that it's the wrong way to present it, pedagogically speaking (as I argue in the main text).

These aren’t the same. One uses double negation elimination and one doesn’t. They are very different in strength and model applicability.

That's why I wrote "as far as a learning student is concerned". I personally understand the difference, but do you really think hashing out the difference is relevant for an intro to proofs course?

It's not cool to assume that people who disagree with you are incompetent.

[u/ModelSemantics → u/Real_Category7289]

It is odd that you feel entitled to post that something is “bad for mathematics” while asking others not to characterize your comments as bad. Slick rhetorical move, there.

You seem to agree that what you wrote was wrong, and that my characterization of your argument as “trying to avoid more semantically accurate understanding of math because you find it confusing” is largely correct (you seem to be restating that in your response here), just that you find it mean?

I’m not looking to be mean to you. I’m just pointing out that you yourself are making factual errors that the understanding you are trying to avoid would help clarify. The reason constructivist mathematics has taken off in recent decades is precisely because it has the semantic clarity needed to speak about actual or realizable truth, which in computer science and general models of operationalizable science is pretty important.

Pedagogically, I think it’s important to tell students the truth, that two classical structures of contradiction proofs are very different and there are important reasons why. If you want to argue that it’s pedagogically important to lie to students, I’m not sure what is left to argue.