Proof of negation and proof by contradictionI am discovering that mathematicians cannot tell the difference between “proof by contradiction” and “proof of negation”. This is so for good reasons, but conflation of different kinds of proofs is bad mental hygiene which leads to bad teaching practice and confusion. For reference, here is a short explanation of the difference between proof of negation and proof by contradiction.
By the way, this post is something I have been meaning to write for a while. It was finally prompted by Timothy Gowers’s blog post “When is proof by contradiction necessary?” in which everything seems to be called “proof by contradiction”.
As far as I can tell, “proof by contradiction” among ordinary mathematicians means any proof which starts with “Suppose …” and ends with a contradiction. But two kinds of proofs are like that:
Proof of negation is an inference rule which explains how to prove a negation:
To prove ¬ϕ, assume ϕ and derive absurdity.
The rule for proving negation is the same classically and intuitionistically. I mention this because I have met ordinary mathematicians who think intuitionistic proofs are never allowed to reach an absurdity.
Proof by contradiction, or reductio ad absurdum, is a different kind of animal. As a reasoning principle it says:
To prove ϕ, assume ¬ϕ and derive absurdity.
As a proposition the principle is written ¬¬ϕ⇒ϕ, which can be proved from the law of excluded middle (and is in fact equivalent to it). In intuitionistic logic this is not a generally valid principle.
Admittedly, the two reasoning principles look very similar. A classical mathematician will quickly remark that we can get either of the two principles from the other by plugging in ¬ϕ and cancelling the double negation in ¬¬ϕ to get back to ϕ. Yes indeed, but the cancellation of double negation is precisely the reasoning principle we are trying to get. These really are different.
I blame the general confusion on the fact that an informal proof of negation looks almost the same as an informal proof by contradiction. In order to prove ¬ϕ a mathematician will typically write:
“Suppose ϕ. Then … bla … bla … bla, which is a contradiction. QED.”
In order to prove ϕ by contradiction a mathematician will typically write:
“Suppose ¬ϕ. Then … bla … bla … bla, which is a contradiction. QED.”
The difference will be further obscured because the text will typically state ¬ϕ in an equivalent form with negation pushed inwards. That is, if ϕ is something like ∃x,∀y,f(y)<x and the proof goes by contradiction then the opening statement will be “Suppose for every x there were a y such that f(y)≥x.” With such “optimizations” we really cannot tell what is going on by looking just at the proof. We have to take into account the surrounding context (such as the original statement being proved).
A second good reason for the confusion is the fact that both proof principles feel the same when we try to use them. In both cases we assume something believed to be false and then we hunt down a contradiction. The difference in placement of negations is not easily appreciated by classical mathematicians because their brains automagically cancel out double negations, just like good students automatically cancel out double negation signs.