[MaxRegret]

Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth, rather than a reasonable view of what a proof by contradiction is?

I agree with what you say about mathematicians, being in an adjacent field myself. However, most mathematicians are not logicians, and we are seldom careful about making distinctions that only matter in non-classical logics. I do think that this particular distinction (between proving negation vs. proving the negation of a negation) is worth making, though.

Even if we are, as a matter of practice, used to invoking the law of the excluded middle without a second thought, I think it's good to keep in mind in which proofs it is actually required and where it is not. So, for example, and to the GP's point, proving ¬Q ⇒ ¬P by proving P ⇒ Q doesn't require LEM, but the converse does.

The trouble is that when translating mathematics to logic, it's often not clear what is a negation and what isn't. Is "x is irrational" the sentence ¬P for P being "x is rational" or is it simply an atomic sentence on its own? 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.

[saithound]

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.

[MaxRegret]

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.

[saithound]

> If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.

Fwiw, I am in full agreement, and it's commendable when people do have at least a basic understanding of intuitionistic logic.

My remark was simply that the majority in the field don't make this (barely 16 years old) distinction between "proof of negation" and "proof by contradiction", and it has come to be associated with a more introductory or superficial understanding. This is not to suggest that everyone who uses Bauer's terms has a superficial understanding, e.g. Bauer and Escardo are top tier and certainly use it a lot.

I also don't say that this distinction is unique to Bauer. I'm saying he invented and popularized it (I was in fact there in the 2010 thread where it was invented).

With that out of the way:

> It's simply a way to square two widely-held beliefs, even amongst professional mathematicians [...] > > 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.

Well, yes, one should correct the first widely held belief, because it is a baseless misconception (or rather, was a baseless misconception under the reading of everyone before 2010).

There is no necessity to divide it into “two kinds,” or to speak of positive and negative statements though. If one assumes not-X and thereby arrives at a contradiction, then one has indeed established that not-X is not the case. This works the same way in both classical and intuitionistic logic, in both classical and constructive mathematics.

If you have some way of going from not-not-X to X, then you also proved X. The difference between classical logic and intuitionistic logic is that the latter does not admit any general way of going from not-not-X to X.

This is what's actually going on, and it's entirely orthogonal to proofs by contradictions. Redefining "proof by contradiction" to make a common misconception come out right does not help communicate this in any way, since the end of a proof by contradiction is not the only place where double negations are eliminated in classical mathematics.

If anything, it obscures what is going on: mathematicians usually come away with more misconceptions, like "in constructive mathematics you are not allowed to assume a negative". And it makes it a fair bit harder for constructive mathematicians to converse clearly with the rest of the mathematical world.