# But Why Is Proof by Contradiction Non-Constructive?

We think of a proof as being non-constructive if it proves “There exists an $x$ such that $P(x)$ without ever actually exhibiting such an $x$.

If you want to form a system of mathematics where all proofs are constructive, one thing you can do is remove the principle of proof by contradiction: the principle that you can prove a statement $P$ by showing that $\neg P$ is false. (Let’s leave aside set-theoretical considerations for the moment.)

But one thing you can ask is: exactly why is the principle of proof by contradiction non-constructive? In the paper Linear logic for constructive mathematics, Mike Shulman gave an answer which I found quite mind-blowing: Imagine you’re proving $\exists x\,P(x)$ by contradiction. This means that you allow yourself to assume $\neg\exists x\,P(x)$ and show a contradiction from there. The assumption is equivalent to $\forall x\,\neg P(x)$, but in order to use such an assumption, you actually have to produce an $x$, so shouldn’t that be constructive?

The answer is that yes it will be, unless you use the hypothesis more than once! So (the paper reasons), you can form a constructive system of mathematics not by removing the law of proof by contradiction, but by requiring you to only use a hypothesis $P$ once when proving a statement $P\rightarrow Q$. Absolutely amazing!

It gets even more amazing: Once you’ve committed to doing that, there’s a question: Does proving $(A\wedge B)\rightarrow C$ mean you’re allowed to use both $A$ and $B$ in your proof of $C$, or that you could use either to prove $C$? Both are reasonable interpretations, so conjunction splits into two separate connectives.

Dually, disjunction also splits into two connectives, and these two connectives can be given the interpretations of “constructive-or” and “non-constructive-or”. Fantastic!