I’m watching this video on Constructive Mathematics Five Stages of Accepting Constructive Mathematics, and Andrej Bauer makes the following claim:
Mathematicians call two different things “Proof by Contradiction”. One is assume $\neg p$, blah blah blah contradiction. Therefore, $p$. The other is assume $p$, blah blah blah contradiction. Therefore, $\neg p$. The first is not constructively valid, but the second is. The second is how you prove negation.
I’m confused why the latter is constructively valid. Aren’t the two statements dual to each other in some sense, even constructively speaking? Perhaps I’m confused about proving negation.
Best Answer
One rule is negation-introduction; that is "If we derive a contradiction under an assumption, then we may infer that the premises entail the negation of the assumption." This is a "Proof of Negation". $$\begin{split}\Gamma, p&\vdash \bot\\\hline\Gamma&\vdash\lnot p\end{split}\tag {1, $\lnot$i}$$
Well, what if we derive a contradiction when we assume a negation? Applying this rule we would infer that the premises entail the negation of that negation; ie a 'double negation'. $$\begin{split}\Gamma, \lnot p&\vdash \bot\\\hline\Gamma&\vdash\lnot\lnot p\end{split}\tag 2$$
This is all intuitionistically valid. The difference between intuitionistic (contructive) and classical logic is the rule of double-negation-elimination (DNE), is only admissible under the later; it says "if we can derive a double negation of a proposition we may infer that we can derive the proposition." $$\begin{split}\Gamma &\vdash \lnot\lnot p\\\hline\Gamma&\vdash p\end{split}\tag {3, DNE}$$
Putting (2) and (3) together and we have "Proof by Reduction to Absurdity", and this is why it is not intuitionistically valid. $$\begin{split}\Gamma, \lnot p&\vdash \bot\\\hline\Gamma&\vdash p\end{split}\tag{4, RAA}$$