Making Sense of Proof by Contradiction [pdf]

The distinction you make is correct in the sense there is indeed a fundamental difference between proving P by assuming not-P and reaching a contradiction and on the other hand proving not-P by assuming P and reaching a contradiction. However, both are called proof by contradiction. It is just plain wrong to say that the second kind is not proof by contradiction. It has been called like that for more than two millenia, whereas intuitionism is a 20th century idea. Besides, if you insist on the difference, then you have to distinguish between positive and negative mathematical properties. For instance, in your example, "finite" is positive and "infinite" is not-finite, so negative. For a classical mathematician, which is most of them, this is actually an undesirable distinction that depends on how things are defined, and is not intuitively clear.

There is something which always made me uncomfortable with informal proof by contradiction (by informal I mean "with pen and paper"). So OK we reach a contradiction, and then immediately "oh yeah, that is _this hypothesis_ which is wrong". Erh, well why exactly this one? All we know is we started from an inconsistent state.

The article enters this territory at the last paragraph and simply concludes "This can be difficult questions to resolve to student's satisfaction", without even trying to answer it.

For the working logician or the constructive mathematician, the distinction that matters is whether an argument uses a constructively invalid instance of the law of excluded middle (or double-negation elimination) or not.

Indeed, long before 2010, they already had perfectly serviceable language for this sort of thing: they said "this proof uses DNE". They do not need a separate, additional term for "this proof of this particular form uses DNE at a very specific place".

> One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.

Bridges, cited above, coauthored with Bishop the main monograph on constructive analysis. Birkedal, for his part, might fairly be said to have done as much as anyone to shape what we now call modern realizability.

They don't scoff at these questions, they take them rather seriously. Yet like almost all mathematicians AND most other logicians, they chose not to use Bauer's terminology.

> Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth?

It's something of a shibboleth because it reveals the speaker first encountered the field through pop literature like blog posts (there is nothing wrong with that), and has not then spent sufficient time with the primary literature to realize that this is not, in fact, customary terminology used by most of those who work in the discipline proper. So it marks the speaker as somebody likely to have somewhat superficial knowledge of the field.

Is your position that the term "proof by contradiction" should not be limited to proofs of ¬¬P followed by double negation elimination, and should instead also encompass proofs of ¬P that start with "suppose P, for contradiction"? I agree that this is in keeping with traditional usage.

But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience):

1. Intuitionistic logic does not admit proof by contradiction. 2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid.

I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link.

The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time.

I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry.

To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.

You give me a rational candidate for √2 and by the argument of the submitted article I “construct” another rational candidate with strictly smaller numerator and denominator.

You give me a rational candidate p/q for log 2 and by the argument of the article I “construct” that p = q = 0.

In both instances I create a contradiction thus showing that you could not have provided me such a rational to begin with.

Now let me show you non-constructively that there are irrationals a and b with a^b rational.

To prove this I consider c = √2^√2. I don’t know whether this is rational or irrational so I invoke the law of the excluded middle.

Suppose c is rational. Then take a = b = √2 and we have a^b = c where a and b are irrational and c is rational.

Otherwise suppose c is irrational. Then take a = c and b = √2 and we have a^b = (√2^√2)^√2 = √2^2 = 2 and again we have our result.

What is the difference here? I have no idea whether c is rational or irrational. Either way I can make it work but I can’t tell you which possibility is the genuine one.

You can actually make better choices of a and b and show this result constructively.

This leads to a deeper question. Are there statements with no constructive proof and how do you prove that. This is beyond my expertise, but there are indeed high-powered logical tools that allow you prove such results for certain statements.

The stuff that human beings have done by simply looking at the stars and dreaming really hard is pretty awe-inspiringly incredible.