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

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 by showing that 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 by contradiction. This means that you allow yourself to assume and show a contradiction from there. The assumption is equivalent to , but in order to use such an assumption, you actually have to produce an , 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 once when proving a statement . Absolutely amazing!

It gets even more amazing: Once you’ve committed to doing that, there’s a question: Does proving mean you’re allowed to use both and in your proof of , or that you could use either to prove ? 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!