| 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. |
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.