Proof by contradiction in Constructive Mathematics

Question

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.

Answer 1

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}$$

Answer 2

The second is how you prove negation.

When you are proving "not $A$", you are proving "if $A$, then contradiction", because this is literally how "not $A$" is defined in constructive logic.

When you are proving "$A$", it does not suffice to prove "if not $A$, then contradiction", because $A$ is not defined this way (that would be circular!) and there is no general rule that tells you that "if not $A$, then contradiction" implies $A$. There are situations when this does hold (for example, if $A$ is computable -- i.e., there exists a boolean $a \in \left\{\operatorname{True}, \operatorname{False}\right\}$ such that $A \Longleftrightarrow \left(a = \operatorname{True} \right)$), but these are theorems that have to be proven rather than consequences of a general axiom like TND. (For example, when $A$ is computable -- i.e., when you know a boolean $a \in \left\{\operatorname{True}, \operatorname{False}\right\}$ such that $A \Longleftrightarrow \left(a = \operatorname{True} \right)$ -- you can prove $A$ by proving "if not $A$, then contradiction" -- but the reason why this works is simply that you can distinguish cases based upon whether $a = \operatorname{True}$ or $a = \operatorname{False}$. So, on the level of axioms, you are not using TND, but rather emulating a "proof by contradiction" by inducting (= distinguishing cases) upon a boolean. If you don't know such a boolean $a$, then this trick does not work.)

Yes, these situations are dual in a sense, but "dual" does not mean "equally true" in mathematics. Even in classical mathematics. For example, a basis of a vector space may have any cardinality, but a basis of a dual of a vector space may not :)