Difference between proof of negation and proof by contradiction

I stumbled across article titled "Proof of negation and proof by contradiction" in which the author differentiates proof by contradiction and proof by negation and denounces an abuse of language that is "bad for mental hygiene". I get that it is probably a hyperbole but I am genuinely curious about what's so horrible in using those two interchangeably and I struggle to see any difference at all.

• to prove $\neg\phi$ assume $\phi$ and derive absurdity (proof by negation)

and

• to prove $\phi$ suppose $\neg\phi$ and derive absurdity (proof by contradiction)

More specifically the author claims that:

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.

Could you provide an example where the "difference in placement of negations" can be appreciated and make a difference?

The author later use two cases: the irrationality of $\sqrt{2}$ and the statement "a continuous map [0,1) on $\mathbb{R}$ is bounded" but I can't see the difference. If I massage the semantics of the proof a little bit I obtain two valid proofs as well using negation/contradiction.

Can we turn this proof into one that does not use contradiction (but still uses Bolzano-Weierstrass)?

Why would we want to do that if both proof methods are equivalent?

I feel that the crux of the article is the following sentence:

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 have done some research and it seems that $\neg\neg\phi$ is the issue here. To quote Wikipedia\Double_Negation on that:

this principle is considered to be a law of thought in classical logic,2 but it is disallowed by intuitionistic logic

I should probably precise that my maths background is pretty limited so far as I am finishing my first year in college. This is bugging me and I would really appreciate if someone could explain it to me. Layman terms would be great but feel free to dive deeper as well. That will be homework for the summer (and interesting for more advanced readers)!

Are proofs by contradiction and proofs of negation equivalent? If not, in which situation do differences matters and what makes them different?

Solution 1:

Proof of negation and proof by contradiction are equivalent in classical logic. However there are not equivalent in constructive logic.

One would usually define $\neg \phi$ as $\phi \rightarrow \perp$, where $\perp$ stands for contradiction / absurdity / falsum. Then the proof of negation is nothing more than an instance of "implication introduction":

If $B$ follows from $A$, then $A\rightarrow B$. So in particular: If $\perp$ follows from $\phi$, then $\phi \rightarrow \perp$ ($\neg \phi$).

The following rule is of course just a special case:

If $\perp$ follows from $\neg \phi$, then $\neg \neg \phi$.

But the rule $\neg \neg \phi \rightarrow \phi$ is not valid in constructive logic in general. It is equivalent to the law of excluded middle ($\phi\vee \neg \phi$). If you add this rule to your logic, you get classical logic.

Solution 2:

Intuitionistic refusal of double negation is particularly relevant in the context of "existence proofs"; see :

• Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 26 :

Classical logic contains the principle of indirect proof: If $¬A$ leads to a contradiction, $A$ can be inferred. Axiomatically expressed, this principle is contained in the law of double negation, $¬¬A → A$. The law of excluded middle, $A \lor ¬A$, is a somewhat stronger way of expressing the same principle.

Under the constructive interpretation, the law of excluded middle is not an empty "tautology," but expresses the decidability of proposition $A$. Similarly, a direct proof of an existential proposition $∃xA$ consists of a proof of $A$ for some ["witness"] $a$. Classically, we can prove existence indirectly by assuming that there is no $x$ such that $A$, then deriving a contradiction, and concluding that such an $x$ exists. Here the classical law of double negation is used for deriving $∃xA$ from $¬¬∃xA$.

Thus, it is correct to say that, from a constructivist point of view, tertium non datur [i.e. excluded middle] does not apply in general.

Its application to existence proofs impies that the existence of a witness of $A$ is undecided/unproven until we are not able to "show it".

Solution 3:

The proof of irrationality of $\sqrt{2}$: a number is either rational or not rational. The situation of being rational has to be ruled out so being not rational remains. That is called a proof by negation by the author. A proof by contradiction would end into 'rational and not rational'. A subtle difference. I take the 2nd example of the author and rewrite it a bit: Accept f is not unbounded Then there is a sequence $(x_n)$ in $[0,1]$ such that the sequence $f(x_n)$ is increasing and unbounded (this uses Countable Choice, by the way). By Bolzano-Weierstras there is a convergent subsequence $(y_n)$ of $(x_n)$ such that, as f is continuous, the sequence $f(y_n)$ is convergent and thus bounded. In fact there are two different strategies: using 'tertium non datur' and 'contradiction'. Both are closely linked.