# Proof by contradiction in Constructive Mathematics

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.

• Note that saying 'assume $\neg p$, blah blah, contradiction' is still a fine argument - but what it proves is $\neg \neg p$, and in constructive mathematics you can't infer $p$ from $\neg \neg p$. Feb 8, 2019 at 2:27
• Note that it is more accurate to say "intuitionistically", since "constructive" is not at all restricted to only "intuitionistic" in general. Also note that negation in intuitionistic logic is not the same as negation in classical logic, hence the asymmetry. It so happens that ¬P and (P⇒⊥) are classically equivalent, but that does not imply that classical negation is the same as intuitionistic negation. Feb 8, 2019 at 7:24
• A very deep question indeed. It is the difference between "If we add assumption ~p to the system, does it break down? If it breaks down, we cannot add ~p to the system (but we do not have license to add p to the system either)." and "If we add assumption p to the system, does it break down? If it breaks down, we can definitely add ~p to the system as anything else would not make sense." Aug 5, 2022 at 9:06

## 2 Answers

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, \lnoti}$$

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

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 :)

• Perhaps it's worth adding that TND stands for "tertium non datur" also known as LEM "law of excluded middle", which states $p\lor \lnot p$ and is, in a sense, "the" axiom of classical logic which is not postulated by constructive logic.
– chi
Feb 8, 2019 at 10:32