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!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s