Difference between proof of negation and proof by contradiction

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.

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

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.